Equational Logic

Origin. Birkhoff's completeness theorem for equational logic (1935). Term rewriting developed by Knuth and Bendix (1970), providing algorithms for equational reasoning. Foundation for algebraic specification (OBJ, Maude, CafeOBJ) and functional programming. Connects algebra, logic, and computation.

Models. Equations between terms: when are two expressions equal? t = u holds if they denote the same value in all interpretations. Algebras satisfying equations form varieties. Equational reasoning: derive new equations from given ones by substitution and replacement. Term rewriting: orient equations into rules for computation.

Formalism.

Signatures: A set of function symbols with arities.

• Constants: 0, nil, true (arity 0)
• Functions: succ, cons, + (arity 1, 2, 2)

Terms: Built from variables and function symbols.

• Variables: x, y, z
• If f has arity n and t₁,...,tₙ are terms, so is f(t₁,...,tₙ)

Equations: t = u where t, u are terms (possibly with variables). Examples:

• x + 0 = x
• x + succ(y) = succ(x + y)
• reverse(reverse(xs)) = xs

Equational theory: A set E of equations. An algebra A satisfies E if all equations hold under all variable assignments.

Inference rules (Birkhoff):

• Reflexivity: t = t
• Symmetry: t = u ⟹ u = t
• Transitivity: t = u, u = v ⟹ t = v
• Congruence: t₁ = u₁, ..., tₙ = uₙ ⟹ f(t₁,...,tₙ) = f(u₁,...,uₙ)
• Substitution: t = u ⟹ tσ = uσ (for any substitution σ)

Term rewriting: Orient equations as rules l → r. Rewrite t to u if a subterm matches l and is replaced by r. Termination: no infinite rewrite sequences. Confluence: if t →* u and t →* v, then u →* w and v →* w for some w. Terminating + confluent = unique normal forms = decidable equality.

Knuth-Bendix completion: Given equations, attempt to produce a terminating, confluent rewrite system. May fail, succeed, or run forever.

Symbols.

Metatheory. Birkhoff (1935) proved both halves of the subject. Completeness: E ⊢ t = u exactly when t = u holds in every algebra satisfying E, so the five rules are all the equational reasoning there is. The HSP theorem: a class of algebras is axiomatizable by equations exactly when it is closed under homomorphic images, subalgebras and direct products. Decidability is a different matter — Post and Markov independently proved in 1947 that the word problem for finitely presented semigroups is undecidable, so equality in a finitely axiomatized equational theory is undecidable in general. Rewriting supplies the partial method. Newman's lemma (1942): a terminating relation is confluent iff it is locally confluent. The Knuth–Bendix critical pair lemma (1970): a terminating rewrite system is confluent iff all of its finitely many critical pairs are joinable, so confluence is decidable once termination is known. Termination itself is undecidable, and Dauchet (1989) showed this already for single-rule systems.

Applies to. Algebraic specification languages. Functional programming (Haskell's equational reasoning). Theorem proving (superposition, paramodulation). Compiler optimization (rewriting). Protocol verification (Maude). Abstract data types.

Limitations. Birkhoff completeness is about all models, and the model that usually matters is the initial one: properties true in the initial algebra but requiring induction, such as commutativity of the Peano definition of addition, are not equational consequences of the defining equations, so the logic proves strictly less than the intended semantics asserts. The language has no negation, no implication and no predicate but equality, so disequalities and case distinctions are inexpressible; conditional equations move to quasivarieties, where the HSP characterization no longer holds. Not every theory has a convergent rewrite system, completion may diverge, and no procedure decides in advance which will happen. Permutative axioms such as commutativity cannot be oriented at all, forcing rewriting modulo them, and associative-commutative matching is NP-complete.

© 2026 Lingenic LLC