The Henkin Construction: A Step-by-Step Demonstration

An interactive illustration of the proof of Gödel's completeness theorem for first-order predicate calculus.

What's Going On Here

Gödel's completeness theorem states: if a set of formulas \(\Gamma\) is consistent, then it has a model. The proof constructively builds this model in three steps.

Extending the language. For each formula \(\exists x\,\varphi(x)\) we introduce a new "witness" constant \(c\) and the axiom \(\exists x\,\varphi(x) \to \varphi(c)\). Since adding constants generates new existential formulas, the procedure is iterated: \(\mathcal{L}_0 \subseteq \mathcal{L}_1 \subseteq \cdots \subseteq \mathcal{L}_\omega\). These are the Henkin constants.

Lindenbaum's lemma. Enumerate all the closed formulas of the extended language \(\mathcal{L}_\omega\). At each step we add the next formula \(\varphi_k\) to the theory if this creates no contradiction, otherwise we add \(\lnot\varphi_k\). In the end we get a complete consistent set \(\Delta\): for each formula, exactly one of \(\varphi, \lnot\varphi\) lies in \(\Delta\).

The term model. The carrier of the model is the set of equivalence classes of closed terms under \((s \sim t) \iff (s{=}t) \in \Delta\). The predicate \({<}\) is interpreted by definition: \([s] < [t]\) iff \((s{<}t)\in\Delta\). The truth lemma (induction on the formula) guarantees that the model satisfies \(\Gamma\).

This same completeness theorem is why second-order arithmetic, taken as a formal system, stays first-order: its models turn out to be general (Henkin) structures, in which the second sort is an arbitrary family of “sets” rather than the genuine power set \(\mathcal{P}(\mathbb{N})\). What follows from that for \(\mathsf{ACA}_0\), \(\mathsf{Z}_2\) and categoricity is examined in «Hierarchy of Second-Order Arithmetic Theories».

The example on this page. The language \(\mathcal{L} = \{=,\,{<},\,0\}\) with the theory of a linear order and the minimality axiom \(\forall x\,(0{=}x \vee 0{<}x)\). The constant \(0\) gives the first closed term, so the Henkin construction starts right away: already in \(\mathcal{L}_0\) the formula \(\exists x\,(0{<}x)\) makes sense. The slider n controls the number of iterations of the language extension, the slider k — the number of Lindenbaum steps.

↓ Full text of the proof of Gödel's completeness theorem (PDF)

language iteration — \(n\)

\(\mathcal{L}_0 \subseteq \mathcal{L}_1 \subseteq \mathcal{L}_2 \subseteq \mathcal{L}_3 = \mathcal{L}_\omega\)

Lindenbaum step — \(k\)

add the axiom \(\forall x\,\forall y\,\forall z\;(x{=}y \vee y{=}z \vee z{=}x)\)

initial theory \(\Gamma\)

language \(\mathcal{L}_n\)

Henkin axioms \(H\)

CC-set \(\Delta\) — first \(k\) Lindenbaum steps

term model \(\mathfrak{M} = T/{\sim}\)

On the map of mathematical foundations (MathLogic Nexus): Completeness Theorem · Lindenbaum Algebra