[proofplan] We build a model of $S$ in four phases. First, we extend $S$ to a **complete** consistent theory $S_1$ via a Zorn's Lemma argument, so that for every sentence $p$ of $L$, either $S_1 \vdash p$ or $S_1 \vdash \neg p$. Second, we **add Henkin witnesses**: for each sentence of the form $(\exists x)\, q$ in $S_1$, we introduce a fresh constant symbol $c$ and add the witness axiom $q[c/x]$; a finitary argument using existential reasoning shows the extension remains consistent. Third, we **iterate** the completion-plus-witnessing procedure, obtaining nested languages $L \subseteq L_1 \subseteq L_2 \subseteq \cdots$ and theories $\bar S = \bigcup_n S_n$ which is complete, consistent, and has a witness for every existential sentence. Fourth, we construct the **term model** $A$ whose elements are equivalence classes of closed terms modulo provable equality, and prove by induction on sentence complexity that $A \models p$ iff $\bar S \vdash p$ — the existential step is exactly where Henkin witnesses are consumed. [/proofplan]

[step:Extend $S$ to a complete consistent theory $S_1$ via Zorn's Lemma]Let $\mathcal P = \{ T \subseteq L : T \supseteq S \text{ and } T \text{ is consistent}\}$, ordered by inclusion. Then $S \in \mathcal P$, so $\mathcal P$ is non-empty. We verify that every chain $\mathcal C \subseteq \mathcal P$ has an upper bound. Put $T^* = \bigcup_{T \in \mathcal C} T$. Since $S \in T$ for every $T \in \mathcal{C}$, we have $T^* \supseteq S$. If $T^* \vdash \bot$, then since proofs are finite, there exist finitely many sentences $p_1, \dots, p_k \in T^*$ used in the proof, each belonging to some $T_i \in \mathcal C$. Because $\mathcal C$ is totally ordered, one of these $T_i$ contains all $p_j$, hence $T_i \vdash \bot$, contradicting consistency of $T_i$. Thus $T^* \in \mathcal P$ is an upper bound. By Zorn's Lemma, $\mathcal P$ has a maximal element $S_1$. We claim $S_1$ is complete. Suppose, for contradiction, that there exists a sentence $p \in L$ with $S_1 \not\vdash p$ and $S_1 \not\vdash \neg p$. Then both $S_1 \cup \{p\}$ and $S_1 \cup \{\neg p\}$ are consistent: for if $S_1 \cup \{p\} \vdash \bot$, then by the Deduction Theorem $S_1 \vdash \neg p$, contradicting the assumption. Either extension strictly contains $S_1$, contradicting maximality. Hence for every sentence $p$, either $S_1 \vdash p$ or $S_1 \vdash \neg p$.[/step]

[guided]We want to extend $S$ to a consistent theory that decides every sentence. The standard tool is Zorn's Lemma applied to the poset of consistent extensions. Let \begin{align*} \mathcal P = \{ T \subseteq L : T \supseteq S \text{ and } T \text{ is consistent}\}, \end{align*} ordered by set inclusion. Since $S$ itself lies in $\mathcal P$, the poset is non-empty. **Chains have upper bounds.** Let $\mathcal C \subseteq \mathcal P$ be a chain and put $T^* = \bigcup_{T \in \mathcal C} T$. Every $T \in \mathcal{C}$ contains $S$, so $T^* \supseteq S$. Why is $T^*$ consistent? Suppose $T^* \vdash \bot$. A formal proof is a **finite** sequence of formulas, so it uses only finitely many axioms $p_1, \dots, p_k \in T^*$. Each $p_j$ belongs to some $T_{i_j} \in \mathcal C$. Since $\mathcal C$ is totally ordered, the finite subfamily $\{T_{i_1}, \dots, T_{i_k}\}$ has a maximum element $T_i$, which then contains every $p_j$. Thus $T_i \vdash \bot$, contradicting $T_i \in \mathcal P$. This **finitary consistency argument** is used repeatedly in the proof. **Zorn gives a maximal element.** By Zorn's Lemma, $\mathcal P$ has a maximal element, call it $S_1$. **Maximality implies completeness.** Suppose $p$ is a sentence with $S_1 \not\vdash p$ and $S_1 \not\vdash \neg p$. We claim both extensions $S_1 \cup \{p\}$ and $S_1 \cup \{\neg p\}$ are consistent. Indeed, if $S_1 \cup \{p\} \vdash \bot$, the Deduction Theorem gives $S_1 \vdash p \Rightarrow \bot$, i.e., $S_1 \vdash \neg p$, contrary to the hypothesis. So both extensions live in $\mathcal P$ and strictly contain $S_1$, contradicting maximality. Therefore for every sentence $p \in L$, either $S_1 \vdash p$ or $S_1 \vdash \neg p$. This is the completeness of $S_1$.[/guided]

[step:Add Henkin witnesses to obtain $T_1 \subseteq L_1$]Let $E_1 = \{(\exists x)\, q : (\exists x)\, q \in S_1\}$ be the collection of existential sentences provable from $S_1$. For each $(\exists x)\, q \in E_1$ introduce a fresh constant symbol $c_{(\exists x)\, q}$, pairwise distinct and distinct from all constants of $L$. Let $C_1$ be the set of these new constants, and let \begin{align*} L_1 &= L(\Omega \cup C_1, \Pi) \end{align*} be the language obtained by adjoining $C_1$. Put \begin{align*} T_1 &= S_1 \cup \{ q[c_{(\exists x)\, q}/x] : (\exists x)\, q \in E_1 \} \subseteq L_1. \end{align*} We claim $T_1$ is consistent. Suppose $T_1 \vdash \bot$. Any proof of $\bot$ uses only finitely many axioms, so there exist $(\exists x_1)\, q_1, \dots, (\exists x_m)\, q_m \in E_1$ with \begin{align*} S_1 \cup \{ q_1[c_1/x_1], \dots, q_m[c_m/x_m] \} \vdash \bot, \end{align*} where $c_j := c_{(\exists x_j)\, q_j}$. By the Deduction Theorem applied $m$ times, \begin{align*} S_1 \vdash q_1[c_1/x_1] \Rightarrow \big( q_2[c_2/x_2] \Rightarrow \cdots \Rightarrow (q_m[c_m/x_m] \Rightarrow \bot) \cdots \big). \end{align*} Each $c_j$ is a constant of $L_1$ that does not appear in $S_1$ or in the sentences $(\exists x_i)\, q_i$. Therefore, applying the rule of **constant generalisation** (a constant not occurring in the premises may be replaced by a variable and universally quantified) and using the equivalence $(\forall x)(q(x) \Rightarrow \psi) \iff (\exists x)\, q(x) \Rightarrow \psi$ when $x$ does not occur free in $\psi$, we successively eliminate the constants $c_j$ from left to right, each time replacing $q_j[c_j/x_j]$ by $(\exists x_j)\, q_j$ on the left-hand side of the implication. We obtain \begin{align*} S_1 \vdash (\exists x_1)\, q_1 \Rightarrow \big( (\exists x_2)\, q_2 \Rightarrow \cdots \Rightarrow ((\exists x_m)\, q_m \Rightarrow \bot) \cdots \big). \end{align*} But each $(\exists x_j)\, q_j \in S_1$, so repeated modus ponens yields $S_1 \vdash \bot$, contradicting the consistency of $S_1$. Hence $T_1$ is consistent.[/step]

[guided]We now address a major obstacle. Even if $S_1$ is complete, it may not contain "explicit witnesses" for its existential claims: $S_1$ may prove $(\exists x)\, q(x)$ without any particular closed term $t$ such that $S_1 \vdash q(t)$. When we later build a model from closed terms, we will need such witnesses. The fix is to **postulate them**. **Introduce fresh constants.** For each existential sentence $(\exists x)\, q \in S_1$, we introduce a new constant symbol $c_{(\exists x)\, q}$, chosen to be distinct from every constant in $L$ and pairwise distinct. Let $C_1$ denote the set of all such new constants, and let the enlarged language be \begin{align*} L_1 &= L(\Omega \cup C_1, \Pi). \end{align*} **Postulate the witness axioms.** Add to $S_1$ the axiom $q[c_{(\exists x)\, q}/x]$ for each $(\exists x)\, q \in S_1$: \begin{align*} T_1 &= S_1 \cup \{ q[c_{(\exists x)\, q}/x] : (\exists x)\, q \in S_1 \} \subseteq L_1. \end{align*} **Why is $T_1$ consistent?** This is the crux of the step, and it rests on the finiteness of proofs plus a generalisation-on-constants argument. Suppose, for contradiction, $T_1 \vdash \bot$. A proof is finite, so only finitely many of the new witness axioms are actually used: \begin{align*} S_1 \cup \{ q_1[c_1/x_1], \dots, q_m[c_m/x_m] \} \vdash \bot, \end{align*} where $c_j = c_{(\exists x_j)\, q_j}$. Applying the Deduction Theorem $m$ times peels off the axioms one at a time: \begin{align*} S_1 \vdash q_1[c_1/x_1] \Rightarrow \big( q_2[c_2/x_2] \Rightarrow \cdots \Rightarrow (q_m[c_m/x_m] \Rightarrow \bot) \cdots \big). \end{align*} Now comes the key idea: **each $c_j$ is a fresh constant that does not appear in $S_1$ or in any $(\exists x_i)\, q_i$**. The rule of constant generalisation tells us that if a constant $c$ is provably satisfying some property $P(c)$ and $c$ does not occur in the hypotheses, then $(\forall x)\, P(x)$ is provable. Equivalently, we may substitute $c_j$ back by a bound variable. We do this from left to right. At the outermost level the hypothesis is $q_1[c_1/x_1]$. The constant $c_1$ does not occur anywhere else — not in $S_1$ and (because $c_1$ was chosen fresh for $(\exists x_1)\, q_1$) not in $q_2, \dots, q_m$ or the other $c_i$. Generalising on $c_1$ converts $q_1[c_1/x_1] \Rightarrow \psi$ into $(\forall x_1)(q_1 \Rightarrow \psi)$, which, since $x_1$ does not occur free in $\psi$, is equivalent to $(\exists x_1)\, q_1 \Rightarrow \psi$. Iterating for $j = 2, \dots, m$: \begin{align*} S_1 \vdash (\exists x_1)\, q_1 \Rightarrow \big( (\exists x_2)\, q_2 \Rightarrow \cdots \Rightarrow ((\exists x_m)\, q_m \Rightarrow \bot) \cdots \big). \end{align*} **Consume the existential premises.** Each $(\exists x_j)\, q_j$ is an element of $S_1$, so $S_1 \vdash (\exists x_j)\, q_j$. Applying modus ponens $m$ times discharges the premises and yields $S_1 \vdash \bot$. This contradicts the consistency of $S_1$. Therefore $T_1$ is consistent. Note that $T_1$ **may no longer be complete** — new sentences in $L_1$ involving the constants of $C_1$ may be undecided by $T_1$. This is why we must iterate.[/guided]

[step:Iterate the completion-plus-witnessing procedure]We define recursively: given $T_n \subseteq L_n$ consistent, apply Step 1 inside $L_n$ to extend $T_n$ to a complete consistent theory $S_{n+1} \subseteq L_n$, then apply Step 2 to add witnesses for every existential sentence in $S_{n+1}$, obtaining $T_{n+1} \subseteq L_{n+1}$ where $L_{n+1} = L_n(\Omega_n \cup C_{n+1}, \Pi)$. Set $T_0 = S$ and $L_0 = L$. Define \begin{align*} \bar L &= \bigcup_{n \ge 0} L_n, & \bar S &= \bigcup_{n \ge 0} S_n. \end{align*} **$\bar S$ is consistent.** If $\bar S \vdash \bot$, the proof uses finitely many axioms, each lying in some $S_n$. Since $(S_n)$ is an increasing chain, all these axioms lie in a single $S_N$, giving $S_N \vdash \bot$, contradicting Step 1. **$\bar S$ is complete.** Any sentence $p$ of $\bar L$ uses finitely many symbols, hence lies in some $L_N$. Then $p \in L_N$, so by completeness of $S_{N+1}$, either $S_{N+1} \vdash p$ or $S_{N+1} \vdash \neg p$, hence $\bar S \vdash p$ or $\bar S \vdash \neg p$. **$\bar S$ has witnesses.** Let $(\exists x)\, q$ be a sentence of $\bar L$ with $\bar S \vdash (\exists x)\, q$. Then $(\exists x)\, q \in L_N$ for some $N$, and by completeness of $S_{N+1}$, we have $(\exists x)\, q \in S_{N+1}$ (indeed, $\bar S \vdash (\exists x)\, q$ implies $S_{N+1} \not\vdash \neg(\exists x)\, q$ since $\bar S \supseteq S_{N+1}$ is consistent, and completeness of $S_{N+1}$ then forces $S_{N+1} \vdash (\exists x)\, q$). At stage $N+1$, the witnessing step introduced a constant $c \in C_{N+2}$ with $q[c/x] \in T_{N+2} \subseteq S_{N+3} \subseteq \bar S$. Hence $\bar S$ contains a witness for $(\exists x)\, q$.[/step]

[guided]One round of completion followed by witnessing is not enough: witness axioms may contain new existential sentences not yet witnessed, and new sentences in the expanded language may not be decided. We need to iterate. **The recursion.** Set $T_0 = S$, $L_0 = L$. Suppose $T_n \subseteq L_n$ has been defined and is consistent. Apply Step 1 inside $L_n$ to extend $T_n$ to a complete consistent theory $S_{n+1} \subseteq L_n$. Then apply Step 2 to $S_{n+1}$, adding Henkin witnesses to obtain $T_{n+1} \subseteq L_{n+1}$, where $L_{n+1}$ is $L_n$ augmented by fresh constants $C_{n+1}$ indexed by existential sentences of $S_{n+1}$. **The union.** Let \begin{align*} \bar L &= \bigcup_{n \ge 0} L_n, & \bar S &= \bigcup_{n \ge 0} S_n. \end{align*} We now verify three properties. **(a) Consistency of $\bar S$.** Suppose $\bar S \vdash \bot$. The proof uses finitely many sentences $p_1, \dots, p_k \in \bar S$. Each $p_i \in S_{n_i}$ for some $n_i$. Since $S_0 \subseteq S_1 \subseteq S_2 \subseteq \cdots$, setting $N = \max_i n_i$ gives $\{p_1, \dots, p_k\} \subseteq S_N$, hence $S_N \vdash \bot$. This contradicts the consistency of $S_N$ (established at stage $N$ by Step 1 / Step 2). **(b) Completeness of $\bar S$.** Let $p$ be a sentence of $\bar L$. Then $p$ is a finite string in $\bar L$, so it uses only finitely many symbols — in particular, only constants from $C_1 \cup \cdots \cup C_N$ for some $N$. Thus $p \in L_N$. By Step 1 applied at stage $N+1$, $S_{N+1}$ is complete over $L_N$: either $S_{N+1} \vdash p$ or $S_{N+1} \vdash \neg p$. Since $S_{N+1} \subseteq \bar S$, this property ascends to $\bar S$. **(c) Witnesses in $\bar S$.** Suppose $\bar S \vdash (\exists x)\, q$. We want a closed term $t \in \bar L$ (in fact, a constant) such that $\bar S \vdash q[t/x]$. Since $(\exists x)\, q$ uses only finitely many symbols, $(\exists x)\, q \in L_N$ for some $N$. By the completeness of $S_{N+1}$ and the consistency of $\bar S$, we have $(\exists x)\, q \in S_{N+1}$. At stage $N+2$, Step 2 introduces a fresh constant $c \in C_{N+2}$ and adds the axiom $q[c/x]$ to $T_{N+2}$. Since $T_{N+2} \subseteq S_{N+3} \subseteq \bar S$, we conclude $q[c/x] \in \bar S$, so $c$ is our witness. In summary, $\bar S$ is a consistent, complete, Henkin-witnessed theory in the language $\bar L$. We can now build a model.[/guided]

[step:Construct the term model $A$]Let $\mathrm{CT}(\bar L)$ denote the set of closed terms of $\bar L$. Define a relation $\sim$ on $\mathrm{CT}(\bar L)$ by \begin{align*} s \sim t &\iff \bar S \vdash s = t. \end{align*} We verify $\sim$ is an equivalence. Reflexivity follows from the axiom $t = t$, hence $\bar S \vdash t = t$. Symmetry and transitivity follow from the standard equality axioms $(s = t) \Rightarrow (t = s)$ and $(s = t) \wedge (t = u) \Rightarrow (s = u)$, which are part of the predicate calculus; since $\bar S$ is closed under $\vdash$, these rewrites are available. Let $A = \mathrm{CT}(\bar L)/\!\sim$, with typical element $[t]$. For each function symbol $f \in \Omega \cup \bigcup_n C_n$ of arity $k \ge 0$, define \begin{align*} f_A: A^k &\to A \\ ([t_1], \dots, [t_k]) &\mapsto [f(t_1, \dots, t_k)]. \end{align*} This is well-defined: if $t_i \sim t_i'$ for each $i$, then $\bar S \vdash t_i = t_i'$, and the congruence axiom $(t_1 = t_1') \wedge \cdots \wedge (t_k = t_k') \Rightarrow f(t_1, \dots, t_k) = f(t_1', \dots, t_k')$ yields $\bar S \vdash f(t_1, \dots, t_k) = f(t_1', \dots, t_k')$, i.e., $[f(t_1, \dots, t_k)] = [f(t_1', \dots, t_k')]$. For each relation symbol $\phi \in \Pi$ of arity $k$, define \begin{align*} \phi_A &= \{ ([t_1], \dots, [t_k]) \in A^k : \bar S \vdash \phi(t_1, \dots, t_k) \}. \end{align*} Well-definedness follows from the analogous congruence axiom for predicates. Constants (nullary function symbols) are interpreted as their own equivalence classes: if $c \in \Omega \cup \bigcup_n C_n$, then $c_A = [c] \in A$. In particular, since every Henkin witness is a constant in $\bar L$, $A$ is non-empty.[/step]

[guided]Having constructed $\bar S$, we now build a model from the syntactic data: the **Herbrand-style term model**. The underlying set consists of equivalence classes of closed terms. **The equivalence relation.** Two closed terms $s, t$ are deemed equal if $\bar S$ proves them equal: \begin{align*} s \sim t &\iff \bar S \vdash s = t. \end{align*} Why is $\sim$ an equivalence? The axioms of equality in predicate calculus give \begin{align*} \vdash t = t, \qquad \vdash (s = t) \Rightarrow (t = s), \qquad \vdash (s = t) \wedge (t = u) \Rightarrow (s = u). \end{align*} Since $\bar S$ is closed under logical consequence, these deductions lift to $\bar S$-proofs, giving reflexivity, symmetry, and transitivity. **The domain.** Let $A = \mathrm{CT}(\bar L)/\!\sim$ be the set of equivalence classes. Since $\bar L$ contains constants (e.g., every Henkin witness), $\mathrm{CT}(\bar L)$ is non-empty, hence $A$ is non-empty. **Interpreting function symbols.** For $f$ of arity $k$: \begin{align*} f_A: A^k &\to A \\ ([t_1], \dots, [t_k]) &\mapsto [f(t_1, \dots, t_k)]. \end{align*} We must check this is well-defined — that the right-hand side does not depend on the choice of representatives. Suppose $t_i \sim t_i'$ for each $i$, i.e., $\bar S \vdash t_i = t_i'$. The predicate-calculus axiom of **congruence for function symbols** states \begin{align*} \vdash (t_1 = t_1') \wedge \cdots \wedge (t_k = t_k') \Rightarrow f(t_1, \dots, t_k) = f(t_1', \dots, t_k'). \end{align*} Applying modus ponens with the hypotheses, $\bar S \vdash f(t_1, \dots, t_k) = f(t_1', \dots, t_k')$, i.e., $[f(t_1, \dots, t_k)] = [f(t_1', \dots, t_k')]$. For a **constant** $c$ (nullary $f$), we set $c_A = [c]$. **Interpreting relation symbols.** For $\phi$ of arity $k$: \begin{align*} \phi_A &= \{ ([t_1], \dots, [t_k]) \in A^k : \bar S \vdash \phi(t_1, \dots, t_k) \}. \end{align*} Well-definedness uses the congruence axiom for predicates: \begin{align*} \vdash (t_1 = t_1') \wedge \cdots \wedge (t_k = t_k') \Rightarrow (\phi(t_1, \dots, t_k) \iff \phi(t_1', \dots, t_k')). \end{align*} Thus membership of the equivalence-class tuple in $\phi_A$ does not depend on chosen representatives. We now have a full $\bar L$-structure $A$. It remains to show $A$ is a model of $\bar S$ (and hence of $S \subseteq \bar S$).[/guided]

[step:Prove by induction on complexity that $A \models p \iff \bar S \vdash p$]We prove by structural induction on the sentence $p$ of $\bar L$ that \begin{align*} A \models p &\iff \bar S \vdash p. \tag{$\star$} \end{align*} **Atomic sentences.** For closed terms $t_1, \dots, t_k$, \begin{align*} A \models \phi(t_1, \dots, t_k) &\iff ([t_1], \dots, [t_k]) \in \phi_A \iff \bar S \vdash \phi(t_1, \dots, t_k), \end{align*} by the definition of $\phi_A$. The case $\phi(t_1, t_2) = (t_1 = t_2)$ is $A \models t_1 = t_2 \iff [t_1] = [t_2] \iff t_1 \sim t_2 \iff \bar S \vdash t_1 = t_2$. **Negation.** Suppose $(\star)$ holds for $p$. Then \begin{align*} A \models \neg p &\iff A \not\models p \iff \bar S \not\vdash p \iff \bar S \vdash \neg p, \end{align*} where the last equivalence uses completeness and consistency of $\bar S$: if $\bar S \not\vdash p$, completeness forces $\bar S \vdash \neg p$; conversely, if $\bar S \vdash \neg p$ and also $\bar S \vdash p$, then $\bar S \vdash \bot$, contradicting consistency. **Implication.** Suppose $(\star)$ holds for $p$ and $q$. Then \begin{align*} A \models p \Rightarrow q &\iff A \not\models p \text{ or } A \models q \\ &\iff \bar S \not\vdash p \text{ or } \bar S \vdash q \\ &\iff \bar S \vdash \neg p \text{ or } \bar S \vdash q \\ &\iff \bar S \vdash p \Rightarrow q. \end{align*} The third equivalence uses completeness of $\bar S$ as above. For the last: $(\Rightarrow)$ if $\bar S \vdash \neg p$, then $\bar S \vdash p \Rightarrow q$ by the tautology $\neg p \Rightarrow (p \Rightarrow q)$; if $\bar S \vdash q$, then $\bar S \vdash p \Rightarrow q$ by $q \Rightarrow (p \Rightarrow q)$. $(\Leftarrow)$ if $\bar S \vdash p \Rightarrow q$ and $\bar S \not\vdash \neg p$, then by completeness $\bar S \vdash p$, hence by modus ponens $\bar S \vdash q$. **Existential quantifier.** Suppose $(\star)$ holds for every sentence of the form $q[t/x]$, with $t$ a closed term of $\bar L$. We show $(\star)$ for $(\exists x)\, q$. $(\Leftarrow)$ Suppose $\bar S \vdash (\exists x)\, q$. By the witness property of $\bar S$ (Step 3(c)), there exists a constant $c \in \bar L$ with $\bar S \vdash q[c/x]$. By the inductive hypothesis, $A \models q[c/x]$, i.e., the interpretation $c_A = [c]$ satisfies $q$ in $A$. Therefore $A \models (\exists x)\, q$. $(\Rightarrow)$ Suppose $A \models (\exists x)\, q$. Then there exists $[t] \in A$, with $t$ a closed term of $\bar L$, such that $A \models q[t/x]$ (we use the fact that every element of $A$ is of the form $[t]$ for some closed term $t$). By the inductive hypothesis, $\bar S \vdash q[t/x]$. By the predicate-calculus axiom of **existential introduction** $q[t/x] \Rightarrow (\exists x)\, q$, we conclude $\bar S \vdash (\exists x)\, q$. **Universal quantifier.** $(\forall x)\, q$ is logically equivalent to $\neg(\exists x)\, \neg q$; the case follows from the existential and negation cases. **Conclusion.** By $(\star)$, for every $p \in S$, since $\bar S \vdash p$ (as $S \subseteq \bar S$), we have $A \models p$. Thus $A$ is a model of $S$ in the expanded language $\bar L$; by forgetting the interpretations of the fresh constants (i.e., taking the **reduct** to $L$), $A$ becomes a model of $S$ in $L$.[/step]

[guided]The heart of the proof is a single structural induction establishing \begin{align*} A \models p &\iff \bar S \vdash p, \tag{$\star$} \end{align*} for every sentence $p$ of $\bar L$. We handle each connective. **Atomic case.** For relation symbols: \begin{align*} A \models \phi(t_1, \dots, t_k) &\iff ([t_1], \dots, [t_k]) \in \phi_A \iff \bar S \vdash \phi(t_1, \dots, t_k), \end{align*} by the very definition of $\phi_A$ (Step 4). For equality $t_1 = t_2$: \begin{align*} A \models t_1 = t_2 &\iff [t_1] = [t_2] \iff t_1 \sim t_2 \iff \bar S \vdash t_1 = t_2. \end{align*} The base case is purely a matter of unwinding definitions. **Negation.** Assume $(\star)$ for $p$. Then \begin{align*} A \models \neg p \iff A \not\models p \iff \bar S \not\vdash p \iff \bar S \vdash \neg p. \end{align*} The middle equivalence is the inductive hypothesis. The final equivalence is **exactly where completeness and consistency of $\bar S$ are used**: completeness forces one of $\bar S \vdash p$ or $\bar S \vdash \neg p$, and consistency prevents both. Without completeness, the direction $\bar S \not\vdash p \Rightarrow \bar S \vdash \neg p$ would fail, and the whole induction would collapse. **Implication.** Assume $(\star)$ for $p$ and $q$. Unpacking the semantic definition of $\Rightarrow$: \begin{align*} A \models p \Rightarrow q &\iff A \not\models p \text{ or } A \models q \\ &\iff \bar S \not\vdash p \text{ or } \bar S \vdash q \qquad \text{(IH)} \\ &\iff \bar S \vdash \neg p \text{ or } \bar S \vdash q \qquad \text{(completeness + consistency)} \\ &\iff \bar S \vdash p \Rightarrow q. \end{align*} For the final step, we use the tautologies $\vdash \neg p \Rightarrow (p \Rightarrow q)$ and $\vdash q \Rightarrow (p \Rightarrow q)$ in one direction; in the reverse direction, given $\bar S \vdash p \Rightarrow q$ and $\bar S \not\vdash \neg p$, completeness gives $\bar S \vdash p$, and modus ponens yields $\bar S \vdash q$. **Existential quantifier — the crucial case.** Assume $(\star)$ for every $q[t/x]$ with $t$ a closed term. $(\Leftarrow)$: Suppose $\bar S \vdash (\exists x)\, q$. **This is where the witness property earns its keep.** By Step 3(c), there is a constant $c$ of $\bar L$ with $\bar S \vdash q[c/x]$. The inductive hypothesis gives $A \models q[c/x]$. Interpreting $c$ as $c_A = [c] \in A$, we have a witness in $A$, so $A \models (\exists x)\, q$. $(\Rightarrow)$: Suppose $A \models (\exists x)\, q$. By the Tarski definition, some element $a \in A$ satisfies $q$ — that is, $A \models q[a/x]$ under the assignment $x \mapsto a$. **Every element of $A$ is $[t]$ for some closed term $t$ of $\bar L$** — this is how we defined $A$. Unwinding the interpretation, $A \models q[t/x]$. By the inductive hypothesis, $\bar S \vdash q[t/x]$. The predicate calculus has the axiom of existential introduction, $q[t/x] \Rightarrow (\exists x)\, q$, so modus ponens yields $\bar S \vdash (\exists x)\, q$. Note how the forward direction uses that closed terms are dense in $A$ (in fact, exhaust $A$); the backward direction uses the witness property. Without both, the induction fails. **Universal quantifier.** By the equivalence $(\forall x)\, q \iff \neg(\exists x)\, \neg q$, the universal case reduces to the existential and negation cases. **Finishing up.** The induction establishes $(\star)$ for every sentence $p$ of $\bar L$. In particular, for each $p \in S \subseteq \bar S$, we have $\bar S \vdash p$, hence $A \models p$. **Reduct.** The structure $A$ interprets symbols from the expanded language $\bar L$ — in particular, the Henkin constants. To get a model of $S$ in the original language $L$, we take the **reduct** of $A$ to $L$: we forget the interpretations of symbols not in $L$, retaining only those of $\Omega$ and $\Pi$. Since $S \subseteq L$ mentions only symbols of $L$, $A\restriction_L$ still satisfies $S$. This completes the proof: every consistent set of sentences has a model.[/guided]