Notes - Logic MT24, Gödel's completeness theorem



Although similar-sounding to Gödel’s incompleteness theorems, the completeness theorem actually establishes a positive result, namely that any formula entailed by a collection of sentences in a first order language is provable from those sentences (at least in the proof system we are using).

Proof summary

In other words, Gödel’s completeness theorem says that if $\Sigma \models \phi$, then $\Sigma \vdash \phi$. To prove this, we first note that:

  • $\Sigma \models \tau$ if and only if $\Sigma \cup \{\lnot \tau\}$ is unsatisfiable. (1)
  • $\Sigma \cup \{\lnot \tau\}$ is inconsistent if and only if $\Sigma \vdash \tau$. (2)

If we could prove that

  • If $\Sigma \cup \{\lnot \tau\}$ is unsatisfiable, then $\Sigma \cup \{\lnot \tau\}$ is inconsistent, or equivalently
  • If $\Sigma \cup \{\lnot \tau\}$ is consistent, then $\Sigma \cup \{\lnot \tau\}$ is satisfiable.

Then we would bridge the gap between statements $1$ and $2$, and the result would follow. Instead of working with $\Sigma \cup \{\lnot \tau\}$, we just work with any $\mathcal L$-theory $\Sigma$, so need to show:

  • If $\Sigma$ is consistent, then $\Sigma$ is satisfiable.

We break this down as follows:

  • If $\Sigma$ is consistent, $\Sigma$ extends to a complete and ‘witnessing’ $\Sigma’$
    • A theory is witnessing if $\Sigma \vdash \exists x _ i \psi$ and $\exists x _ i \psi$ is a sentence, then there’s some constant symbol $c$ such that $\Sigma \vdash \psi[c/x _ i]$.
    • (For example, Peano arithmetic is not witnessing since $\exists x _ i (x _ i = S(0))$ is true, but $1$ is not a constant symbol).
    • You can prove (in $K(\mathcal L)$) that if $\Sigma$ is not witnessing, you can just add constants from $\mathcal L$ in order to extend to $\Sigma’$.
    • You can also extend to a complete theory in the same way as for the completeness of proofs in propositional logic.
  • If $\Sigma’$ is complete and witnessing, then $\Sigma$ is satisfiable.
    • First it’s shown that $\Sigma’$ is satisfiable (i.e. has a model). This is done by the Henkin construction, which is very similar to the Herbrand construction but where you take equivalence classes of terms that the theory proves equal.
    • Then, since $\Sigma \subseteq \Sigma’$, this is also a model for $\Sigma$. The only slight problem is that $\Sigma’$ and $\Sigma$ are over different languages, but you can show this is actually fine.

Flashcards

@State 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 a $\mathcal L$-theory

@Define what it means for $\Sigma$ to be witnessing.


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

@Prove that if:

  • $\mathcal L$ is a first-order language
  • $\Sigma \subseteq \text{Sent}(\mathcal L)$ is a $\mathcal L$-theory
  • $i \in \mathbb N$
  • $c \in \mathcal L$ is a constant symbol which does not occur in $\phi$, not in any sentence in $\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
  • (@todo, intuitive usefulness?)

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.

@Prove that if:

  • $\mathcal L$ is a first-order language
  • $\Sigma \subseteq \text{Sent}(\mathcal L)$ is a $\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 \{\psi[c/x _ i]\}$ is consistent

We first prove the sub-claim that if

  • $\tau$ is a $\mathcal L$-sentence
  • $\Sigma \cup \{\psi[c/x _ i]\} \vdash \tau$

then:

  • $\Sigma \vdash \tau$

Suppose that

\[\Sigma \cup \\{\psi[c/x_i]\\} \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 \models (\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 a $\mathcal L$-theory
  • $i \in \mathbb N$
  • $c \in \mathcal L$ is a constant symbol which does not occur in $\phi$, not in any sentence in $\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

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)$ (@todo). But then by assumption $\Sigma \vdash \exists x _ i \psi$, so by MP, $\Sigma \vdash \tau$, as required. So the claim follows.


Now returning to the original proposition.

If $\Sigma \cup \{\psi[c/x _ i]\}$ were inconsistent then we would have that for any $\tau$, $\Sigma \cup \{\psi [c/x _ i]\} \vdash \tau$ and $\Sigma \cup \{\psi [c/x _ i]\} \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.

@Prove that if:

  • $\mathcal L$ is a first-order language
  • $\Sigma \subseteq \text{Sent}(\mathcal L)$ is a $\mathcal L$-theory
  • $\Sigma$ is consistent
  • $\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)$

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

\[\text{Sent}(\mathcal L) = \\{\tau_0, \tau_1, \ldots\\}\]

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 \\{\tau_n\\} &\text{if } \Sigma_n \cup \\{\tau_n\\} \text{ is consistent} \\\\ \Sigma_n \cup \\{\lnot \tau_n\\} &\text{otherwise} \end{cases}\]

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

Let $\Sigma$ be a consistent $\mathcal L$-theory and $\tau$ a $\mathcal L$-sentence. Then either $\Sigma \cup \{\tau\}$ is consistent or $\Sigma \cup \{\lnot \tau\}$ 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 \{\psi\}$ (whose existence is ensured by the conditions), and let $\Sigma _ {n+1} := \Sigma _ n’ \cup \{\psi[c/x _ i]\}$. By the result that says

If:

  • $\mathcal L$ is a first-order language
  • $\Sigma \subseteq \text{Sent}(\mathcal L)$ is a $\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 \{\psi[c/x _ i]\}$ 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$.

@State a theorem related to the Henkin construction.


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

@Define what it means for a term in a first-order language $\mathcal L$ to be closed.


It doesn’t contain any variables.

@Prove that every complete witnessing $\mathcal L$-theory $\Sigma$ has a model.


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

This is an equivalence relation by (@todo).

Let $T/E$ be the set of equivalence classes $t/E$ for each $t \in T$.

Define a $\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 := \{(t _ 1 / E, \ldots, t _ k / E) \mid \Sigma \vdash P(t _ 1, \ldots, t _ k)\}$

This is well-defined because (@todo) and $t^\mathcal M = t/E$ for any $t \in T$ by (@todo).

We want to show that $\mathcal M \models \Sigma$. In fact, we show more generally that for any $\sigma \in \text{Sent}(\mathcal L)$

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

We prove this by induction on the number of symbols among $\{\lnot, \to, \forall\}$ in the sentence $\sigma$. Considering cases:

If $\sigma = P(t _ 1, \ldots, t _ k)$: Then since the construction doesn’t depend on the choice of representatives:

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

If $\sigma = t _ 1 \doteq t _ 2$: Then

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

If $\sigma = \lnot \tau$, then

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

If $\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 \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 (@todo):

  • $(\tau \to (\lnot \rho \to \lnot (\tau \to \rho)))$
  • $(\lnot (\tau \to \rho) \to \tau)$
  • $(\lnot (\tau \to \rho) \to \lnot \rho)$

If $\sigma = \forall x _ i \phi$: By the substitution lemma,

\[\mathcal M \models \phi[t/x_i] \iff \mathcal M \models_{a_t} \phi\]

where $a _ t$ is any assignment with $a _ t(x _ i) = t^\mathcal M = t/E$.

Since the domain of $\mathcal M$ is $T/E$, $\mathcal M \models \forall x _ i \phi$ iff for all $t \in T$, $\mathcal M \models \phi[t/x _ i]$.

Now for $t \in T$, $\phi[t/x _ i]$ is a sentence containing fewer symbols among $\{\lnot, \to, \forall \}$ than $\sigma = \forall x _ i \phi$, so by the inductive hypothesis, $\mathcal M \models \phi[t/x _ i]$ iff $\Sigma \vdash \phi[t/x _ i]$.

So to show that $\Sigma \vdash \forall x _ i \phi$ iff $\mathcal M \models \forall x _ i \phi$, it suffices to show that

\[\Sigma \vdash \forall x_i \phi \text{ iff } \text{for all } t \in T, \Sigma \vdash \phi[t/x_i]\]

The forward direction follows from A4 and MP. For the backward direction, note that

\[\\{\forall x_I \lnot\lnot \phi\\} \vdash \forall x_i \phi\]

since by A4, $\{\forall x _ i \lnot \lnot \phi\} \vdash \lnot \lnot \phi$ and then by the tautology $(\lnot \lnot \phi \to \phi)$ and Gen. Now suppose that $\Sigma \not\vdash \forall x _ i \phi$. Then $\Sigma \not\vdash \forall x _ i \lnot \lnot \phi$ by the above.

But then by completeness, $\Sigma \vdash \lnot \forall x _ i \lnot \lnot \phi$, i.e. $\Sigma \vdash \exists x _ i \lnot \phi$. Since $\exists x _ i \lnot \phi$ is a sentence since $\sigma = \forall x _ i \phi$ is.

Since $\Sigma$ is witnessing, $\Sigma \vdash \lnot \phi [c/x _ i]$ for some constant symbol $c$. Since $\Sigma$ is consistent, $\Sigma \not\vdash \phi[c/x _ i]$. Since $c \in T$, it is not the case that for all $t \in T, \Sigma \vdash \phi[t/x _ i]$. So it follows that

\[\Sigma \vdash \forall x_i \phi \text{ iff } \text{for all } t \in T, \Sigma \vdash \phi[t/x_i]\]

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

@State a result about proofs in first-order language $\mathcal L$, but where you’ve added extra constants.


Suppose:

  • $\mathcal L$ is a first-order language
  • $\Sigma \subseteq \text{Sent}(\mathcal L)$ is a $\mathcal L$-theory
  • $\mathcal L’ := \mathcal L \cup \{c _ 0, c _ 1, \ldots\}$ 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 consistent in $K(\mathcal L’)$, then $\Sigma$ is consistent 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.

@Prove that if:

  • $\mathcal L$ is a first-order language
  • $\Sigma \subseteq \text{Sent}(\mathcal L)$ is a $\mathcal L$-theory
  • $\mathcal L’ := \mathcal L \cup \{c _ 0, c _ 1, \ldots\}$
  • $\Sigma \vdash _ {\mathcal L’} \phi$ means that there is a proof of $\phi$ from $\Sigma$ in $K(\mathcal L’)$

then:

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

Claim 1: Since proofs are finite, there is a proof of $\tau$ from $\Sigma$ in $K(\mathcal L \cup \{c _ 1, \ldots, c _ n\})$ 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 a $\mathcal L$-theory
  • $i \in \mathbb N$
  • $c \in \mathcal L$ is a constant symbol which does not occur in $\phi$, not in any sentence in $\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 \{c _ 1, \ldots, c _ {n-1}\})$. 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 \tau$ and $\Sigma \vdash \lnot \tau$ for some $\tau$. But these proofs are also proofs in $K(\mathcal L’)$, and so $\Sigma$ is also inconsistent in $K(\mathcal L’)$.

@Prove that every consistent $\mathcal L$-theory is satisfiable, by appealing to other results.


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 \{c _ 1, c _ 2, \ldots\}$ 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.

@Prove Gödel’s Completeness Theorem, that if:

  • $\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$

(do this by appealing to other results).


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

$\Sigma \models \phi$ iff $\Sigma \cup \{\lnot \phi\}$ is unsatisfiable.

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

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

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

$\Sigma \vdash \phi$ iff $\Sigma \cup \{\lnot \phi\}$ is unsatisfiable.

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

Gödel’s Completeness Theorem states that if:

  • $\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$

Why does it suffice to only prove the case where $\phi$ is a sentence?


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




Related posts