Gödel's second incompleteness theorem

1. Introduction

The first incompleteness theorem (and the Gödel-Rosser theorem which came a bit later) show that sufficiently strong recursive theories of arithmetic are necessarily incomplete. They do not quite settle the most pressing foundational question that was around at 1931, which is whether a theory of arithmetic can establish the consistency of a stronger and more useful theory for mathematics. Gödel's second incompleteness theorem establishes a negative answer to this question. In fact it says that a consistent theory of arithmetic $T$ cannot even prove its own consistency, $Con (T)$ .

2. The second theorem as a formalisation of the first

One part of the first incompleteness theorem gives, for each recursive theory $T$ extending $DOR$ , a statement $G$ equivalent to $\forall x \neg {Proof}_{T} (x, ⌜G⌝)$ , and the first part of the argument shows that, assuming $T$ is consistent, $T ⊬ G$ , to which we can step outside $T$ momentarily and conclude that $G$ must actually be true because $T$ really cannot prove it.

There's a lot that has been made about this argument, to wit that $T$ cannot know that $G$ is true but we can see that $G$ is in fact true and therefore we are in some sense cleverer than $T$ . (The Lucas argument against artificial intelligence, for example.) Much of what has been said doesn't bear too close scrutiny because ultimately it depends on us knowing that the hypotheses of the Gödel first theorem are true, and the most tricky hypothesis that we need to know is that $T$ is consistent. Gödel realised this and in fact this is how he originally stated his second incompleteness theorem: a sufficiently strong theory $T$ can formalise the argument just given and prove $Con (T) \to G$ . Since $T ⊬ G$ , Gödel concludes that $T ⊬ Con (T)$ .

It's worth looking at this argument in a bit more detail, because it is illuminating and indicates what we expect such theories $T$ to be able to do, and of course it is essential if we are to say what we mean by sufficiently strong. We start with our recursive theory $T$ extending $DOR$ , our predicate ${Proof}_{T} (x, y)$ , and our sentence $G$ equivalent (in $DOR$ ) to $\forall x \neg {Proof}_{T} (x, ⌜G⌝)$ . We also write $Con (T)$ for $\forall x \neg {Proof}_{T} (x, ⌜⊥⌝)$ . We attempt to prove $Con (T) \to G$ in $T$ so we take an arbitrary model $M ⊨ T + \neg G$ and attempt to show $M ⊨ \neg Con (T)$ .

We have from $M ⊨ \neg G$ that $M ⊨ \exists x {Proof}_{T} (x, ⌜G⌝)$ . This statement true in $M$ is a $Σ_{1}$ statement.
Any $Σ_{1}$ statement true in the real world is provable in $DOR$ . But this is a statement about provability and hence (via Gödel-numbering) a statement of arithmetic. When written as a statement of arithmetic it is the assertion that $σ \to \exists x {Proof}_{DOR} (x, ⌜σ⌝)$ for each $Σ_{1}$ sentence $σ$ . That $T$ proves all such assertions is a reasonable assumption to make as part of what we mean by $T$ is sufficiently strong..
Suppose $T$ is strong enough to prove the assertion that all true $Σ_{1}$ sentences are provable, as in the previous paragraph. Then we can apply this in $M$ to the Gödel statement $\neg G$ in the paragraph before it, since $M ⊨ \neg G$ and $\neg G$ is $Σ_{1}$ . We conclude that $M ⊨ \exists y {Proof}_{T} (y, ⌜\neg G⌝)$ .
But then $M$ contains proofs of both $G$ and $\neg G$ . These proofs could be combined to obtain a single proof of $⊥$ , a proof that is an element of $M$ . In other words, $M ⊨ \exists y {Proof}_{T} (y, ⌜⊥⌝)$ or $M ⊨ \neg Con (T)$ .
Since we have concluded that $M ⊨ \neg Con (T)$ and $M$ was arbitrary model of $T + \neg G$ , it follows by Completeness that $T ⊢ \neg G \to \neg Con (T)$ , as required.

There are some small details left out here, to do with how $T$ and $M$ can manipulate logic and proofs, in particular the logic of $\to$ , $\neg$ and $⊥$ . These details are filled in in the next section.

3. Provability predicates

There is a more modern axiomatic treatment of the Gödel second incompleteness theorem that is basically the same as just given, but identifies exactly what it is about the logic and provability that is required for it to work.

Definition.

Suppose $T$ is a theory extending $DOR$ . A first order formula $Prov (x)$ in the language of $DOR$ with single free-variable $x$ is called a provability predicate for $T$ if the following hold for all sentences $σ, τ$ in the language of $T$ :

if $T ⊢ σ$ then $T ⊢ Prov (⌜σ⌝)$ ;
$T ⊢ Prov (⌜σ \to τ⌝) \to (Prov (⌜σ⌝) \to Prov (⌜τ⌝))$ ;
$T ⊢ Prov (⌜σ⌝) \to Prov (⌜Prov (⌜σ⌝)⌝)$ .

The first of these clauses connects $Prov (⌜σ⌝)$ to provability; the second provides all the basic logic needed and the third indicates that provability when true is computationally easily checkable hence provably true.

Definition.

If a provability predicate $Prov (x)$ is given for a theory $T$ then $Con (T)$ is $\neg Prov (⌜⊥⌝)$ .

Theorem.

Suppose $T$ is a consistent theory extending $DOR$ with a provability predicate $Prov (x)$ . Then $T ⊬ Con (T)$ .

Proof.

By diagonalisation let $G$ satisfy $DOR ⊢ G \leftrightarrow \neg Prov (⌜G⌝)$ . Then if $T ⊢ G$ then $T ⊢ Prov (⌜G⌝)$ hence $T ⊢ \neg G$ so $T ⊢ ⊥$ , against assuption. So $T ⊬ G$ and $T ⊬ \neg Prov (⌜G⌝)$ .

Now let $σ$ be

G \to (Prov (⌜G⌝) \to ⊥)

Note that $σ$ is equivalent (in $DOR$ ) to $G \to \neg Prov (⌜G⌝)$ and hence to $\neg Prov (⌜G⌝) \to \neg Prov (⌜G⌝)$ and therefore

T ⊢ σ

By the property of being a provability predicate

T ⊢ Prov (⌜σ⌝)

i.e.

T ⊢ Prov (⌜G \to (Prov (⌜G⌝) \to ⊥⌝))

So using the second axiom for a provability predicate twice

T ⊢ Prov (⌜G⌝) \to (Prov (⌜Prov (⌜G⌝)⌝) \to Prov (⌜⊥⌝))

But the third axiom gives

T ⊢ Prov (⌜G⌝) \to Prov (⌜Prov (⌜G⌝)⌝)

hence

T ⊢ Prov (⌜G⌝) \to Prov (⌜⊥⌝)

T ⊢ \neg Prov (⌜⊥⌝) \to \neg Prov (⌜G⌝)

so as $T ⊬ \neg Prov (⌜G⌝)$ we have

T ⊬ \neg Prov (⌜⊥⌝)

T ⊬ Con (T)

as required.