[proofplan] We prove the contrapositive. Assuming $T \nvdash \varphi$, we show that $T \cup \{\neg \varphi\}$ is syntactically consistent, extend it to a maximally consistent Henkin theory in an expanded language, and build its canonical term model. The truth lemma for the term model shows that every sentence in the maximal theory is true in that model; hence the reduct to the original language satisfies $T$ and satisfies $\neg \varphi$. This gives a countermodel to $T \models \varphi$. [/proofplan]

[step:Pass from non-provability of $\varphi$ to consistency of $T \cup \{\neg \varphi\}$]Let $\mathcal{L}$ be the given first-order language, let $T$ be an $\mathcal{L}$-theory, and let $\varphi$ be an $\mathcal{L}$-sentence. Assume $T \nvdash \varphi$. We first prove that the $\mathcal{L}$-theory \begin{align*} T_0 := T \cup \{\neg \varphi\} \end{align*} is syntactically consistent. If $T_0$ were inconsistent, then for some contradiction sentence $\bot$ one would have \begin{align*} T \cup \{\neg \varphi\} \vdash \bot. \end{align*} By the [deduction theorem](/theorems/1452) for classical first-order logic, this gives \begin{align*} T \vdash \neg \varphi \to \bot. \end{align*} Since classical negation satisfies $\neg \varphi \to \bot \vdash \varphi$, modus ponens and propositional reasoning yield $T \vdash \varphi$, contradicting the assumption. Hence $T_0$ is consistent.[/step]

[guided]The contrapositive begins with the assumption that $\varphi$ is not derivable from $T$. The first task is to turn this proof-theoretic failure into a consistent theory that explicitly asserts the failure of $\varphi$. Define \begin{align*} T_0 := T \cup \{\neg \varphi\}. \end{align*} We claim that $T_0$ is consistent. Suppose instead that $T_0$ is inconsistent. Then there is a contradiction sentence $\bot$ such that \begin{align*} T \cup \{\neg \varphi\} \vdash \bot. \end{align*} The deduction theorem applies because $\neg \varphi$ is a sentence, so no free-variable condition is involved. It gives \begin{align*} T \vdash \neg \varphi \to \bot. \end{align*} In classical logic, the implication $\neg \varphi \to \bot$ is equivalent to $\varphi$. Therefore propositional reasoning inside the proof system gives \begin{align*} T \vdash \varphi. \end{align*} This contradicts $T \nvdash \varphi$. Therefore $T_0$ must be consistent.[/guided]

[step:Add Henkin witnesses while preserving consistency] We construct an expanded language $\mathcal{L}_H$ and a consistent $\mathcal{L}_H$-theory $T_H$ extending $T_0$ with Henkin witnesses. Set $\mathcal{L}_0 := \mathcal{L}$. Recursively, after $\mathcal{L}_n$ has been defined, form $\mathcal{L}_{n+1}$ by adjoining, for every $\mathcal{L}_n$-formula $\psi(x)$ with at most the displayed variable $x$ free, a new constant symbol $c_{\psi,n}$. Let \begin{align*} \mathcal{L}_H := \bigcup_{n=0}^{\infty} \mathcal{L}_n. \end{align*} For every such pair $(\psi,n)$, define the Henkin axiom \begin{align*} h_{\psi,n} := \exists x\,\psi(x) \to \psi(c_{\psi,n}). \end{align*} Let \begin{align*} H := \{h_{\psi,n} : n \in \mathbb{N} \cup \{0\},\ \psi(x) \text{ an } \mathcal{L}_n\text{-formula with at most }x\text{ free}\} \end{align*} and set \begin{align*} T_H := T_0 \cup H. \end{align*} We verify that $T_H$ is consistent. By finiteness of formal derivations, if $T_H$ were inconsistent, then some finite subset $T_0' \subset T_0$ together with finitely many Henkin axioms would be inconsistent. Among all such finite inconsistent sets choose one with the smallest possible number of Henkin axioms, and write its Henkin axioms as \begin{align*} h_1,\dots,h_m. \end{align*} If $m=0$, this contradicts the consistency of $T_0$. Assume $m>0$. Each $h_i$ has the form \begin{align*} h_i = \exists x\,\theta_i(x) \to \theta_i(c_i), \end{align*} where $\theta_i(x)$ is an $\mathcal{L}_{n_i}$-formula with at most $x$ free and $c_i=c_{\theta_i,n_i}$ is the new constant introduced at stage $n_i+1$. Reorder the finite list so that $n_m=\max\{n_1,\dots,n_m\}$. Then $c_m$ does not occur in $T_0' \cup \{h_1,\dots,h_{m-1}\}$. Indeed, $T_0'$ is an $\mathcal{L}$-theory and contains no Henkin constants; if $n_i<n_m$, then $h_i$ is an $\mathcal{L}_{n_i+1}$-sentence and $\mathcal{L}_{n_i+1}\subseteq \mathcal{L}_{n_m}$, while $c_m$ is introduced only when passing from $\mathcal{L}_{n_m}$ to $\mathcal{L}_{n_m+1}$; if $n_i=n_m$, then the formula $\theta_i$ is already an $\mathcal{L}_{n_m}$-formula and the only new constant in $h_i$ is $c_i$, which is distinct from $c_m$ for $i<m$. Write \begin{align*} h_m = \exists x\,\theta(x) \to \theta(c), \end{align*} where $c=c_m$ and $\theta=\theta_m$. By minimality of $m$, the theory \begin{align*} \Gamma := T_0' \cup \{h_1,\dots,h_{m-1}\} \end{align*} is consistent. If $\Gamma \cup \{h_m\}$ were inconsistent, then \begin{align*} \Gamma \vdash \neg h_m. \end{align*} Since $h_m$ is $\exists x\,\theta(x) \to \theta(c)$, classical propositional reasoning yields \begin{align*} \Gamma \vdash \exists x\,\theta(x) \wedge \neg \theta(c). \end{align*} In particular, \begin{align*} \Gamma \vdash \exists x\,\theta(x) \end{align*} and \begin{align*} \Gamma \vdash \neg \theta(c). \end{align*} Because $c$ does not occur in $\Gamma$, the eigenconstant generalization rule for first-order logic applies to the derivation of $\neg\theta(c)$ from $\Gamma$ and gives \begin{align*} \Gamma \vdash \forall x\,\neg \theta(x). \end{align*} By the classical quantifier equivalence between $\forall x\,\neg\theta(x)$ and $\neg\exists x\,\theta(x)$, we obtain \begin{align*} \Gamma \vdash \neg \exists x\,\theta(x). \end{align*} This contradicts both $\Gamma \vdash \exists x\,\theta(x)$ and the consistency of $\Gamma$. Therefore no finite inconsistent subset exists, and $T_H$ is consistent. [/step]

[step:Extend to a maximally consistent Henkin theory]Let $\mathfrak{C}$ be the collection of all consistent $\mathcal{L}_H$-theories $R$ such that \begin{align*} T_H \subset R. \end{align*} Order $\mathfrak{C}$ by inclusion. The set $\mathfrak{C}$ is nonempty because $T_H \in \mathfrak{C}$. If $\mathcal{D} \subset \mathfrak{C}$ is a chain, define \begin{align*} R_{\mathcal{D}} := \bigcup_{R \in \mathcal{D}} R. \end{align*} The theory $R_{\mathcal{D}}$ extends $T_H$. It is consistent: any derivation of a contradiction from $R_{\mathcal{D}}$ uses only finitely many premises, and those premises lie in a single member of the chain $\mathcal{D}$, contradicting that member's consistency. Thus $R_{\mathcal{D}} \in \mathfrak{C}$ and is an upper bound for $\mathcal{D}$. By [Zorn's lemma](/theorems/1226), $\mathfrak{C}$ has a maximal element. Fix such a maximal consistent theory and denote it by $S$. Then $S$ is complete in the syntactic sense: for every $\mathcal{L}_H$-sentence $\sigma$, \begin{align*} \sigma \in S \quad \text{or} \quad \neg \sigma \in S. \end{align*} Indeed, if neither sentence belonged to $S$, then both $S \cup \{\sigma\}$ and $S \cup \{\neg \sigma\}$ would be inconsistent by maximality; applying the deduction theorem to both inconsistencies would give $S \vdash \neg \sigma$ and $S \vdash \sigma$, contradicting consistency. Since $T_H \subset S$, the theory $S$ also has the Henkin property: for every $\mathcal{L}_H$-formula $\psi(x)$ with at most $x$ free, there is a constant symbol $c$ of $\mathcal{L}_H$ such that \begin{align*} \exists x\,\psi(x) \to \psi(c) \in S. \end{align*}[/step]

[guided]We now enlarge the consistent Henkin theory to a theory that makes a decision about every sentence. This maximality is needed later for the truth lemma, especially for Boolean connectives and quantifiers. Let $\mathfrak{C}$ be the set of all consistent $\mathcal{L}_H$-theories $R$ satisfying \begin{align*} T_H \subset R. \end{align*} The order is inclusion. This collection is nonempty because $T_H$ itself is consistent. To apply Zorn's lemma, take a chain $\mathcal{D} \subset \mathfrak{C}$ and define \begin{align*} R_{\mathcal{D}} := \bigcup_{R \in \mathcal{D}} R. \end{align*} The union contains $T_H$. We check consistency. A formal derivation is finite, so if $R_{\mathcal{D}}$ derived a contradiction, only finitely many sentences of $R_{\mathcal{D}}$ would be used as non-logical premises. Since $\mathcal{D}$ is linearly ordered by inclusion, those finitely many premises all lie in one member $R \in \mathcal{D}$. Then $R$ would be inconsistent, contradicting $R \in \mathfrak{C}$. Hence $R_{\mathcal{D}}$ is a consistent upper bound. Zorn's lemma gives a maximal consistent extension $S$ of $T_H$. We next show that maximal consistency implies syntactic completeness. Let $\sigma$ be any $\mathcal{L}_H$-sentence. Suppose neither $\sigma$ nor $\neg \sigma$ belongs to $S$. By maximality, both extensions $S \cup \{\sigma\}$ and $S \cup \{\neg \sigma\}$ are inconsistent. The first inconsistency gives \begin{align*} S \vdash \neg \sigma, \end{align*} and the second gives \begin{align*} S \vdash \sigma. \end{align*} Thus $S$ proves both a sentence and its negation, contradicting consistency. Therefore exactly one of $\sigma$ and $\neg \sigma$ belongs to $S$. Finally, $S$ retains the Henkin property because $T_H \subset S$. Every Henkin axiom introduced during the construction remains a member of $S$.[/guided]

[step:Build the canonical term model of $S$] Let $\operatorname{Term}(\mathcal{L}_H)$ denote the set of closed $\mathcal{L}_H$-terms. Define a binary relation $\sim$ on $\operatorname{Term}(\mathcal{L}_H)$ by \begin{align*} t \sim u \quad \Longleftrightarrow \quad t = u \in S. \end{align*} The equality axioms and rules of first-order logic imply that $\sim$ is an [equivalence relation](/page/Equivalence%20Relation) and is compatible with all function and relation symbols. Define the $\mathcal{L}_H$-structure $\mathcal{M}_S$ as follows. Its underlying set is \begin{align*} |\mathcal{M}_S| := \operatorname{Term}(\mathcal{L}_H)/{\sim}. \end{align*} For a closed term $t$, write $[t]$ for its $\sim$-equivalence class. If $c$ is a constant symbol, define \begin{align*} c^{\mathcal{M}_S} := [c]. \end{align*} If $f$ is an $n$-ary function symbol and $[t_1],\dots,[t_n] \in |\mathcal{M}_S|$, define \begin{align*} f^{\mathcal{M}_S}([t_1],\dots,[t_n]) := [f(t_1,\dots,t_n)]. \end{align*} This is well-defined by compatibility of $\sim$ with function symbols. If $R$ is an $n$-ary relation symbol, define \begin{align*} R^{\mathcal{M}_S}([t_1],\dots,[t_n]) \end{align*} to hold exactly when \begin{align*} R(t_1,\dots,t_n) \in S. \end{align*} This is well-defined by compatibility of $\sim$ with relation symbols. Thus $\mathcal{M}_S$ is an $\mathcal{L}_H$-structure. [/step]

[step:Prove the truth lemma for the canonical term model]We prove the following truth lemma: for every $\mathcal{L}_H$-formula $\alpha(x_1,\dots,x_n)$ whose free variables are among $x_1,\dots,x_n$, and for all closed $\mathcal{L}_H$-terms $t_1,\dots,t_n$, \begin{align*} \mathcal{M}_S \models \alpha([t_1],\dots,[t_n]) \quad \Longleftrightarrow \quad \alpha(t_1,\dots,t_n) \in S. \end{align*} The proof is by induction on the complexity of $\alpha$. For atomic formulas, the assertion is exactly the definition of the interpretations of relation symbols, together with the definition of $\sim$ for equality. The Boolean connectives follow from maximal consistency: for example, \begin{align*} \neg \beta(t_1,\dots,t_n) \in S \quad \Longleftrightarrow \quad \beta(t_1,\dots,t_n) \notin S, \end{align*} and similarly conjunction is governed by the proof-theoretic equivalence between $\beta \wedge \gamma$ and the pair $\beta,\gamma$. It remains to check the existential quantifier. Let $\alpha$ be $\exists y\,\beta(y,x_1,\dots,x_n)$. If \begin{align*} \mathcal{M}_S \models \exists y\,\beta(y,[t_1],\dots,[t_n]), \end{align*} then there is some element $[u] \in |\mathcal{M}_S|$, represented by a closed term $u$, such that \begin{align*} \mathcal{M}_S \models \beta([u],[t_1],\dots,[t_n]). \end{align*} By the induction hypothesis, \begin{align*} \beta(u,t_1,\dots,t_n) \in S. \end{align*} First-order existential introduction gives \begin{align*} S \vdash \exists y\,\beta(y,t_1,\dots,t_n), \end{align*} so maximal consistency and deductive closure give \begin{align*} \exists y\,\beta(y,t_1,\dots,t_n) \in S. \end{align*} Conversely, suppose \begin{align*} \exists y\,\beta(y,t_1,\dots,t_n) \in S. \end{align*} By the Henkin property, there is a constant symbol $c$ such that \begin{align*} \exists y\,\beta(y,t_1,\dots,t_n) \to \beta(c,t_1,\dots,t_n) \in S. \end{align*} Since $S$ is closed under modus ponens, \begin{align*} \beta(c,t_1,\dots,t_n) \in S. \end{align*} By the induction hypothesis, \begin{align*} \mathcal{M}_S \models \beta([c],[t_1],\dots,[t_n]). \end{align*} Therefore \begin{align*} \mathcal{M}_S \models \exists y\,\beta(y,[t_1],\dots,[t_n]). \end{align*} The universal quantifier follows from $\forall y\,\beta$ being classically equivalent to $\neg \exists y\,\neg \beta$. This proves the truth lemma.[/step]

[guided]The truth lemma is the central bridge between syntax and semantics. It says that membership in the maximal theory $S$ is exactly the same as truth in the model built from $S$. We prove: for every $\mathcal{L}_H$-formula $\alpha(x_1,\dots,x_n)$ and closed terms $t_1,\dots,t_n$, \begin{align*} \mathcal{M}_S \models \alpha([t_1],\dots,[t_n]) \quad \Longleftrightarrow \quad \alpha(t_1,\dots,t_n) \in S. \end{align*} The proof is an induction on the complexity of $\alpha$. For atomic formulas, there are two cases. If the atomic formula is equality, then \begin{align*} \mathcal{M}_S \models [t] = [u] \end{align*} means exactly $[t]=[u]$ in the quotient set, which is exactly $t \sim u$, which by definition means \begin{align*} t = u \in S. \end{align*} If the atomic formula is $R(t_1,\dots,t_n)$ for an $n$-ary relation symbol $R$, then the interpretation of $R^{\mathcal{M}_S}$ was defined precisely so that \begin{align*} \mathcal{M}_S \models R([t_1],\dots,[t_n]) \quad \Longleftrightarrow \quad R(t_1,\dots,t_n) \in S. \end{align*} For Boolean connectives, maximal consistency does the work. For negation, syntactic completeness of $S$ gives exactly one of $\beta(t_1,\dots,t_n)$ and $\neg\beta(t_1,\dots,t_n)$ in $S$. Hence \begin{align*} \neg\beta(t_1,\dots,t_n) \in S \quad \Longleftrightarrow \quad \beta(t_1,\dots,t_n) \notin S. \end{align*} By the induction hypothesis, this is equivalent to \begin{align*} \mathcal{M}_S \not\models \beta([t_1],\dots,[t_n]), \end{align*} which is precisely \begin{align*} \mathcal{M}_S \models \neg\beta([t_1],\dots,[t_n]). \end{align*} For conjunction, the proof rules for $\wedge$ give \begin{align*} \beta \wedge \gamma \in S \quad \Longleftrightarrow \quad \beta \in S \text{ and } \gamma \in S, \end{align*} after substituting the displayed closed terms. Applying the induction hypothesis to $\beta$ and $\gamma$ gives the semantic clause for conjunction. The remaining propositional connectives are handled by their classical definitions in terms of $\neg$ and $\wedge$. Now consider the existential case. Let \begin{align*} \alpha(x_1,\dots,x_n) := \exists y\,\beta(y,x_1,\dots,x_n). \end{align*} Suppose first that \begin{align*} \mathcal{M}_S \models \exists y\,\beta(y,[t_1],\dots,[t_n]). \end{align*} By the semantic meaning of $\exists$, some element of $|\mathcal{M}_S|$ witnesses this formula. Every element of $|\mathcal{M}_S|$ is an equivalence class $[u]$ of a closed term $u$, so for some closed term $u$, \begin{align*} \mathcal{M}_S \models \beta([u],[t_1],\dots,[t_n]). \end{align*} The induction hypothesis gives \begin{align*} \beta(u,t_1,\dots,t_n) \in S. \end{align*} By existential introduction in first-order logic, \begin{align*} S \vdash \exists y\,\beta(y,t_1,\dots,t_n). \end{align*} Since a maximal consistent theory is deductively closed, we obtain \begin{align*} \exists y\,\beta(y,t_1,\dots,t_n) \in S. \end{align*} Conversely, suppose \begin{align*} \exists y\,\beta(y,t_1,\dots,t_n) \in S. \end{align*} The Henkin property was designed exactly for this moment: it provides a constant symbol $c$ such that \begin{align*} \exists y\,\beta(y,t_1,\dots,t_n) \to \beta(c,t_1,\dots,t_n) \in S. \end{align*} Using modus ponens inside $S$, we get \begin{align*} \beta(c,t_1,\dots,t_n) \in S. \end{align*} The induction hypothesis then gives \begin{align*} \mathcal{M}_S \models \beta([c],[t_1],\dots,[t_n]). \end{align*} Thus the element $[c] \in |\mathcal{M}_S|$ witnesses the existential statement: \begin{align*} \mathcal{M}_S \models \exists y\,\beta(y,[t_1],\dots,[t_n]). \end{align*} Finally, the universal quantifier follows from the classical equivalence \begin{align*} \forall y\,\beta \quad \Longleftrightarrow \quad \neg \exists y\,\neg \beta. \end{align*} This completes the induction and proves the truth lemma.[/guided]

[step:Extract an original-language countermodel to semantic entailment] Apply the truth lemma to sentences. Since $T_0 \subset T_H \subset S$, every sentence $\tau \in T$ belongs to $S$, and also \begin{align*} \neg \varphi \in S. \end{align*} Therefore \begin{align*} \mathcal{M}_S \models \tau \end{align*} for every $\tau \in T$, and \begin{align*} \mathcal{M}_S \models \neg \varphi. \end{align*} Let $\mathcal{M}$ be the $\mathcal{L}$-reduct of $\mathcal{M}_S$. Because all sentences in $T$ and the sentence $\varphi$ are $\mathcal{L}$-sentences, satisfaction of these sentences is unchanged by passing from $\mathcal{M}_S$ to its $\mathcal{L}$-reduct. Hence \begin{align*} \mathcal{M} \models T \end{align*} and \begin{align*} \mathcal{M} \not\models \varphi. \end{align*} Thus $T \not\models \varphi$. We have proved the contrapositive: \begin{align*} T \nvdash \varphi \quad \Longrightarrow \quad T \not\models \varphi. \end{align*} Therefore, if $T \models \varphi$, then $T \vdash \varphi$. This proves the Gödel Completeness Theorem. [/step]