Browse Groups

• ## "higher order" version of equational-logic completeness for a *fixed* model?

(16)
• NextPrevious
• Dear Members, When trying to switch from a deep to a shallow embedding of a system into the rigidly-typed logic of a theorem prover, I discovered that I need
Message 1 of 16 , Jun 3, 2008
View Source
Dear Members,

When trying to switch from a deep to a shallow embedding of a system
into the rigidly-typed logic of a theorem prover, I discovered that I
need the following seemingly true proposition about equational logic
which, if true, is probably known. I kindly ask for confirmation that
it is true and for some reference and/or hint on how to prove it.
Here is the proposition (I am
mentioning the concepts in full detail to prevent any confusion):

Fix an at least countable set Op of operation symbols and a countable
set Var of variables. Terms T are inductively defined to be either
variables pairs (f,Ts) with f operation symbol and Ts list of terms.
An equation is a pair of terms (T,T'). Given a set A, an
A-environment is a pair (K,L) where K : Op -> (A* -> A) and
L : Var -> A (where A* is the set of lists with elements in A). Given
an A-environment (K,L), a term T has a canonical interpretation
Int(A,K,L,T) as an element of A. An equation (T,T') is said to hold in
A via (K,L), written holds(A,K,L,T,T'), if
Int(A,K,L,T) = Int(A,K,L,T'). (T,T')
is said to hold in A via K, written holds(A,K,T,T'), if
holds(A,K,L,T,T') for all L : Var -> A.
Given a set A, a set of equations Eqs and an equation (T,T'),
Eqs is said to A-deduce semantically (T,T') if
for all K : Op -> (A^* -> A), (holds(A,K,S,S') for all (S,S') in Eqs)
implies holds(A,K,T,T').

Proposition: Fix a set A of the same cardinality as Op, a set of
equations Eqs and an equation (T,T'). Assume Eqs A-deduces
semantically (T,T'). Then Eqs also deduces (T,T') syntactically,
i.e., using the standard equational reasoning rules.

(Note: The model A is *fixed* independently of the set of equations
Eqs, so I cannot assume it to be a term model factored to Eqs.)

Andrei Popescu
• Andrei, This is Birkhoff s completeness theorem for equational logic. See Theorem 2 on page 170 of G. Gratzer s Universal Algebra , 2nd edition. (See also
Message 1 of 16 , Jun 3, 2008
View Source
Andrei,

This is Birkhoff's completeness theorem for equational logic. See Theorem 2 on page 170 of G. Gratzer's "Universal Algebra", 2nd edition. (See also Walter Taylor's appendix in George's text, in particular Theorem 1 on page 381.

Brian

____________________________________________

Dr Brian A. Davey
Department of Mathematics
La Trobe University
Victoria 3086
Australia
Phone (Office): +61 3 9479 2599
Phone (Sec.):  +61 3 9479 2600
FAX: +61 3 9479 2466
Email: B.Davey@...

http://www.latrobe.edu.au/www/mathstats/staff/davey/
____________________________________________

From: univalg@yahoogroups.com [mailto:univalg@yahoogroups.com] On Behalf Of uuomul
Sent: Wednesday, 4 June 2008 4:03 AM
To: univalg@yahoogroups.com
Subject: [univalg] "higher order" version of equational-logic completeness for a *fixed* model?

Dear Members,

When trying to switch from a deep to a shallow embedding of a system
into the rigidly-typed logic of a theorem prover, I discovered that I
need the following seemingly true proposition about equational logic
which, if true, is probably known. I kindly ask for confirmation that
it is true and for some reference and/or hint on how to prove it.
Here is the proposition (I am
mentioning the concepts in full detail to prevent any confusion):

Fix an at least countable set Op of operation symbols and a countable
set Var of variables. Terms T are inductively defined to be either
variables pairs (f,Ts) with f operation symbol and Ts list of terms.
An equation is a pair of terms (T,T'). Given a set A, an
A-environment is a pair (K,L) where K : Op -> (A* -> A) and
L : Var -> A (where A* is the set of lists with elements in A). Given
an A-environment (K,L), a term T has a canonical interpretation
Int(A,K,L,T) as an element of A. An equation (T,T') is said to hold in
A via (K,L), written holds(A,K,L, T,T'), if
Int(A,K,L,T) = Int(A,K,L,T' ). (T,T')
is said to hold in A via K, written holds(A,K,T, T'), if
holds(A,K,L, T,T') for all L : Var -> A.
Given a set A, a set of equations Eqs and an equation (T,T'),
Eqs is said to A-deduce semantically (T,T') if
for all K : Op -> (A^* -> A), (holds(A,K,S, S') for all (S,S') in Eqs)
implies holds(A,K,T, T').

Proposition: Fix a set A of the same cardinality as Op, a set of
equations Eqs and an equation (T,T'). Assume Eqs A-deduces
semantically (T,T'). Then Eqs also deduces (T,T') syntactically,
i.e., using the standard equational reasoning rules.

(Note: The model A is *fixed* independently of the set of equations
Eqs, so I cannot assume it to be a term model factored to Eqs.)

Andrei Popescu

• Brian, Do you know that my book is again available? GG
Message 1 of 16 , Jun 3, 2008
View Source
Brian,

Do you know that my book is again available?

GG

On 3-Jun-08, at 7:17 PM, Brian Davey wrote:

Andrei,

This is Birkhoff's completeness theorem for equational logic. See Theorem 2 on page 170 of G. Gratzer's "Universal Algebra", 2nd edition. (See also Walter Taylor's appendix in George's text, in particular Theorem 1 on page 381.

Brian

____________ _________ _________ _________ _____

Dr Brian A. Davey
Department of Mathematics
La Trobe University
Victoria 3086
Australia
Phone (Office): +61 3 9479 2599
Phone (Sec.):  +61 3 9479 2600
FAX: +61 3 9479 2466
Email: B.Davey@latrobe. edu.au

http://www.latrobe. edu.au/www/ mathstats/ staff/davey/
____________ _________ _________ _________ _____

From: univalg@yahoogroups .com [mailto:univalg@ yahoogroups. com] On Behalf Of uuomul
Sent: Wednesday, 4 June 2008 4:03 AM
To: univalg@yahoogroups .com
Subject: [univalg] "higher order" version of equational-logic completeness for a *fixed* model?

Dear Members,

When trying to switch from a deep to a shallow embedding of a system
into the rigidly-typed logic of a theorem prover, I discovered that I
need the following seemingly true proposition about equational logic
which, if true, is probably known. I kindly ask for confirmation that
it is true and for some reference and/or hint on how to prove it.
Here is the proposition (I am
mentioning the concepts in full detail to prevent any confusion):

Fix an at least countable set Op of operation symbols and a countable
set Var of variables. Terms T are inductively defined to be either
variables pairs (f,Ts) with f operation symbol and Ts list of terms.
An equation is a pair of terms (T,T'). Given a set A, an
A-environment is a pair (K,L) where K : Op -> (A* -> A) and
L : Var -> A (where A* is the set of lists with elements in A). Given
an A-environment (K,L), a term T has a canonical interpretation
Int(A,K,L,T) as an element of A. An equation (T,T') is said to hold in
A via (K,L), written holds(A,K,L, T,T'), if
Int(A,K,L,T) = Int(A,K,L,T' ). (T,T')
is said to hold in A via K, written holds(A,K,T, T'), if
holds(A,K,L, T,T') for all L : Var -> A.
Given a set A, a set of equations Eqs and an equation (T,T'),
Eqs is said to A-deduce semantically (T,T') if
for all K : Op -> (A^* -> A), (holds(A,K,S, S') for all (S,S') in Eqs)
implies holds(A,K,T, T').

Proposition: Fix a set A of the same cardinality as Op, a set of
equations Eqs and an equation (T,T'). Assume Eqs A-deduces
semantically (T,T'). Then Eqs also deduces (T,T') syntactically,
i.e., using the standard equational reasoning rules.

(Note: The model A is *fixed* independently of the set of equations
Eqs, so I cannot assume it to be a term model factored to Eqs.)

Andrei Popescu

• Dear George, Can your UA book be ordered now? (Springer?) Fred ... Dear George, Can your UA book be ordered now? (Springer?) Fred Le 4 juin 08 à 04:23, George
Message 1 of 16 , Jun 4, 2008
View Source
Dear George,

Can your UA book be ordered now? (Springer?)

Fred

Le 4 juin 08 à 04:23, George Gratzer a écrit :

Brian,

Do you know that my book is again available?

GG

On 3-Jun-08, at 7:17 PM, Brian Davey wrote:

Andrei,

This is Birkhoff's completeness theorem for equational logic. See Theorem 2 on page 170 of G. Gratzer's "Universal Algebra", 2nd edition. (See also Walter Taylor's appendix in George's text, in particular Theorem 1 on page 381.

B

• Dear Fred, I have not tried, but I assume so. GG ... Dear Fred, I have not tried, but I assume so. GG On 4-Jun-08, at 3:35 AM, Friedrich Wehrung wrote: Dear
Message 1 of 16 , Jun 4, 2008
View Source
Dear Fred,

I have not tried, but I assume so.

GG

On 4-Jun-08, at 3:35 AM, Friedrich Wehrung wrote:

Dear George,

Can your UA book be ordered now? (Springer?)

Fred

Le 4 juin 08 à 04:23, George Gratzer a écrit :

Brian,

Do you know that my book is again available?

GG

On 3-Jun-08, at 7:17 PM, Brian Davey wrote:

Andrei,

This is Birkhoff's completeness theorem for equational logic. See Theorem 2 on page 170 of G. Gratzer's "Universal Algebra", 2nd edition. (See also Walter Taylor's appendix in George's text, in particular Theorem 1 on page 381.

B

• I checked on amazon.com. There, the paperback version can be pre-ordered. Is there a hard copy version available? Matt Insall From: univalg@yahoogroups.com
Message 1 of 16 , Jun 4, 2008
View Source

I checked on amazon.com. There, the paperback version can be pre-ordered. Is there a hard copy version available?

Matt Insall

From: univalg@yahoogroups.com [mailto:univalg@yahoogroups.com] On Behalf Of George Gratzer
Sent: Wednesday, June 04, 2008 9:14 AM
To: univalg@yahoogroups.com
Subject: Re: [univalg] UA book?

Dear Fred,

I have not tried, but I assume so.

GG

On 4-Jun-08, at 3:35 AM, Friedrich Wehrung wrote:

Dear George,

Can your UA book be ordered now? (Springer?)

Fred

Le 4 juin 08 à 04:23, George Gratzer a écrit :

Brian,

Do you know that my book is again available?

GG

On 3-Jun-08, at 7:17 PM, Brian Davey wrote:

Andrei,

This is Birkhoff's completeness theorem for equational logic. See Theorem 2 on page 170 of G. Gratzer's "Universal Algebra", 2nd edition. (See also Walter Taylor's appendix in George's text, in particular Theorem 1 on page 381.

B

• I called the publisher. It slipped from June to mid July. GG ... I called the publisher. It slipped from June to mid July. GG On 4-Jun-08, at 9:30 AM, Insall,
Message 1 of 16 , Jun 4, 2008
View Source
I called the publisher. It slipped from June to mid July.

GG

On 4-Jun-08, at 9:30 AM, Insall, Matt wrote:

I checked on amazon.com. There, the paperback version can be pre-ordered. Is there a hard copy version available?

Matt Insall

From: univalg@yahoogroups .com [mailto:univalg@ yahoogroups. com] On Behalf Of George Gratzer
Sent: Wednesday, June 04, 2008 9:14 AM
To: univalg@yahoogroups .com
Subject: Re: [univalg] UA book?

Dear Fred,

I have not tried, but I assume so.

GG

On 4-Jun-08, at 3:35 AM, Friedrich Wehrung wrote:

Dear George,

Can your UA book be ordered now? (Springer?)

Fred

Le 4 juin 08 à 04:23, George Gratzer a écrit :

Brian,

Do you know that my book is again available?

GG

On 3-Jun-08, at 7:17 PM, Brian Davey wrote:

Andrei,

This is Birkhoff's completeness theorem for equational logic. See Theorem 2 on page 170 of G. Gratzer's "Universal Algebra", 2nd edition. (See also Walter Taylor's appendix in George's text, in particular Theorem 1 on page 381.

B

• Hello Andrei, i) Why do you need the same cardinality with alphabet and function symbols? ii) From syntactical equivalence folows semantical equivalence in the
Message 1 of 16 , Jun 5, 2008
View Source
Hello Andrei,

i) Why do you need the same cardinality with alphabet and function
symbols?

ii) From syntactical equivalence folows semantical equivalence in the
theory used, but not vice versa, as can be seen by the terms x**2-1
and (x-1)*(x+1), which are semantically equivalent, but not
syntactically.

Jens
• Dear Brian and Jens, I thank you very late for your answers since I had been expecting to receive all potential answers on my email account and have not
Message 1 of 16 , Jun 13, 2008
View Source
Dear Brian and Jens,

receive all potential answers on my email account and have not checked
the list.

I disagree with your remarks (or fail to understand them). First, my
assertion is not, as far as I see, Birkhoff's theorem, but a
modification of it -- to prevent any confusion, I had listed all the
details. Later I have realized that my question can be phrased more
concisely, as follows:

(***) Does Birkhoff completeness still hold if one restricts the class
of models in the notion of semantic deduction (E |= e iff M |= E
implies M |= e for all models M) to only those models having the same
cardinality as the set T(X) of terms (over infinitely many variables)?

(Jens, the reason why I ask for a large enough cardinality of the
fixed support is for hoping for completeness.)

The answer to (***) would be positive if it were true that for any
model M there exists a model M' of the same cardinality as T(X) and
satisfying the same equations as M. In turn, the latter seems true
for non-singleton models M, if one takes M' to be T(X) factored to the
equational theory of M. But is it true that T(X) factored to a set of
equations is either a singleton or has the same cardinality as T(X)?

My not very extensive background in universal algebra prevents me from
clarifying this issues, although I have a feeling that they might be
plain for an expert. So my newly phrased question is (***).

A final word about the motivation behind my question -- a
Birkhoff-like theorem stated in a type theory that does not allow
universal quantification over types; there, one would like to have the
completeness locally, for models having a fixed type as support.

Regards,
Andrei

--- In univalg@yahoogroups.com, "uuomul" <uuomul@...> wrote:
>
> Dear Members,
>
> When trying to switch from a deep to a shallow embedding of a system
> into the rigidly-typed logic of a theorem prover, I discovered that I
> need the following seemingly true proposition about equational logic
> which, if true, is probably known. I kindly ask for confirmation that
> it is true and for some reference and/or hint on how to prove it.
> Here is the proposition (I am
> mentioning the concepts in full detail to prevent any confusion):
>
> Fix an at least countable set Op of operation symbols and a countable
> set Var of variables. Terms T are inductively defined to be either
> variables pairs (f,Ts) with f operation symbol and Ts list of terms.
> An equation is a pair of terms (T,T'). Given a set A, an
> A-environment is a pair (K,L) where K : Op -> (A* -> A) and
> L : Var -> A (where A* is the set of lists with elements in A). Given
> an A-environment (K,L), a term T has a canonical interpretation
> Int(A,K,L,T) as an element of A. An equation (T,T') is said to hold in
> A via (K,L), written holds(A,K,L,T,T'), if
> Int(A,K,L,T) = Int(A,K,L,T'). (T,T')
> is said to hold in A via K, written holds(A,K,T,T'), if
> holds(A,K,L,T,T') for all L : Var -> A.
> Given a set A, a set of equations Eqs and an equation (T,T'),
> Eqs is said to A-deduce semantically (T,T') if
> for all K : Op -> (A^* -> A), (holds(A,K,S,S') for all (S,S') in Eqs)
> implies holds(A,K,T,T').
>
> Proposition: Fix a set A of the same cardinality as Op, a set of
> equations Eqs and an equation (T,T'). Assume Eqs A-deduces
> semantically (T,T'). Then Eqs also deduces (T,T') syntactically,
> i.e., using the standard equational reasoning rules.
>
> (Note: The model A is *fixed* independently of the set of equations
> Eqs, so I cannot assume it to be a term model factored to Eqs.)
>
> Andrei Popescu
>
• I wonder how the Birkhoff completeness theorem complies with Goedel s incompleteness theorem. If we have arithmetic formulas, which are neither provable nor
Message 1 of 16 , Jun 22, 2008
View Source
I wonder how the Birkhoff completeness theorem complies with Goedel's
incompleteness theorem. If we have arithmetic formulas, which are
neither provable nor disprovable, how could an equational based TRS
reduce them and thus prove them? Where can such formulas be found?

Jens
• Jens, As far as I know, Godel s (first) incompleteness theorem implies (or, rather, has as an instance the fact) that the set of first-oder sentences satisfied
Message 1 of 16 , Jun 22, 2008
View Source

Jens,

As far as I know, Godel's (first) incompleteness theorem implies (or, rather, has as an instance the fact) that the set of first-oder sentences satisfied by the algebra of natural numbers with successor, plus and multiplication is not recursively axiomatizable, or equivalently, it is not recursively enumerable.  On the other hand, a completeness theorem (such as Godel's completeness theorem for first-order logic or Birkhoff's theorem for equational logic) says that, for a certain deduction system, the set of (syntactically) deducible sentences using that system includes (and, given soundness, is equal to) that of the semantically deducible sentences.  There is no contradiction between incompleteness in the above sense and completeness in the above sense.  Clearly there exists a set of axioms such that the first-order deduction system is able to deduce from them all true statemens about naturals with successor, addition and multiplication (just take the set of all such statements as axioms!), but Godel's incompleteness theorem says that one cannot find a *recursive* such set.

Regarding the equational part of the theory of naturals with successor,
multiplication and addition, I think it is not only recursively enumerable, but even recursive (decidable), but I might be wrong.

Regards,
Andrei

--- In univalg@yahoogroups.com, "Jens Doll" <jd@...> wrote:
>
> I wonder how the Birkhoff completeness theorem complies with Goedel's
> incompleteness theorem. If we have arithmetic formulas, which are
> neither provable nor disprovable, how could an equational based TRS
> reduce them and thus prove them? Where can such formulas be found?
>
> Jens

• Hello Andrei, consider a grammar G, which generates terms T and also consider equations E out of language L(G), which together with G define a terminating and
Message 1 of 16 , Jun 24, 2008
View Source
Hello Andrei,

consider a grammar G, which generates terms T and also consider
equations E out of language L(G), which together with G define a
terminating and confluent TRS and enable me to reduce each sentence
from L(G) to a normal form N.

What is the normal form N for? I suppose, one could define a set of
equations and a normal form N, so that you can derive from the reduced
sentence, if it belongs to the class of true aritmetic formulas or not.

Jens
• Dear Andrei, ... counterexample: take a signature with countably many constants and uncountably many unary function symbols, and let X be countable. Then
Message 1 of 16 , Jun 25, 2008
View Source
Dear Andrei,

> But is it true that T(X) factored to a set of
> equations is either a singleton or has the same cardinality as T(X)?

counterexample:
take a signature with countably many constants and uncountably many
unary function symbols, and let X be countable. Then clearly T(X) is
uncountable, but T(X) factored by { f(x)=x | f function symbol }
is countable.

This also shows that the usual completeness proof won't work.

All the best,
Till
• Dear Jens, Canonic (i.e., confluent and terminating) TRS s indeed provide a decision procedure for their corresponding equational theories. Yet these
Message 1 of 16 , Jun 25, 2008
View Source
Dear Jens,

Canonic (i.e., confluent and terminating) TRS's indeed provide a
decision procedure for their corresponding equational theories. Yet
these equational theories are not usually complete, but only
ground-complete for the intended model. (I am probably not using
standard terminology here.) For example, take the usual euqations that
define multiplication and addition in terms of 0 and successor:

x + 0 = x
x + S y = S(x + y)
x * 0 = 0
x * S y = x * y + x

This system is confluent and terminating for ground terms (by ground
term I mean term not containing variables), implying
decidability of the ground identities (i.e., of the form t1 = t2 with
t1 and t2 ground terms) which are (syntactic) consequences of that
theory. And, via ground completeness, these identities are the same
as the ones true in the algebra of natural numbers, so we have a
decision procedure for ground identities on natural numbers with 0, S,
+, *.

The same line of reasoning cannot be applied to arbitrary equations
though, because, while the above system if confluent and terminating
on arbitrary terms too, it is not true that the corresponding
equations are enough to deduce syntactically all true equations about
numbers. (E.g., associativity of + does not follow using the
equational deduction system.)

Summing up the above discussion, a canonical TRS of the form you have
in mind does make its own equational theory decidable, but that
equational theory needs not be complete for the intended model.

On the other hand, there are techniques more powerful than TRS
canonicity (about which I know very little) that ensure decidability
of the equational theory of a fixed model, such as that of the
naturals. Your question made me curious and I have searched for the
for the equational theory of naturals -- please find at the link below
an article that I found, containing a positive answer for the case

Best regards,
Andrei

--- In univalg@yahoogroups.com, "Jens Doll" <jd@...> wrote:
>
> Hello Andrei,
>
> consider a grammar G, which generates terms T and also consider
> equations E out of language L(G), which together with G define a
> terminating and confluent TRS and enable me to reduce each sentence
> from L(G) to a normal form N.
>
> What is the normal form N for? I suppose, one could define a set of
> equations and a normal form N, so that you can derive from the reduced
> sentence, if it belongs to the class of true aritmetic formulas or not.
>
> Jens
>
• Dear Till, Many thanks for your answer and it is nice to hear from you! Your example indeed shows that I cannot get away with the classical proof ``up to
Message 1 of 16 , Jun 25, 2008
View Source
Dear Till,

Many thanks for your answer and it is nice to hear from you!

Your example indeed shows that I cannot get away with the classical
proof ``up to isomorphism", using a fixed support. My feeling that
the result is true stubbornly persists though.

Best regards,
Andrei

--- In univalg@yahoogroups.com, Till Mossakowski <till@...> wrote:
>
> Dear Andrei,
>
> > But is it true that T(X) factored to a set of
> > equations is either a singleton or has the same cardinality as T(X)?
>
> counterexample:
> take a signature with countably many constants and uncountably many
> unary function symbols, and let X be countable. Then clearly T(X) is
> uncountable, but T(X) factored by { f(x)=x | f function symbol }
> is countable.
>
> This also shows that the usual completeness proof won't work.
>
> All the best,
> Till
>
• Hello Andrei, thanks for answer and the keywords. I did a search for equational theory on http://citeseer.ist.psu.edu/ and found some seemingly useful
Message 1 of 16 , Jun 28, 2008
View Source
Hello Andrei,

thanks for answer and the keywords. I did a search for "equational
theory" on http://citeseer.ist.psu.edu/ and found some seemingly
useful papers.

Regarding your ground TRS for a set of natural numbers, I now wonder
if we could also define the additive group (N,+,-) by a TRS? All we
would need would be the equations for