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]$.

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 offences 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 \notin \Sigma’ _ n$, or if $\tau _ n$ is not of the form $\exists x _ i \psi$, let $\Sigma _ {n+1} := \Sigma _ n’$.

Otherwise 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.

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).

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).

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)} \\\\ &\iff \Sigma \vdash (\tau \to \rho) &&(\Sigma \text{ complete}) \end{aligned}\]

where the penultimate line uses the following tautologies:

• For the forward direction: $(\tau \to (\lnot \rho \to \lnot (\tau \to \rho)))$
• For the backward direction:
  • $\lnot (\tau \to \rho) \to \tau$
  • $\lnot (\tau \to \rho) \to \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.

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}\]

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.