Varieties, Free Algebras and Equational Logic
Equational Logic and the Rules of Deduction
A formal proof system for identities, its five rules, and the completeness theorem matching syntactic derivability with semantic consequence.
Learning objectives
- State the rules of equational deduction
- Derive identities formally in the system
- State Birkhoff's completeness theorem for equational logic
The proof system
Given a set Σ of identities, one writes Σ ⊢ p ≈ q when the identity is derivable from Σ using the following rules.
| Rule | Form | Name |
|---|---|---|
| 1 | p ≈ p | Reflexivity |
| 2 | from p ≈ q infer q ≈ p | Symmetry |
| 3 | from p ≈ q and q ≈ r infer p ≈ r | Transitivity |
| 4 | from pi ≈ qi infer f(p1,…) ≈ f(q1,…) | Replacement / congruence |
| 5 | from p ≈ q infer pσ ≈ qσ for any substitution σ | Substitution |
Rules 1–3 make derivability an equivalence relation on terms; rule 4 makes it a congruence on the term algebra; rule 5 makes that congruence fully invariant.
A worked derivation
Deriving idempotence from absorption in lattice theory
- x ≈ x ∧ (x ∨ y) — this is L4(b)
- Substitute x ∧ x for y: x ≈ x ∧ (x ∨ (x ∧ x)) — by rule 5
- x ∨ (x ∧ x) ≈ x — this is L4(a) with y replaced by x
- Substituting into step 2 using rules 3 and 4: x ≈ x ∧ x
This confirms the remark made earlier that the idempotent laws L3 are derivable from the absorption laws L4, so the standard axiom list for lattices is redundant.
Completeness
Σ ⊢ p ≈ q if and only if Σ ⊧ p ≈ q — that is, the identity is derivable from Σ by the five rules exactly when it holds in every algebra satisfying Σ.
Soundness — the easy direction — is verified rule by rule. Completeness is proved by constructing the free algebra T(X)/⊢Σ, where terms are identified exactly when their equality is derivable. That quotient satisfies Σ, so any identity holding in all models of Σ holds there — which means the terms are identified, which means the identity was derivable.
This is the same argument shape as Birkhoff's HSP theorem: build a free object out of syntax, observe it is a model, and conclude that semantic truth forces syntactic identification. Both theorems are the Galois connection between algebras and identities examined from the two sides.
Equational logic compared to first-order logic
| Equational logic | First-order logic | |
|---|---|---|
| Formulas | Identities p ≈ q only | Arbitrary first-order sentences |
| Rules | Five | More; includes quantifier rules |
| Quantifiers | Implicit universal only | Explicit ∀ and ∃ |
| Completeness | Birkhoff | Gödel |
| Compactness | Holds | Holds |
| Decidability of a theory | Undecidable in general | Undecidable in general |
| Models | Varieties | Elementary classes |
Deciding whether Σ ⊢ p ≈ q for a given finite Σ is the word problem for the variety. It is undecidable in general — a result of Markov and Post for semigroups — even though the proof system has only five rules.
Frequently asked questions
Are the five rules independent?
Reflexivity, symmetry and transitivity are needed to get an equivalence relation; replacement to get a congruence; substitution to get full invariance. Each contributes a distinct closure property, so none is redundant.
Does equational logic have a deduction theorem?
No, because there are no implications in the language. This is one of the ways equational logic is genuinely weaker than first-order logic, and it is why quasi-identities require a different treatment.
Source. S. Burris and H. P. Sankappanavar, A Course in Universal Algebra, The Millennium Edition — a corrected re-typesetting of Springer-Verlag Graduate Texts in Mathematics 78 (1981). Section II.14, book pages 99-105.
This page is an original exposition prepared for the KEVOS® knowledge library. It restates and reorganises mathematical results; it is not a reproduction of the source text.