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, $\text{Con}\left(T\right)$.

One part of the first incompleteness theorem gives, for each recursive theory $T$
extending $\text{DOR}$, a statement $G$ equivalent to
$\forall x\u200a\neg {\mathrm{Proof}}_{T}(x,\u231cG\u231d)$, and the first
part of the argument shows that, assuming $T$ is consistent, $T\u22acG$,
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 $\text{Con}\left(T\right)\to G$. Since $T\u22acG$, Gödel concludes
that $T\u22ac\text{Con}\left(T\right)$.

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 $\text{DOR}$, our predicate
${\mathrm{Proof}}_{T}(x,y)$, and our sentence $G$ equivalent (in $\text{DOR}$)
to $\forall x\u200a\neg {\mathrm{Proof}}_{T}(x,\u231cG\u231d)$. We also
write $\text{Con}\left(T\right)$ for $\forall x\u200a\neg {\mathrm{Proof}}_{T}(x,\u231c\perp \u231d)$.
We attempt to prove $\text{Con}\left(T\right)\to G$ in $T$ so we take an arbitrary
model $M\models T+\neg G$ and attempt to show $M\models \neg \text{Con}\left(T\right)$.

- We have from $M\models \neg G$ that $M\models \exists x\u200a{\mathrm{Proof}}_{T}(x,\u231cG\u231d)$. This statement true in $M$ is a ${\Sigma}_{1}$ statement.
- Any ${\Sigma}_{1}$ statement true in the real world is provable in
$\text{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 $\sigma \to \exists x\u200a{\mathrm{Proof}}_{\text{DOR}}(x,\u231c\sigma \u231d)$
for each ${\Sigma}_{1}$ sentence $\sigma $.
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 ${\Sigma}_{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\models \neg G$ and $\neg G$ is ${\Sigma}_{1}$. We conclude that $M\models \exists y\u200a{\mathrm{Proof}}_{T}(y,\u231c\neg G\u231d)$.
- But then $M$ contains proofs of both $G$ and $\neg G$. These proofs could be combined to obtain a single proof of $\perp $, a proof that is an element of $M$. In other words, $M\models \exists y\u200a{\mathrm{Proof}}_{T}(y,\u231c\perp \u231d)$ or $M\models \neg \text{Con}\left(T\right)$.
- Since we have concluded that $M\models \neg \text{Con}\left(T\right)$ and $M$ was arbitrary model of $T+\neg G$, it follows by Completeness that $T\u22a2\neg G\to \neg \text{Con}\left(T\right)$, 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 $\perp $. These details are filled in in the next section.

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 $\text{DOR}$. A first order
formula $\text{Prov}\left(x\right)$ in
the language of $\text{DOR}$ with single free-variable $x$ is called
a *provability predicate* for $T$ if the following hold for
all sentences $\sigma ,\tau $ in the language of $T$:

- if $T\u22a2\sigma $ then $T\u22a2\text{Prov}\left(\u231c\sigma \u231d\right)$;
- $T\u22a2\text{Prov}\left(\u231c\sigma \to \tau \u231d\right)\to \left(\text{Prov}\right(\u231c\sigma \u231d)\to \text{Prov}(\u231c\tau \u231d\left)\right)$;
- $T\u22a2\text{Prov}\left(\u231c\sigma \u231d\right)\to \text{Prov}\left(\u231c\text{Prov}\left(\u231c\sigma \u231d\right)\u231d\right)$.

The first of these clauses connects $\text{Prov}\left(\u231c\sigma \u231d\right)$ 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 $\text{Prov}\left(x\right)$ is given for a theory $T$ then $\text{Con}\left(T\right)$ is $\neg \text{Prov}\left(\u231c\perp \u231d\right)$.

Theorem.

Suppose $T$ is a consistent theory extending $\text{DOR}$ with a provability predicate $\text{Prov}\left(x\right)$. Then $T\u22ac\text{Con}\left(T\right)$.

**Proof.**

By diagonalisation let $G$ satisfy $\text{DOR}\u22a2G\leftrightarrow \neg \text{Prov}\left(\u231cG\u231d\right)$. Then if $T\u22a2G$ then $T\u22a2\text{Prov}\left(\u231cG\u231d\right)$ hence $T\u22a2\neg G$ so $T\u22a2\perp $, against assuption. So $T\u22acG$ and $T\u22ac\neg \text{Prov}\left(\u231cG\u231d\right)$.

Now let $\sigma $ be

$$G\to \left(\text{Prov}\right(\u231cG\u231d)\to \perp )$$Note that $\sigma $ is equivalent (in $\text{DOR}$) to $G\to \neg \text{Prov}\left(\u231cG\u231d\right)$ and hence to $\neg \text{Prov}\left(\u231cG\u231d\right)\to \neg \text{Prov}\left(\u231cG\u231d\right)$ and therefore

$$T\u22a2\sigma $$By the property of being a provability predicate

$$T\u22a2\text{Prov}\left(\u231c\sigma \u231d\right)$$i.e.

$$T\u22a2\text{Prov}\left(\u231cG\to \left(\text{Prov}\right(\u231cG\u231d)\to \perp \u231d\right))$$So using the second axiom for a provability predicate twice

$$T\u22a2\text{Prov}\left(\u231cG\u231d\right)\to \left(\text{Prov}\right(\u231c\text{Prov}\left(\u231cG\u231d\right)\u231d)\to \text{Prov}(\u231c\perp \u231d\left)\right)$$But the third axiom gives

$$T\u22a2\text{Prov}\left(\u231cG\u231d\right)\to \text{Prov}\left(\u231c\text{Prov}\left(\u231cG\u231d\right)\u231d\right)$$hence

$$T\u22a2\text{Prov}\left(\u231cG\u231d\right)\to \text{Prov}\left(\u231c\perp \u231d\right)$$or

$$T\u22a2\neg \text{Prov}\left(\u231c\perp \u231d\right)\to \neg \text{Prov}\left(\u231cG\u231d\right)$$so as $T\u22ac\neg \text{Prov}\left(\u231cG\u231d\right)$ we have

$$T\u22ac\neg \text{Prov}\left(\u231c\perp \u231d\right)$$or

$$T\u22ac\text{Con}\left(T\right)$$as required.