Equational logic

Formal languages are mathematical models of the natural (informal) languages of mathematics (cf. also Formal languages and automata). In mathematical logic (i.e., meta-mathematics) one builds several classes of formal languages, of which first-order logic and equational logic are especially important. Languages of the first class are most often used to give complete mathematical definitions of mathematical theories, their axioms and their rules of proof. Languages of the second class are used most often in universal algebra, and in automatic theorem proving procedures.

An equational language is a formal language whose alphabet consists of a countable set of variables, a set of function symbols and an equality symbol . Moreover, a function is given and for each , denotes the number of argument places of . If , then is called a constant.

One associates with a class of algebras of type , i.e. structures of the form

where is a non-empty set; if , then is a function with arguments running over and with values in ; if , then .

One defines the set of terms of to be the least set of finite sequences of letters of such that contains the one-term sequence consisting of a variable or a constant, and such that if , then . If is an algebra of type and , then denotes a composition of some of the functions and constants , which is coded by . A term of the form , where and , is called atomic.

The only truth-valued expressions of are equations, i.e., sequences of letters of the form

(a1)

where . One says that (a1) is true in if and only if the objects and are equal.

If is a set of equations, then is called a model of if and only if all the equations of are true in . The class of all models of some set is called a variety.

For any and , one denotes by

the term obtained from by substituting all occurrences of by .

The rules of proof of are the following:

i) is accepted for all ;

ii) yields ;

iii) and yield ;

iv) and yield

A set of equations is called an equational theory if and only if is closed under the rules i)–iv). Thus, if is a model of , then is also a model of the least equational theory including .

The above concepts and rules were introduced in 1935 by G. Birkhoff, and he proved the following fundamental theorems.

Birkhoff's completeness theorem: If is an equational theory and is true in all the models of , then belongs to .

Birkhoff's characterization of varieties: A class of algebras of type is a variety if and only if it satisfies the following three conditions:

a) all subalgebras of the algebras of are in ;

b) all homomorphic images of the algebras of are in ;

c) for any subset of , the direct product of the algebras in belongs to .

These theorems are the roots of a very large literature, see [a2], [a4] and references therein.

In mathematical practice, as a rule one uses informal multi-sorted languages (cf. also Logical calculus). Equational logic generalizes in a similar way. For example, a module over a ring is a two-sorted algebra with two universes, an Abelian group and a ring, and its language has two separate sorts of variables for the elements of those universes. Every model of a first-order theory can be regarded as a two-sorted algebra whose universes are the universe of and a two-element Boolean algebra, while treating the relations of as Boolean-valued functions. Corresponding to that view (following [a3]) there is a natural translation of any first-order language into a two-sorted equational language . Namely, the formulas of are treated as Boolean-valued terms of and the terms of are treated as object-valued terms of . The axioms and rules of first-order logic turn into the rules i)–iv) (adapted to the two-sorted language ) plus five axiom schemata:

1) ;

2) ;

3) ;

4) ;

5) . Here run over formulas of , the quantifiers of are understood as abbreviations, viz.

where is an object-valued variable, is an object-valued atomic term, called an -term, whose variables are the free variables of other than , 1)–3) are equational versions of the Łukasiewicz axioms for propositional calculus, 4) yields the proper version of modus ponens, and 5) is the equational version of Hilbert's axiom about the -symbol (which he formulated in 1925).

In this way, the Gödel completeness theorem for first-order logic can be seen as a consequence of Birkhoff's completeness theorem stated above (see [a3]). Moreover, equational logic corroborates a philosophical idea of H. Poincaré about the constructive and finitistic nature of mathematics. The same idea (in the context of set theory) was also expressed by D. Hilbert in 1904. Poincaré died in 1912, before the relevant mathematical concepts described above were developed by T. Skolem in 1920, Hilbert in 1925, and Birkhoff in 1935; see [a2], [a1]. Those concepts allow one to express this idea as follows. Quantifiers may suggest the actual existence of all objects of some infinite universes (a Platonic reality). But the above formalism shows that, at least in pure mathematics, they can be understood in a more concrete way, namely as abbreviations or blueprints for expressions involving certain -terms. And those -terms denote actually imagined objects or operations, thus they do not refer to nor imply the existence of any actually infinite universes. Hence the rules i)–iv) and the axiom schemata 1)–5) are constructive and finitistic in the sense of Poincaré and Hilbert.

Presently (1998), many researchers are trying to apply equational logic to obtain efficient automatic theorem proving procedures (see [a5]).

References

[a1]	J. van Heijenoort, "From Frege to Gödel: A source book in mathematical logic 1878-1931" , Harvard Univ. Press (1977) (Edition: Third, corrected)
[a2]	R.N. McKenzie, G.F. McNulty, W.F. Taylor, "Algebras, lattices, varieties" , I , Wadsworth&Brooks/Cole (1987)
[a3]	J. Mycielski, "Equational treatment of first-order logic" Algebra Univ. , 33 (1995) pp. 26–39
[a4]	W.F. Taylor, "Equational logic" Houston J. Math. (1979) (Survey issue)
[a5]	S.N. Burris, "Logic for mathematics and computer science" , Prentice-Hall (1998)