Birkhoff's completeness theorem

Remarks

Soundness, from 1 to 2, holds because each rule of equational logic preserves truth in every algebra. For completeness, let $\theta$ be the set of pairs $(u, v)$ of terms with $\Sigma \vdash u \approx v$. The rules say that $\theta$ is a congruence of the term algebra that is invariant under substitutions, and the quotient of the term algebra by $\theta$ satisfies $\Sigma$. Evaluating $s$ and $t$ in this quotient at the assignment $x \mapsto x/\theta$ gives $s/\theta$ and $t/\theta$, so if $\Sigma \models s \approx t$ then $(s, t) \in \theta$. The quotient is the free algebra on $X$ of the variety defined by $\Sigma$.

Consequence: a set of identities is an equational theory exactly when it contains all identities $t \approx t$ and is closed under the rules of symmetry, transitivity, replacement and substitution.

Going deeper

For a student

This is the equational analogue of Gödel's completeness theorem, with a much simpler set of rules. The proof builds a canonical model: the term algebra divided by provable equality, which is the free algebra of the variety defined by $\Sigma$. Together with Birkhoff's HSP theorem, it sets up the correspondence between varieties of algebras and equational theories. It also justifies term rewriting: a rewriting proof of $s \approx t$ is a derivation in equational logic, and every true consequence has such a derivation, though finding it may be undecidable.