Logic MT24, Gödel's completeness theorem

Suppose:

• $\mathcal L$ is a first-order language
• $\Sigma \subseteq \text{Sent}(\mathcal L)$
• $\phi \in \text{Form}(\mathcal L)$
• $\Sigma \models \phi$

Then:

• $\Sigma \vdash \phi$

Suppose:

• $\mathcal L$ is a first-order language
• $\Sigma \subseteq \text{Sent}(\mathcal L)$ is an $\mathcal L$-theory
• $\mathcal L’ := \mathcal L \cup \lbrace c _ 0, c _ 1, \ldots\rbrace$ where $c _ i$ not in $\mathcal L$

Then:

1. If $\Sigma \vdash _ {\mathcal L’} \tau \in \text{Sent}(\mathcal L)$, then $\Sigma \vdash \tau$
2. If $\Sigma$ is inconsistent in $K(\mathcal L’)$, then $\Sigma$ is inconsistent in $K(\mathcal L)$.

($\Sigma \vdash _ {\mathcal L’} \phi$ means that there is a proof of $\phi$ from $\Sigma$ in $K(\mathcal L’)$). In other words, if you can prove something using the extra constants, you can also prove it without using the extra constants.

Claim 1: Since proofs are finite, there is a proof of $\tau$ from $\Sigma$ in $K(\mathcal L \cup \lbrace c _ 1, \ldots, c _ n\rbrace )$ for some $c _ 1, \ldots, c _ n \in C$. Since $\tau$ is a sentence, $\tau = \tau[c _ n / x _ 0]$ and so by the result that says

If:

• $\mathcal L$ is a first-order language
• $\Sigma \subseteq \text{Sent}(\mathcal L)$ is an $\mathcal L$-theory
• $c \in \mathcal L$ is a constant symbol which does not occur in $\phi$, nor in any sentence of $\Sigma$
• $\Sigma \vdash \phi[c / x _ i]$

Then:

• $\Sigma \vdash \phi$, and
• There is a proof of $\phi$ from $\Sigma$ in which $c$ does not appear

there is a proof of $\tau$ from $\Sigma$ in $K(\mathcal L’)$ in which $c _ n$ does not appear, i.e. a proof in $K(\mathcal L \cup \lbrace c _ 1, \ldots, c _ {n-1}\rbrace )$. Iterating this, we obtain a proof in $K(\mathcal L)$.

Claim 2: Arguing by the contrapositive, if $\Sigma$ is inconsistent in $K(\mathcal L’)$, $\Sigma \vdash _ {\mathcal L’} \tau$ and $\Sigma \vdash \lnot \tau$ for some $\tau$. But then by 1, it follows $\Sigma \vdash _ {\mathcal L} \tau$ and $\Sigma \vdash _ {\mathcal L} \lnot\tau$, hence $\Sigma$ is inconsistent.

For all $\psi \in \text{Form}(\mathcal L)$ such that for all $\exists x _ i \psi \in \text{Sent}(\mathcal L)$ where $\Sigma \vdash \exists x _ i \psi$, there exists some constant symbol $c \in \mathcal L$ such that $\Sigma \vdash \psi[c/x _ i]$.

Overall idea: Let $\alpha _ 1, \ldots, \alpha _ n$ be a proof of $\phi[c / x _ i]$, and show that replacing each occurrence of $c$ in $\alpha _ i$ by a fresh variable $x _ m$ yields a proof $\alpha _ 1’, \ldots, \alpha _ n’$ of $\phi[x _ m/x _ i]$, which by Gen and A4 gives a proof of $\phi[x _ m/x _ i][x _ i/x _ m] = \phi$ as required.

---

Suppose

\[\alpha _ 1, \ldots, \alpha _ n = \phi[c/x _ i]\]

is a proof of $\phi[c/x _ i]$ from $\Sigma$. Suppose $m \in \mathbb N$ such that no $\alpha _ k$ contains $x _ m$.

Let $\alpha _ 1’, \ldots, \alpha _ n’$ be the sequence obtained by replacing in each $\alpha _ k$ each occurrence of $c$ by $x _ m$. We claim that $\alpha _ 1’, \ldots, \alpha _ n’$ is a proof of $\alpha _ n’ = \phi[x _ m / x _ i]$ from $\Sigma$.

Since $c$ doesn’t occur in any formula in $\Sigma$, if $\alpha _ k \in \Sigma$, then $\alpha _ k’ = \alpha _ k \in \Sigma$.

If $\alpha _ k$ is an axiom, then so is $\alpha _ k’$. This is clear for all axiom schemes except A4. For A4, note that if

\[\alpha _ k = (\forall x _ j \phi \to \phi[t/x _ j])\]

then

\[\alpha _ k' = (\forall x _ j \phi' \to \phi'[t'/x _ j])\]

where $\phi’$ and $t’$ are obtained by replacing $c$ with $x _ m$. Here $\phi’[t’/x _ j]$ is defined because $\phi[t/x _ j]$ is defined and the quantifier $\forall x _ m$ does not occur in $\phi’$.

Also, Gen and MP are not affected by the change.

Therefore $\Sigma \vdash \alpha _ n’ = \phi[x _ m / x _ i]$. By Gen, this implies that $\Sigma \vdash \forall x _ m \phi[x _ m /x _ i]$.

Note that

\[(\phi[x _ m / x _ i])[x _ i / x _ m]\]

is defined and equal to $\phi$. The effect of the substitutions is to replace the free occurences of $x _ i$ in $\phi$ with $x _ m$ then revert them to $x _ i$ (which doesn’t create new bound occurrences because only the free occurrences of $x _ i$ were substituted by $x _ m$).

So by A4 with $t = x _ i$ and MP, we obtain $\Sigma \vdash (\phi[x _ m / x _ i])[x _ i / x _ m] = \phi$, and $c$ does not appear in the proof.

We prove the sub-claim that if

• $\tau$ is an $\mathcal L$-sentence
• $\Sigma \cup \lbrace \psi[c/x _ i]\rbrace \vdash \tau$

then:

• $\Sigma \vdash \tau$

This implies the result, since if $\Sigma \cup \lbrace \psi[c/x _ i]\rbrace$ were inconsistent then we would have that for any $\tau$, $\Sigma \cup \lbrace \psi [c/x _ i]\rbrace \vdash \tau$ and $\Sigma \cup \lbrace \psi [c/x _ i]\rbrace \vdash \lnot\tau$. Picking $\tau$ in which $c$ does not occur, it would follow by the claim that $\Sigma \vdash \tau$ and $\Sigma \vdash \lnot \tau$, a contradiction.

---

Suppose that

\[\Sigma \cup \lbrace \psi[c/x _ i]\rbrace \vdash \tau \in \text{Sent}(\mathcal L)\]

and $c$ does not occur in $\tau$. By assumption, $c$ does not occur in $\Sigma$ or $\psi$.

Then $\psi[c/x _ i] \in \text{Sent}(\mathcal L)$. By the deduction theorem,

\[\Sigma \vdash (\psi [c/x _ i] \to \tau)\]

By the result that says

If:

• $\mathcal L$ is a first-order language
• $\Sigma \subseteq \text{Sent}(\mathcal L)$ is an $\mathcal L$-theory
• $c \in \mathcal L$ is a constant symbol which does not occur in $\phi$, nor in any sentence of $\Sigma$
• $\Sigma \vdash \phi[c / x _ i]$

Then:

• $\Sigma \vdash \phi$, and
• There is a proof of $\phi$ from $\Sigma$ in which $c$ does not appear

@ref(ObsJdLA6yA0wxHlCIUoV6d60)

it follows that $\Sigma \vdash (\psi \to \tau)$.

By Gen, $\Sigma \vdash \forall x _ i (\psi \to \tau)$. Then $\Sigma \vdash (\exists x _ i \psi \to \tau)$ because it’s possible to prove in $K(\mathcal L)$:

If:

• $\mathcal L$ is a first-order language
• $\tau \in \text{Sent}(\mathcal L)$
• $\psi \in \text{Form}(\mathcal L)$
• $\text{Free}(\psi) \subseteq \lbrace i\rbrace$

Then:

\[\vdash (\forall x _ i (\psi \to \tau)\to(\exists x _ i \psi \to \tau))\]

@ref(ObspHJLpwtE1MJostD6D57Ae)

But then by assumption $\Sigma \vdash \exists x _ i \psi$, so by MP, $\Sigma \vdash \tau$, as required. Hence the sub-claim claim follows.

Note that $\text{Sent}(\mathcal L)$ is countable, and consider an enumeration

\[\text{Sent}(\mathcal L) = \lbrace \tau _ 0, \tau _ 1, \ldots\rbrace\]

Construct a chain $\Sigma _ i \subseteq \text{Sent}(\mathcal L)$

\[\Sigma = \Sigma _ 0 \subseteq \Sigma _ 1 \subseteq \Sigma _ 2 \subseteq \cdots\]

such that for each $n$:

• $\Sigma _ n$ is consistent
• $\mathcal L$ contains infinitely many constant symbols not appearing in $\Sigma _ n$

Note that $\Sigma _ 0$ satisfies these conditions by assumption.

Now suppose that we are given $\Sigma _ n$ satisfying these conditions, and let

\[\Sigma _ n' := \begin{cases} \Sigma _ n \cup \lbrace \tau _ n\rbrace &\text{if } \Sigma _ n \cup \lbrace \tau _ n\rbrace \text{ is consistent} \\\\ \Sigma _ n \cup \lbrace \lnot \tau _ n\rbrace &\text{otherwise} \end{cases}\]

Then $\Sigma _ n’$ is consistent by the result that says

Let $\Sigma$ be a consistent $\mathcal L$-theory and $\tau$ an $\mathcal L$-sentence. Then either $\Sigma \cup \lbrace \tau\rbrace$ is consistent or $\Sigma \cup \lbrace \lnot \tau\rbrace$ is consistent.

If $\tau _ n$ is not of the form $\exists x _ i \psi$, let $\Sigma _ {n+1} := \Sigma _ n’$ ($\tau _ n$ might already be in the set, but this is okay). We need to handle the case where $\tau _ n = \exists x _ i \psi$ separately to ensure that the theory becomes witnessing.

If $\tau _ n = \exists x _ i \psi \in \Sigma _ n’$, choose a constant symbol $c \in \mathcal L$ which doesn’t occur in any formulas in $\Sigma _ n’ \cup \lbrace \psi\rbrace$ (whose existence is ensured by the conditions), and let $\Sigma _ {n+1} := \Sigma _ n’ \cup \lbrace \psi[c/x _ i]\rbrace$. By the result that says

If:

• $\mathcal L$ is a first-order language
• $\Sigma \subseteq \text{Sent}(\mathcal L)$ is an $\mathcal L$-theory
• $\Sigma$ is consistent
• $\Sigma \vdash \exists x _ i \psi \in \text{Sent}(\mathcal L)$
• $c$ is a constant symbol of $\mathcal L$ which does not occur in $\psi$ nor in any $\sigma \in \Sigma$

Then:

• $\Sigma \cup \lbrace \psi[c/x _ i]\rbrace$ is consistent

it follows that $\Sigma _ {n+1}$ is consistent (note we include both $\exists x _ i \psi$ and $\psi[c/x _ i]$).

Since $\Sigma _ {n+1} \setminus \Sigma _ n$ is finite, $\mathcal L$ contains infinitely many constant symbols not appearing in $\Sigma _ {n+1}$. Therefore $\Sigma _ {n+1}$ meets the two required conditions.

Finally, let

\[\Sigma^\ast := \bigcup _ {n \ge 0} \Sigma _ n\]

Then $\Sigma^\ast$ is consistent since each $\Sigma _ n$ is, and $\Sigma^\ast$ is complete and witnessing by construction, since every sentence appears as some $\tau _ n$.

Every complete witnessing $\mathcal L$-theory $\Sigma$ has a model.

(The Henkin construction gives such a model).

It doesn’t contain any variables.

(“no free variables” is also correct and equivalent, terms do not contain quantifiers so if a variable occurs, it occurs freely).

Let $T$ be the set of all closed $\mathcal L$-terms (i.e. terms containing no variables). Define an equivalence relation $E$ on $T$ by

\[t _ 1 E t _ 2 \iff \Sigma \vdash (t _ 1 \doteq t _ 2)\]

Note that this is an equivalence relation (it is symmetric, reflexive and transitive by considering axioms A6-A8).

Let $T/E$ be the set of equivalence classes $t/E$ for each $t \in T$. Define an $\mathcal L$-structure $\mathcal M$ with domain $T/E$ by:

• $c^\mathcal M := c/E$
• $f^{\mathcal M}(t _ 1 / E, \ldots, t _ k / E) := f(t _ 1, \ldots, t _ k) / E$
• $P^\mathcal M := \lbrace (t _ 1 / E, \ldots, t _ k / E) \mid \Sigma \vdash P(t _ 1, \ldots, t _ k)\rbrace$

This is well-defined because the definitions do not depend on the choice of representatives (i.e. $t _ i / E = t _ i’ / E$, then $f(t _ 1, \ldots, t _ k) / E = f(t _ 1’, \ldots, t’ _ k)/E$, $\Sigma \vdash P(t _ 1, \ldots, t _ k) \iff \Sigma \vdash P(t’ _ 1, \ldots, t’ _ k)$, and $t^\mathcal M = t/E$ for any $t \in T$; this is non-trivial but follows from axioms A4, A8 and induction).

(The Henkin construction). Let $T$ be the set of all closed $\mathcal L$-terms (i.e. terms containing no variables). Define an equivalence relation $E$ on $T$ by

\[t _ 1 E t _ 2 \iff \Sigma \vdash (t _ 1 \doteq t _ 2)\]

Note that this is an equivalence relation (it is symmetric, reflexive and transitive by considering axioms A6-A8; a more detailed justification is given at the end).

Let $T/E$ be the set of equivalence classes $t/E$ for each $t \in T$. Define an $\mathcal L$-structure $\mathcal M$ with domain $T/E$ by:

• $c^\mathcal M := c/E$
• $f^{\mathcal M}(t _ 1 / E, \ldots, t _ k / E) := f(t _ 1, \ldots, t _ k) / E$
• $P^\mathcal M := \lbrace (t _ 1 / E, \ldots, t _ k / E) \mid \Sigma \vdash P(t _ 1, \ldots, t _ k)\rbrace$

This is well-defined because the definitions do not depend on the choice of representatives (i.e. $t _ i / E = t _ i’ / E$, then $f(t _ 1, \ldots, t _ k) / E = f(t _ 1’, \ldots, t’ _ k)/E$, $\Sigma \vdash P(t _ 1, \ldots, t _ k) \iff \Sigma \vdash P(t’ _ 1, \ldots, t’ _ k)$, and $t^\mathcal M = t/E$ for any $t \in T$; this is non-trivial but follows from axioms A4, A8 and induction, a more detailed justification is given at the end).

We aim to show that $\mathcal M \models \Sigma$, i.e. $\mathcal M \models \sigma$ for all $\sigma \in \Sigma$.

---

Claim: For any $\sigma \in \text{Sent}(\mathcal L)$

\[\mathcal M \models \sigma \iff \Sigma \vdash \sigma\]

(and hence in particular, since $\Sigma \vdash \sigma$ immediately when $\sigma \in \Sigma$, $\mathcal M \models \sigma$).

Proof: We prove this by induction on the number of symbols among $\lbrace \lnot, \to, \forall\rbrace$ in the sentence $\sigma$.

Case $\sigma = P(t _ 1, \ldots, t _ k)$:

\[\begin{aligned} \mathcal M \models \sigma &\iff (t _ 1^\mathcal M, \ldots, t _ k^\mathcal M) \in P^\mathcal M \\\\ &\iff (t _ 1 / E, \ldots, t _ k/E) \in P^\mathcal M \\\\ &\iff \Sigma \vdash \sigma \end{aligned}\]

with the middle equivalence following from the fact that the definitions do not depend on the choice of representative.

Case $\sigma = t _ 1 \doteq t _ 2$:

\[\begin{aligned} \mathcal M \models \sigma &\iff t _ 1^\mathcal M = t _ 2^\mathcal M \\\\ &\iff t _ 1 / E = t _ 2 / E \\\\ &\iff t _ 1 E t _ 2 \\\\ &\iff \Sigma \vdash \sigma \end{aligned}\]

Case $\sigma = \lnot \tau$:

\[\begin{aligned} \mathcal M \models \lnot \tau &\iff \mathcal M \not\models \tau &&(\text{def. of} \models) \\\\ &\iff \Sigma \not\vdash \tau &&(\text{by inductive hyp.}) \\\\ &\iff \Sigma \vdash \lnot \tau &&(\Sigma \text{ complete}) \end{aligned}\]

Case $\sigma = (\tau \to \rho)$:

\[\begin{aligned} \mathcal M \models (\tau \to \rho) &\iff \mathcal M \not\models \tau \text{ or } \mathcal M \models \rho &&(\text{def. of} \models) \\\\ &\iff \Sigma \not\vdash \tau \text{ or } \Sigma \vdash \rho &&\text{(by inductive hyp.)} \\\\ &\iff \text{not } (\Sigma \vdash \tau \text{ and } \Sigma \not\vdash \rho) &&\text{(De Morgan's)} \\\\ &\iff \text{not } (\Sigma \vdash \tau \text{ and }\Sigma \vdash \lnot \rho) &&(\Sigma \text{ complete}) \\\\ &\iff \Sigma \not\vdash \lnot (\tau \to \rho) &&\text{(tautology},\star) \\\\ &\iff \Sigma \vdash (\tau \to \rho) &&(\Sigma \text{ complete}) \end{aligned}\]

where the penultimate line $(\star)$ uses the following tautologies:

• For the forward direction:
  • $(\tau \to (\lnot \rho \to \lnot (\tau \to \rho)))$ is a tautology. Then
  • $\text{not }(\Sigma \vdash \tau \text{ and } \Sigma \vdash \lnot \phi)$ implies
  • $\text{not }(\Sigma \vdash \lnot (\tau \to \rho))$ implies
  • $\Sigma \not\vdash (\tau \to \rho)$.
• For the backward direction:
  • $\lnot (\tau \to \rho) \to \tau$ is a tautology, and
  • $\lnot (\tau \to \rho) \to \lnot \rho$ is a tautology. Then
  • $\Sigma \not\vdash (\tau \to \rho)$ implies
  • $\text{not }(\Sigma \vdash \lnot (\tau \to \rho))$ implies
  • $\text{not }(\Sigma \vdash \tau \text{ and } \Sigma \vdash \lnot \rho)$.

Case $\sigma = \forall x _ i \phi$:

\[\begin{aligned} \mathcal M \models \forall x _ i \phi &\iff \forall t/E \in T/E, \mathcal M \models _ {a _ {t/E} } \phi && (\text{where }a _ {t/E}(x _ i) = t/E) \\\\ &\iff \forall t \in T, \mathcal M \models _ {a _ {t/E} } \phi &&(\text{where }a _ {t/E}(x _ i) = t/E) \\\\ &\iff \forall t \in T, \mathcal M \models \phi [t/x _ i] &&(\text{sub. lemma}) \\\\ &\iff \forall t \in T, \Sigma \vdash \phi[t/x _ i] &&(\text{inductive hyp.}) \\\\ &\iff \Sigma \vdash \forall x _ i \phi &&(\ast) \end{aligned}\]

For the backward direction of $(\ast)$: Consider the proof

1. A4: $\forall x _ i \phi \to \phi[t/x _ i]$
2. MP: $\phi [t/x _ i]$

for arbitrary $t$.

For the forward direction of $(\ast)$, we show the contrapositive, i.e. that

\[\Sigma \not\vdash \forall x _ i \phi \implies \exists t \in T \text{ s.t. } \Sigma \not\vdash \phi[t/x _ i]\]

Since $\Sigma$ is complete and witnessing, we have

\[\begin{aligned} \Sigma \not\vdash \forall x _ i \phi &\implies \Sigma \not\vdash \forall x _ i \lnot \lnot \phi &&(\text{otherwise there a short proof of the LHS}) \\\\ &\implies \Sigma \vdash \lnot \forall x _ i \lnot \lnot \phi &&(\text{completeness}) \\\\ &\implies \Sigma \vdash \exists x _ i \lnot \phi &&(\text{def. } \exists) \\\\ &\implies \Sigma \vdash \lnot \phi [c / x _ i] \text{ for some c} &&(\text{witnessing}) \\\\ &\implies \exists t \in T \text{ s.t. } \Sigma \not\vdash \phi[t/x _ i] &&(\text{just rephrasing}) \end{aligned}\]

With this, we have shown $\mathcal M \models \sigma \iff \Sigma \models \sigma$, as required.

---

This covers all cases required for the induction, and hence the overall claim follows.

---

Proof that $E$ is an equivalence relation, and that the definitions do not depend on the choice of representatives:

Symmetry. This amounts to proving $\vdash (t _ 1 \doteq t _ 2 \to t _ 2 \doteq t _ 1)$:

1. A7: $(x _ i \doteq x _ j \to x _ j \doteq x _ i)$
2. Gen1: $\forall x _ i (x _ i \doteq x _ j \to x _ j \doteq x _ i)$
3. Gen2: $\forall x _ j \forall x _ i (x _ i \doteq x _ j \to x _ j \doteq x _ i)$
4. A4: $\forall x _ j \forall x _ i (x _ i \doteq x _ j \to x _ j \doteq x _ i) \to \forall x _ i (x _ i \doteq t _ 2 \to t _ 2 \doteq x _ i)$
5. MP3,4: $\forall x _ i (x _ i \doteq t _ 2 \to t _ 2 \doteq x _ i)$
6. A4: $\forall x _ i (x _ i \doteq t _ 2 \to t _ 2 \doteq x _ i) \to (t _ 1 \doteq t _ 2 \to t _ 2 \doteq t _ 1)$
7. MP5,6: $(t _ 1 \doteq t _ 2 \to t _ 2 \doteq t _ 1)$

Here the general idea is to use Gen and A4 to show that the results which hold for variables hold for terms also.

Transitivity. This amounts to proving $\lbrace t _ 1 \doteq t _ 2, t _ 2 \doteq t _ 3 \rbrace \vdash t _ 1 \doteq t _ 3$. We first show $\lbrace x _ 1 \doteq x _ 2, x _ 2 \doteq x _ 3 \rbrace \vdash x _ 1 \doteq x _ 3$:

1. A8: $x _ 2 \doteq x _ 1 \to (x _ 2 \doteq x _ 3 \to x _ 1 \doteq x _ 3)$
2. A7: $x _ 1 \doteq x _ 2 \to x _ 2 \doteq x _ 1$
3. Hyp: $x _ 1 \doteq x _ 2$
4. MP2,3: $x _ 2 \doteq x _ 1$
5. MP1,4: $x _ 2 \doteq x _ 3 \to x _ 1 \doteq x _ 3$
6. Hyp: $x _ 2 \doteq x _ 3$
7. MP5,6: $x _ 1 \doteq x _ 3$

Then repeated applications of Gen and A4 show the result for terms.

Reflexivity. This amounts to proving $\vdash (t _ 1 \doteq t _ 2)$. This follows similarly to showing symmetry.

Does not depend on the choice of representatives (sketch): Suppose $t _ i$, $t _ i’$ are closed $\mathcal L$-terms such that $\Sigma \vdash t _ i \doteq t _ i’$. We want to show:

• $\Sigma \vdash P(t _ 1, \ldots, t _ k) \iff \Sigma \vdash P(t _ 1’, \ldots, t _ k’)$, and
• $\Sigma \vdash f(t _ 1, \ldots, t _ k) \iff \Sigma \vdash f(t _ 1’, \ldots, t _ k’)$.

Symmetry implies that it suffices to prove just one direction. Consider the versions of the results that just hold for equal variables, and then use Gen, A4 and A8.

For the backward direction of $(\ast)$: Consider the proof

1. A4: $\forall x _ i \phi \to \phi[t/x _ i]$
2. MP: $\phi [t/x _ i]$

for arbitrary $t$.

For the forward direction of $(\ast)$, we show the contrapositive, i.e. that

\[\Sigma \not\vdash \forall x _ i \phi \implies \exists t \in T \text{ s.t. } \Sigma \not\vdash \phi[t/x _ i]\]

Since $\Sigma$ is complete and witnessing, we have

\[\begin{aligned} \Sigma \not\vdash \forall x _ i \phi &\implies \Sigma \not\vdash \forall x _ i \lnot \lnot \phi &&(\text{otherwise there a short proof of the LHS}) \\\\ &\implies \Sigma \vdash \lnot \forall x _ i \lnot \lnot \phi &&(\text{completeness}) \\\\ &\implies \Sigma \vdash \exists x _ i \lnot \phi &&(\text{def. } \exists) \\\\ &\implies \Sigma \vdash \lnot \phi [c / x _ i] \text{ for some c} &&(\text{witnessing}) \\\\ &\implies \exists t \in T \text{ s.t. } \Sigma \not\vdash \phi[t/x _ i] &&(\text{just rephrasing}) \end{aligned}\]

In the proof for the completeness theorem, you first show that if a theory is consistent, it remains consistent even when you add infinitely many constant symbols. So by working over the extended language, you avoid this problem.

Suppose $\Sigma \subseteq \text{Sent}(\mathcal L)$ is consistent in $K(\mathcal L)$.

By the result that says

If $\Sigma$ is consistent in $K(\mathcal L)$, then $\Sigma$ is consistent in $K(\mathcal L’)$ (where $\mathcal L’ = \mathcal L \cup \lbrace c _ 1, c _ 2, \ldots\rbrace$ are constants disjoint from those in $\mathcal L$).

it follows that $\Sigma$ is also consistent in $K(\mathcal L’)$. By the result that says

Let $\Sigma$ be a consistent $\mathcal L$-theory, and suppose $\mathcal L$ contains infinitely many constant symbols not appearing in $\Sigma$. Then $\Sigma$ extends to a complete witnessing $\mathcal L$-theory $\Sigma^\ast \subseteq \text{Sent}(\mathcal L)$.

it follows that $\Sigma$ extends to a complete witnessing set $\Sigma^\ast \subseteq \text{Sent}(\mathcal L’)$. Then by the result which says:

Every complete witnessing $\mathcal L$-theory $\Sigma$ has a model (the Henkin construction).

it follows that $\Sigma^\ast$ is satisfiable. Therefore there exists some $\mathcal L’$-structure $\mathcal M’$ such that $\mathcal M’ \models \Sigma^\ast$, so in particular $\mathcal M’ \models \Sigma$.

Let $\mathcal M$ be the $\mathcal L$-structure obtained from $\mathcal M’$ by forgetting the new constants $C$. Then $\mathcal M \models \Sigma$ as required.

If $\Sigma \models \phi$, then by the result that says

$\Sigma \models \phi$ iff $\Sigma \cup \lbrace \lnot \phi\rbrace$ is unsatisfiable.

it follows that $\Sigma \cup \lbrace \phi\rbrace$ is unsatisfiable. But then by the result that says

Every consistent $\mathcal L$-theory is satisfiable.

it follows that $\Sigma \cup \lbrace \lnot \phi\rbrace$ is inconsistent. But then by the result that says

$\Sigma \vdash \phi$ iff $\Sigma \cup \lbrace \lnot \phi\rbrace$ is inconsistent.

Hence

\[\Sigma \models \phi \implies \Sigma \vdash \phi\]

(A lot of these results assume that $\phi$ is a sentence, but it suffices to consider this case only since if it contains free variables we can consider the sentence $\forall x _ 1 \cdots \forall x _ n \phi$. Then if $\Sigma \models \phi$, then also $\Sigma \models \forall x _ 1 \cdots \forall x _ n \phi$. But then by the result for sentences, $\Sigma \vdash \forall x _ 1 \cdots \forall x _ n \phi$ and then we can conclude $\Sigma \vdash \phi$ by A4 and MP).

If $\phi$ contains free variables we can consider the sentence $\forall^\ast \phi$.

Then if $\Sigma \models \phi$, then also $\Sigma \models \forall^\ast \phi$.

But then by Gödel’s Completeness Theorem for sentences, $\Sigma \vdash \forall^\ast \phi$ and therefore we can conclude $\Sigma \vdash \phi$ by A4 and MP. For reference, A4 says:

A4: $(\forall x _ i \alpha \to \alpha[t/x _ i])$ if $\alpha[t/x _ i]$ is defined

Showing that $\Sigma \models \tau$, which suffices by completeness.