Terms, Free Algebras and Equational Logic

Equational Logic and the Completeness Theorem

Five rules of inference, and every semantic consequence becomes a derivation. Equational logic is complete, and the proof is the free algebra construction read backwards.

Engineering · Mathematics5 min readKV-MATH-0222

Learning objectives

List the rules of equational logic and apply them to derive an equation.
Distinguish ⊢ from ⊨ and state what completeness asserts.
Prove soundness by induction on derivations.
Outline the completeness proof via the free algebra.
Explain why the deduction theorem fails for equational logic.
Recognise the limits: derivability is not always decidable.

01The formal system

Equational logic derives equations from equations. A derivation is a finite sequence of equations, each an axiom of Σ or obtained from earlier ones by a rule.

The rules of inference
Rule	From	Infer
Reflexivity	—	p ≈ p
Symmetry	p ≈ q	q ≈ p
Transitivity	p ≈ q and q ≈ r	p ≈ r
Congruence (replacement)	p₁ ≈ q₁, …, pₙ ≈ qₙ	f(p₁,…,pₙ) ≈ f(q₁,…,qₙ)
Substitution	p ≈ q	p(σ) ≈ q(σ) for any substitution σ

The first three make derivability an equivalence relation on terms; the congruence rule makes it compatible with the operations, hence a congruence on the term algebra; and substitution makes it fully invariant. Those three observations are the entire structure of the completeness proof.

02Soundness

Every derivable equation is semantically valid: if Σ ⊢ p ≈ q then Σ ⊨ p ≈ q.

ProcedureSoundness by induction on the derivation

in: Σ ⊢ p ≈ q → out: Σ ⊨ p ≈ q

input: derivation of p ≈ q from Σ; algebra A with A ⊨ Σ
base: each axiom of Σ holds in A by hypothesis
reflexivity: p^A = p^A trivially
symmetry and transitivity: equality of functions is an equivalence relation
congruence: if pᵢ^A = qᵢ^A then f^A∘(p⃗^A) = f^A∘(q⃗^A) pointwise
substitution: p^A = q^A as functions means they agree on ALL assignments,
in particular on those factoring through σ
conclude: every line of the derivation holds in A, so A ⊨ p ≈ q

The substitution case is where the implicit universal quantification of identities is used; an identity is a statement about all assignments, not one. Caveat: soundness is the easy half — completeness is the theorem.

Note that substitution is sound precisely because identities are universally quantified. If p ≈ q were an assertion about particular elements, substituting terms for variables would not be justified.

03Completeness

The converse holds: every semantically valid consequence is derivable.

Key resultBirkhoff's completeness theorem for equational logic

Σ ⊢ p ≈ q if and only if Σ ⊨ p ≈ q. Syntactic derivability and semantic consequence coincide exactly for equational reasoning.

Form the derivability relation
Let θ = { ⟨p, q⟩ : Σ ⊢ p ≈ q }. By the first four rules θ is a congruence on the term algebra T(X); by substitution it is fully invariant.
Take the quotient
A := T(X)/θ is an algebra of the type, and by construction A ⊨ Σ, since each axiom of Σ is derivable from Σ.
Test the target equation
Since A ⊨ Σ and Σ ⊨ p ≈ q by hypothesis, A ⊨ p ≈ q. Evaluating at the assignment sending each variable to its own class gives p/θ = q/θ.
Read off derivability
p/θ = q/θ means ⟨p, q⟩ ∈ θ, which is precisely Σ ⊢ p ≈ q.

The quotient T(X)/θ is exactly the free algebra for the variety M(Σ). So the completeness theorem and the free algebra construction are two readings of the same object, and Birkhoff's two theorems are more closely related than their statements suggest.

04Why there is no deduction theorem

Propositional logic has a deduction theorem: if Γ, φ ⊢ ψ then Γ ⊢ φ → ψ. Equational logic has no such thing, because there is no implication in the language.

CautionAdding a hypothesis is not the same as forming an implication

The equational language contains only equations, so an implication between equations is not itself an equation. Statements of the form 'if p ≈ q then r ≈ s' are quasi-identities, and they define quasivarieties rather than varieties. Any argument that silently converts a hypothesis into an implication has left equational logic.

This is why quasivarieties form a genuinely different theory, closed under S, P and ultraproducts but not H, and why the corresponding completeness result requires model-theoretic machinery.

05Decidability of derivability

Completeness says derivability and validity coincide; it does not say either is decidable.

Semidecidable always

Enumerate derivations

Derivations are finite objects over a countable language, so the set of derivable equations is recursively enumerable for any recursively enumerable Σ.

Not decidable in general

Undecidable equational theories exist

There is no algorithm deciding which equations hold in all relation algebras (Tarski), nor for unary algebras (Mal'cev), nor for certain finitely based semigroup varieties.

So the situation mirrors first-order logic: complete, semidecidable, not decidable. Where decidability does hold — for finitely generated discriminator varieties, for instance — it is a substantial theorem rather than a consequence of completeness.

06Term rewriting as a decision procedure

When an equational theory can be presented as a confluent and terminating rewriting system, the word problem becomes decidable by normalisation: rewrite both sides to normal form and compare.

ProcedureDeciding p ≈ q by normalisation

in: p, q and a complete rewriting system → out: decision

input: rewriting system R that is terminating and confluent for the theory
reduce p by R until no rule applies → normal form n(p)
reduce q by R until no rule applies → normal form n(q)
if n(p) and n(q) are the same term: p ≈ q is derivable
otherwise: p ≈ q is not derivable
correctness requires BOTH termination and confluence

Knuth–Bendix completion attempts to turn an arbitrary equational axiom set into such a system, but may fail to terminate — consistent with the undecidability results above. Caveat: orienting equations into rules is a choice, and a bad orientation can destroy termination.

Knuth–Bendix completion and the automated theorem provers built on it are the practical face of equational logic. The sourcing policy page routes to current tools rather than reproducing tables of completed systems.

Frequently asked

Are the five rules independent?

Reflexivity is needed as a base case and cannot be derived. Symmetry and transitivity are independent of one another. The congruence rule is sometimes split into replacement-in-context form, and some presentations combine substitution with the axioms. Presentations differ; what matters is that the derivability relation is a fully invariant congruence on the term algebra.

Why 'fully invariant' rather than just 'congruence'?

Because the substitution rule adds closure under endomorphisms of the term algebra, which is exactly full invariance. A congruence on T(X) that is not fully invariant corresponds to a set of equations closed under the first four rules but not substitution, and does not define a variety.

Does completeness hold for infinitary equational logic?

Not in the same clean form. Allowing infinitely long terms breaks the finiteness of derivations that the enumeration argument relies on, and the correspondence with finitary closure operators and algebraic lattices fails too. Finitariness is load-bearing throughout.

Sources and further reading

S. Burris and H. P. Sankappanavar, A Course in Universal Algebra, Millennium Edition (a corrected re-typesetting of Springer GTM 78, 1981).
G. Grätzer, Universal Algebra, 2nd edition, Springer.
R. McKenzie, G. McNulty and W. Taylor, Algebras, Lattices, Varieties, Volume I.

Original KEVOS® explanatory article. Written from the topic map of the cited works; no text is reproduced from them.