[proofplan] We build the Henkin extension in stages. At each stage we enumerate all one-variable formulas in the current countable language, add fresh constants for them, and add the corresponding witness axioms. The only substantive point is consistency preservation: adding one fresh witness axiom cannot create a contradiction, because any derivation using the new constant can be converted into a derivation with a fresh variable and then existentially discharged. A finite-subset argument preserves consistency when all witness axioms at a stage are added, and a second finite-subset argument preserves consistency in the union. [/proofplan] [step:Prove that one fresh Henkin witness preserves consistency] Let $M$ be a first-order language, let $S$ be a syntactically consistent $M$-theory, let $\varphi(x)$ be an $M$-formula whose free variables are among $x$, and let $c$ be a constant symbol not in $M$. Define the expanded language $M(c)$ by adjoining $c$ to $M$, and define the $M(c)$-sentence \begin{align*} \theta_c := \exists x\,\varphi(x) \to \varphi(c). \end{align*} We claim that $S \cup \{\theta_c\}$ is syntactically consistent as an $M(c)$-theory. Suppose, for contradiction, that $S \cup \{\theta_c\}$ is inconsistent. Since derivations are finite, there are sentences $\sigma_1,\dots,\sigma_m \in S$ such that \begin{align*} \sigma_1,\dots,\sigma_m,\theta_c \vdash \bot. \end{align*} Choose a variable $y$ which does not occur in this finite derivation and is distinct from $x$. Since $c$ is not in $M$ and occurs only through the new axiom, uniformly replacing $c$ by $y$ throughout the derivation gives \begin{align*} \sigma_1,\dots,\sigma_m,\exists x\,\varphi(x) \to \varphi(y) \vdash \bot. \end{align*} By the [deduction theorem](/theorems/1452) for this finite derivation, \begin{align*} \sigma_1,\dots,\sigma_m \vdash \neg(\exists x\,\varphi(x) \to \varphi(y)). \end{align*} Equivalently, \begin{align*} \sigma_1,\dots,\sigma_m \vdash \exists x\,\varphi(x) \land \neg \varphi(y). \end{align*} Hence \begin{align*} \sigma_1,\dots,\sigma_m \vdash \exists x\,\varphi(x) \end{align*} and \begin{align*} \sigma_1,\dots,\sigma_m \vdash \neg \varphi(y). \end{align*} Because $y$ does not occur free in any $\sigma_i$, universal generalization gives \begin{align*} \sigma_1,\dots,\sigma_m \vdash \forall y\,\neg \varphi(y). \end{align*} Renaming the bound variable $y$ to $x$ gives \begin{align*} \sigma_1,\dots,\sigma_m \vdash \forall x\,\neg \varphi(x). \end{align*} Classical first-order logic proves \begin{align*} \forall x\,\neg \varphi(x) \to \neg \exists x\,\varphi(x), \end{align*} so \begin{align*} \sigma_1,\dots,\sigma_m \vdash \neg \exists x\,\varphi(x). \end{align*} Thus $\sigma_1,\dots,\sigma_m$ derive both $\exists x\,\varphi(x)$ and its negation, contradicting the consistency of $S$. Therefore $S \cup \{\theta_c\}$ is consistent. [guided] The point is to show that the new constant $c$ has no hidden power: since it is fresh, it cannot encode any old information about the theory $S$. Assume toward a contradiction that adding the single witness axiom \begin{align*} \theta_c := \exists x\,\varphi(x) \to \varphi(c) \end{align*} makes the theory inconsistent. A proof of contradiction is finite, so only finitely many old assumptions from $S$ are used. Let those assumptions be $\sigma_1,\dots,\sigma_m \in S$, so that \begin{align*} \sigma_1,\dots,\sigma_m,\theta_c \vdash \bot. \end{align*} Now choose a variable $y$ which is absent from this finite derivation and distinct from $x$. Since $c$ is a new constant symbol, it occurs nowhere in the old sentences $\sigma_1,\dots,\sigma_m$. Therefore we may uniformly replace $c$ by $y$ in the derivation, obtaining \begin{align*} \sigma_1,\dots,\sigma_m,\exists x\,\varphi(x) \to \varphi(y) \vdash \bot. \end{align*} This is the formal version of saying that if the new constant caused a contradiction, then an arbitrary fresh variable would have caused the same contradiction. By the deduction theorem applied to this finite derivation, \begin{align*} \sigma_1,\dots,\sigma_m \vdash \neg(\exists x\,\varphi(x) \to \varphi(y)). \end{align*} In classical logic, the negation of an implication is equivalent to the conjunction of its antecedent and the negation of its consequent. Hence \begin{align*} \sigma_1,\dots,\sigma_m \vdash \exists x\,\varphi(x) \land \neg \varphi(y). \end{align*} Therefore both \begin{align*} \sigma_1,\dots,\sigma_m \vdash \exists x\,\varphi(x) \end{align*} and \begin{align*} \sigma_1,\dots,\sigma_m \vdash \neg \varphi(y) \end{align*} hold. The variable $y$ was chosen fresh, so it does not occur free in any assumption $\sigma_i$. Thus universal generalization is allowed and gives \begin{align*} \sigma_1,\dots,\sigma_m \vdash \forall y\,\neg \varphi(y). \end{align*} Renaming the bound variable $y$ as $x$ gives \begin{align*} \sigma_1,\dots,\sigma_m \vdash \forall x\,\neg \varphi(x). \end{align*} First-order logic proves \begin{align*} \forall x\,\neg \varphi(x) \to \neg \exists x\,\varphi(x), \end{align*} so \begin{align*} \sigma_1,\dots,\sigma_m \vdash \neg \exists x\,\varphi(x). \end{align*} But we already derived $\exists x\,\varphi(x)$ from the same finite set of assumptions. This contradicts the consistency of $S$. Therefore adjoining one fresh Henkin witness axiom preserves consistency. [/guided] [/step] [step:Add all witnesses for one countable language while preserving consistency] Let $M$ be a countable first-order language and let $S$ be a consistent $M$-theory. Since $M$ is countable, the set of $M$-formulas with at most one displayed free variable is countable. Choose an enumeration \begin{align*} (\varphi_k(x))_{k \in \mathbb{N}} \end{align*} of these formulas. Let $(c_k)_{k \in \mathbb{N}}$ be pairwise distinct fresh constant symbols, none belonging to $M$. Define \begin{align*} M^+ := M \cup \{c_k : k \in \mathbb{N}\}. \end{align*} For each $k \in \mathbb{N}$, define the $M^+$-sentence \begin{align*} \theta_k := \exists x\,\varphi_k(x) \to \varphi_k(c_k), \end{align*} and define \begin{align*} S^+ := S \cup \{\theta_k : k \in \mathbb{N}\}. \end{align*} The language $M^+$ is countable because it is the union of the [countable set](/page/Countable%20Set) of symbols of $M$ with the countable set $\{c_k : k \in \mathbb{N}\}$. We prove that $S^+$ is consistent. If $S^+$ were inconsistent, then a finite derivation of contradiction would use only finitely many of the added witness axioms. Thus there would be indices $k_1,\dots,k_r \in \mathbb{N}$ such that \begin{align*} S \cup \{\theta_{k_1},\dots,\theta_{k_r}\} \end{align*} is inconsistent. Order the finitely many indices as written. Starting with the consistent theory $S$, apply the one-witness preservation result successively to $\theta_{k_1},\dots,\theta_{k_r}$. At the $j$-th application, the constant $c_{k_j}$ is fresh relative to the language containing $M$ and the earlier constants $c_{k_1},\dots,c_{k_{j-1}}$, because the constants $(c_k)_{k \in \mathbb{N}}$ are pairwise distinct. Hence each finite extension remains consistent. This contradicts the inconsistency of \begin{align*} S \cup \{\theta_{k_1},\dots,\theta_{k_r}\}. \end{align*} Therefore $S^+$ is consistent. [guided] At this stage we want to add not just one witness, but one witness for every one-variable formula in a fixed countable language $M$. Since $M$ is countable, there are only countably many finite strings of symbols from $M$, and therefore only countably many $M$-formulas. Choose an enumeration \begin{align*} (\varphi_k(x))_{k \in \mathbb{N}} \end{align*} of all $M$-formulas whose free variables are among the displayed variable $x$. For each formula $\varphi_k(x)$, introduce a new constant symbol $c_k$. These constants are chosen pairwise distinct and outside $M$. Define the expanded language \begin{align*} M^+ := M \cup \{c_k : k \in \mathbb{N}\}. \end{align*} This language is countable, because it is obtained from the countable language $M$ by adjoining countably many symbols. For every $k \in \mathbb{N}$, define the witness axiom \begin{align*} \theta_k := \exists x\,\varphi_k(x) \to \varphi_k(c_k). \end{align*} Then define \begin{align*} S^+ := S \cup \{\theta_k : k \in \mathbb{N}\}. \end{align*} Why does consistency survive after adding infinitely many axioms? The reason is finite character of derivability. If $S^+$ were inconsistent, then some finite proof would derive a contradiction from $S^+$. Such a proof can mention only finitely many added witness axioms, so there would be indices $k_1,\dots,k_r$ with \begin{align*} S \cup \{\theta_{k_1},\dots,\theta_{k_r}\} \end{align*} inconsistent. But the previous step says that adding a single fresh witness axiom preserves consistency. Apply that result first to $S$ and $\theta_{k_1}$, then to the resulting theory and $\theta_{k_2}$, and continue through $\theta_{k_r}$. At the $j$-th step, the constant $c_{k_j}$ has not appeared earlier, because all the constants $c_k$ were chosen pairwise distinct. Hence every finite extension \begin{align*} S \cup \{\theta_{k_1},\dots,\theta_{k_j}\} \end{align*} is consistent. Taking $j=r$ contradicts the alleged inconsistency of the finite set of added axioms. Therefore $S^+$ is consistent. [/guided] [/step] [step:Iterate the witness construction through all finite stages] Define languages $(L_n)_{n \in \mathbb{N}_0}$ and theories $(T_n)_{n \in \mathbb{N}_0}$ recursively, where $\mathbb{N}_0 := \{0,1,2,\dots\}$. Set \begin{align*} L_0 := L, \qquad T_0 := T. \end{align*} Assume that $L_n$ is a countable language and $T_n$ is a consistent $L_n$-theory. Apply the one-stage construction to $M := L_n$ and $S := T_n$. This gives a countable language $L_{n+1} \supset L_n$ and a consistent $L_{n+1}$-theory $T_{n+1} \supset T_n$ such that, for every $L_n$-formula $\varphi(x)$ with at most $x$ free, there is a constant symbol $c_{\varphi,n} \in L_{n+1}$ with \begin{align*} \exists x\,\varphi(x) \to \varphi(c_{\varphi,n}) \in T_{n+1}. \end{align*} By induction, every $L_n$ is countable, every $T_n$ is consistent, and \begin{align*} L_0 \subset L_1 \subset L_2 \subset \cdots, \qquad T_0 \subset T_1 \subset T_2 \subset \cdots. \end{align*} [/step] [step:Take the union and verify countability and consistency] Define the language \begin{align*} L^H := \bigcup_{n=0}^{\infty} L_n \end{align*} and the theory \begin{align*} T^H := \bigcup_{n=0}^{\infty} T_n. \end{align*} Since each $L_n$ is countable and the union is indexed by $\mathbb{N}_0$, the language $L^H$ is countable. Also $L = L_0 \subset L^H$ and $T = T_0 \subset T^H$. We prove that $T^H$ is consistent. Suppose, for contradiction, that $T^H$ is inconsistent. Then some finite derivation of contradiction uses only finitely many premises $\tau_1,\dots,\tau_r \in T^H$. For each $j \in \{1,\dots,r\}$, choose $n_j \in \mathbb{N}_0$ such that $\tau_j \in T_{n_j}$. Let \begin{align*} N := \max\{n_1,\dots,n_r\}. \end{align*} Since the theories are increasing, $\tau_1,\dots,\tau_r \in T_N$. Hence $T_N$ is inconsistent, contradicting the construction. Therefore $T^H$ is consistent. [guided] The final language and theory are obtained by taking the union of all finite stages: \begin{align*} L^H := \bigcup_{n=0}^{\infty} L_n, \qquad T^H := \bigcup_{n=0}^{\infty} T_n. \end{align*} The language $L^H$ is countable because it is a [countable union of countable sets](/theorems/755) of symbols. The inclusions $L \subset L^H$ and $T \subset T^H$ hold because $L=L_0$ and $T=T_0$. It remains to check consistency. If $T^H$ were inconsistent, then there would be a finite derivation of contradiction from premises in $T^H$. Let those finitely many premises be \begin{align*} \tau_1,\dots,\tau_r \in T^H. \end{align*} Each premise enters the union at some finite stage, so for each $j \in \{1,\dots,r\}$ there exists $n_j \in \mathbb{N}_0$ such that $\tau_j \in T_{n_j}$. Define \begin{align*} N := \max\{n_1,\dots,n_r\}. \end{align*} Because the theories are increasing, every premise $\tau_j$ belongs to $T_N$. The same finite derivation would therefore show that $T_N$ is inconsistent. This contradicts the inductive construction, which made every $T_N$ consistent. Hence $T^H$ is consistent. [/guided] [/step] [step:Verify the Henkin property for every formula in the final language] Let $\psi(x)$ be an $L^H$-formula whose free variables are among $x$. Since $\psi(x)$ is a finite string of symbols and \begin{align*} L^H = \bigcup_{n=0}^{\infty} L_n, \end{align*} all symbols occurring in $\psi(x)$ already belong to some $L_N$. Thus $\psi(x)$ is an $L_N$-formula. By the construction of $T_{N+1}$, there is a constant symbol $c_{\psi,N} \in L_{N+1} \subset L^H$ such that \begin{align*} \exists x\,\psi(x) \to \psi(c_{\psi,N}) \in T_{N+1} \subset T^H. \end{align*} Therefore $T^H$ contains a Henkin witness axiom for $\psi(x)$. Since $\psi(x)$ was arbitrary, $T^H$ is a Henkin theory in the countable language $L^H$. This completes the construction of a countable consistent Henkin extension of $T$. [/step]