Completeness of calculii for axiomatically defined classes of algebras

Garrett Birkhoff has shown that the identities of an equationally defined class of algebras are provable from the class, using a very simple calculus all of whose proofs involve no linguistic expressions other than equations. This paper will present analogues of Birkhoff s result for the following two classes of algebras: classes all of whose defining conditions can be given by equations and equation implications, and classes all of whose defining conditions can be given by equations and expressions of the form E A... A E — f E, n > 1, where E ,,..,E , E are equations. Axioms of the forms considered comprise almost all axiom systems used in algebra. Also, an algebraic characterization is given of axiomatically defined classes of algebras which are definable by axioms of the latter form. COMPLETENESS OF CALCULI I FOR AXIOMATICALLY DEFINED CLASSES OF ALGEBRAS by Alan Selman 1, Introduction, Garrett Birkhoff has shown [1, p. 440] that the identities of an equationally defined class of algebras are provable from the equations defining the class, using a very simple calculus all of whose proofs involve no linguistic expressions other than equations. This paper will present analogues of Birkhoff s result for the following two classes of algebras: classes all cf whose defining conditions can be given by equations and equation implications, and classes all of whose defining conditions can be given by equations and expressions of the form E A. . . A E — > E, n > 1, where E , • . . ,E , E are equations. The first of these results answers a question posed by G. Birkhoff in [2, pp. 323-324]. Axioms of the forms considered comprise almost all axiom systems used in algebra. Section 6 at the end of this paper gives an algebraic characterization of axiomatically defined classes of algebras which are definable by axioms of the latter form. In Section 2 a formal system for equation implications is described and the precise statement of our first result (Theorem 1) is given. The proof of Theorem 1 is sketched in Section 4, after key lemmas are presented in Section 3. Our second result (Theorem 2) is stated and proved in Section 5. We have deleted those details of the proof of Theorem 2 which are either straightforward or identical to steps in the proof of Theorem 1. The method of L. Henkin [4] will be used to prove our theorems. As will be seen, the principal difficulty is to avoid the natural use of "long" formulas (implications of nonatomic formulas) in a Henkin type completeness argument. This paper is in part a revised version of results first announced in [9]. Donald Loveland has noted that two of the rules of inference present in [9] are redundant. It has also been pointed out that A. Robinson in [8] has proved completeness of a calculus for a class of languages whose syntax is similar to ours. Also, the author wishes to express his gratitude to Professors Hugo Ribeiro and George Gratzer for suggesting this problem to the author. 2. A Calculus of Equation Implications, We shall consider a class of languages called equation implication languages. For each of these the primitive symbols consist of (1) a denumerably infinite set VR of variables, (2) an arbitrary (possibly empty) set CN of individual constants, (3) a non-empty set FN of function letters, (4) a binary relation symbol, = , (5) the implication sign, ——^ , and (6) grouping symbols, ( , ). With every member of FN is associated some finite rank. The terms of an equation implication language are to be defined inductively in the usual way. The only atomic formulas are the equations, formed by applying = to the terms. The set FL of formulas is defined to be the set of all atomic formulas and expressions E — ^ E , where E and E are atomic formulas. The expressions E — ^ E are the equation implications. If q = p. If E ^ E , and E 3 are equations; p ^ q ^ p ^ q ^ . . . >Pn> a r e terms; BeFL; and feFN has rank n; then the following are rules of inference. (pi) From E2 to infer E —>E ; (p2) From E — ^ E and E ^E to infer E — ^ E ; (p3) From E and E ^ o t o ^-^ o (p4) From B to infer the result of replacing all occurrences of a variable z in B by p; (p5) From E y p = q and E — ^ q = r to infer E 1 >p = r; (p6) From E± ^ px = q1,...,Ej—^pn = q^ to infer = f 3. The Lemmas. An easy induction argument yields the following lemma. Lemma 1. Let AeFL. Let x_,...,x be the collection of — 1 n variables occurring in A, c ,,..,c a collection of individual constants not belonging to CN, £' the extension of •••* ur*j has rank n, then the following are derived rules of inference. (o7) From p = q and q = r to infer p = r; (p8) From p = q,,...,p = q to infer