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 cannot even prove its own consistency, .
One part of the first incompleteness theorem gives, for each recursive theory
extending , a statement equivalent to
, and the first
part of the argument shows that, assuming is consistent, ,
to which we can
momentarily and conclude that
must actually be true because really cannot prove it.
There's a lot that has been made about this argument, to wit that cannot
that is true but we can see that is in fact true and therefore
we are in some sense
cleverer than . (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
Gödel realised this and in fact this is how he originally stated his second incompleteness
theorem: a sufficiently strong theory can formalise the argument just given
and prove . Since , Gödel concludes
It's worth looking at this argument in a bit more detail, because it is illuminating
and indicates what we expect such theories 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 extending , our predicate
, and our sentence equivalent (in )
to . We also
write for .
We attempt to prove in so we take an arbitrary
model and attempt to show .
is sufficiently strong..
There are some small details left out here, to do with how and can manipulate logic and proofs, in particular the logic of , and . 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.
Suppose is a theory extending . A first order formula in the language of with single free-variable is called a provability predicate for if the following hold for all sentences in the language of :
The first of these clauses connects 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.
If a provability predicate is given for a theory then is .
Suppose is a consistent theory extending with a provability predicate . Then .
By diagonalisation let satisfy . Then if then hence so , against assuption. So and .
Now let be
Note that is equivalent (in ) to and hence to and therefore
By the property of being a provability predicate
So using the second axiom for a provability predicate twice
But the third axiom gives
so as we have