= Solution
<Gödel's completeness theorem> for <first-order sentences> says that, in a standard sound first-order <Hilbert calculus>,
$$
\boxed{T\models\sigma\quad\Longrightarrow\quad T\vdash\sigma.}
$$
Equivalently every <first-order consistent> <set> of <first-order sentences> has a <first-order model>: apply this existence statement to $T\cup\{\neg\sigma\}$ for the consequence formulation.
For the <first-order model> existence <formal proof> use a <Henkin construction>. Enlarge the language by fresh <constant symbols> and adjoin <Henkin witness axioms>
$$
\exists x\theta(x)\to\theta(c_\theta).
$$
Freshness of $c_\theta$ preserves <first-order consistency>. In detail, if a contradiction followed after adjoining one witness <axiom>, the <deduction theorem for first-order logic> would yield its <negation>, from which one obtains both $\exists x\theta(x)$ and $\neg\theta(c_\theta)$ over the old theory. Since the new <constant symbol> does not occur in that theory or in $\theta$, replace it by a fresh <logical variable> and generalize to derive $\forall x\neg\theta(x)$, a contradiction. Finitely many witness additions preserve <first-order consistency> successively, and <unions> preserve <first-order consistency> because <formal proofs> are finite. Iterate the enlargement so that <logical formulas> involving newly introduced <constant symbols> also receive witnesses. Include at least one <constant symbol> to guarantee <closed terms>.
Extend the resulting <first-order consistent> <witnessed first-order theory> to a <maximal consistent set of first-order sentences> $H$. In the equality-free case make the domain the <set> of <closed terms>. Interpret <constant symbols> and <function symbols> by their formal <first-order term> constructions; interpret an <atomic formula> by
$$
R(t_1,\ldots,t_n)\text{ holds in the term model}\quad\Longleftrightarrow\quad R(t_1,\ldots,t_n)\in H.
$$
The <truth lemma for a Henkin term model> follows by induction on <logical formulas> with <closed terms> substituted for their <free variables>. The <logical connective> steps use <maximal consistency of a first-order theory>. In the existential step, membership of $\exists x\theta$ supplies a <witness constant> and hence a <first-order term> satisfying $\theta$; conversely a satisfying <closed term> gives the <existential sentence> by an inference of the calculus. The <term model> consequently satisfies $H$ and the original theory. <Equality> is absent here, so distinct <closed terms> may remain distinct domain elements without further identifications.
Back to article page
