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.
1
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.
2
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\).
3
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\).
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.