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.

Symbol	Unicode	Name	Meaning
=	—	Equality	Terms are equal
→	U+2192	Rewrites to	Rewrite step
→*	—	Rewrites to (multi)	Zero or more steps
↔	U+2194	Convertible	Equal in theory
↓	—	Joinable	Share a reduct
⊨	U+22A8	Satisfies	Holds in all models
⊢	U+22A2	Derives	Provable from equations
σ	U+03C3	Substitution	Variable replacement
NF	—	Normal form	Irreducible term

Metatheory. Birkhoff completeness: E ⊢ t = u iff t = u in all algebras satisfying E. Equational logic is decidable for ground terms with finite convergent systems. Undecidable in general (word problem for finitely presented algebras). Term rewriting is Turing-complete. Completion semi-decides the word problem: if equations have a convergent presentation, completion finds it.

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. Not all equational theories have convergent rewrite systems. Completion may not terminate. Rewrite strategies affect efficiency. Equational logic alone has no predicates beyond equality — combining with first-order logic (rewriting modulo theories) is complex. Associative-commutative symbols require special handling (matching is NP-complete).