[Edit, Oct. 1, 2013: Robert Solovay has pointed out an inaccuracy in my presentation of Woodin’s argument: Rather than simply requiring that is a hereditary property of models, we must require that
proves this. A corrected presentation of the argument will be posted shortly.]
As part of the University of Florida Special Year in Logic, I attended a conference at Gainesville on March 5–9, 2007, on Singular Cardinal Combinatorics and Inner Model Theory. Over lunch, Hugh Woodin mentioned a nice argument that quickly gives a proof of the second incompleteness theorem for set theory, and somewhat more. I present this argument here.
The proof is similar to that in Thomas Jech, On Gödel’s second incompleteness theorem, Proceedings of the American Mathematical Society 121 (1) (1994), 311-313. However, it is semantic in nature: Consistency is expressed in terms of the existence of models. In particular, we do not need to present a proof system to make sense of the result. Of course, thanks to the completeness theorem, if consistency is first introduced syntactically, we can still make use of the semantic approach.
Woodin’s proof follows.
Argue within .
It is fairly easy to formalize first order languages in set theory so that for each formula we have a formal counterpart (a code)
, the map
is recursive, so that the usual syntactic operations with formulas can be carried out on their formalizations, and satisfaction (for set-sized models) is defined.
The key technical tool we require is the fixed-point lemma:
Lemma 1 For any formula
in one free variable, there is a sentence
such that
Proof: This is well known. Let assert that
is the code of a formula
and that
holds.
Let be the code for
. Then
iff
, so we can take
to be
.
From now on, I will abuse language and simply write for both a formula and its code.
Let . For
, write
,
Then is the actual model that
code within
.
The following is shown by a straightforward induction on formulas:
Lemma 2 Suppose
. If
, then
.
(Of course, by considering , it follows immediately that the converse also holds.)
We say that is a property of models of set theory iff
implies
.
Say that is hereditary iff it is a property of models of set theory and, whenever
then .
Theorem 3 Suppose that
is hereditary. Then, either
fails for all
, or else there is an
such that
.
Proof: Let . Using the fixed-point lemma, let
be such that (
proves that)
.
Suppose . Then
, so
for some
. But then
.
We have shown that implies
. Fix such
, and note that
.
Suppose . Then
, contradiction. Hence
as needed.
Let “ is consistent” be the assertion that there is a model of
. The second incompleteness theorem follows at once:
Corollary 4 Either
is inconsistent, or else
is inconsistent.”
Proof: Let . We claim that
is hereditary. This amounts to showing that
implies
.
This is because for each true axiom of
,
implies
, and
Corollary 5 Either there are no
-models of
or else there is an
-model of
without
-models of
.
Proof: Let is an
-model of
. Suppose that
. Then
and
so
, and
follows.
Corollary 6 Either there are no transitive models of
or else there is a transitive model without transitive models.
Proof: Let is a transitive model of
. Let
,
transitive. Then
, so
is really transitive.
Remark 1 If
is an
-model of
, then
This is because
proves the completeness theorem, and therefore “
is consistent” is (equivalent to) the arithmetic statement “There is no proof from
of
”. But the existence of
implies that this statement is true. Now note that, since
is an
-model, it is correct for arithmetic statements.
Remark 2 Similarly, if
is a transitive model of
, then
This is because of Mostowski’s absoluteness theorem: Any transitive model of set theory is correct about
statements. See, for example, section 13 of Akihiro Kanamori, The higher infinite: Large cardinals in set theory from their beginnings, Springer, second edition (2008).
Note that the statement “There is an
-model of {\sf ZFC}” is
, as it can be expressed by saying that there is a real
coding a model of
, and there is a real
coding an order isomorphism of
onto the natural numbers of the model coded by
.
Since any transitive model is an
-model, the existence of
implies that the
statement that there is an
-model is true. But then it holds in
.
The following is a version for -models of
of a result of Steel on
-models of second order arithmetic, see John Steel, Descending Sequences of Degrees, The Journal of Symbolic Logic, 40 (1), (Mar., 1975), 59–61.
If is a model of set theory, and
is a model of
for some theory
, we can think of
as a code for
. We use “code” in a slightly more general fashion in the statement below:
Corollary 7 There is no sequence
of
-models of
such that for all
, there is a code for
in
.
Proof: Let is an
-model of
and there is a sequence
of
-models of
such that
and, for all
, there is a code for
in
.
Obviously, is hereditary, since being an
-model is. It follows that either the corollary holds, or else there is an
such that
but
.
However, the second possibility is impossible, since if is a sequence witnessing
, then
is a sequence witnessing
. But the code
for this sequence is in
and so, in
,
holds of the code for
, as witnessed by
. Contradiction.
Finally, I sketch how to recover the full version of the second incompleteness theorem from Woodin’s proof.
Theorem 8 If
is a consistent recursively enumerable theory that interprets
, then
cannot prove its own consistency.
Proof: There are a few additional wrinkles, since we only assume that the theory under consideration interprets :
- It is not clear how to even state the completeness theorem within
. However, completeness is provable within the system
of second order arithmetic (this is shown in Stephen Simpson, Subsystems of second order arithmetic, Cambridge University Press, second edition (2010), see for example Theorem IV.3.3). Moreover, for arithmetic statements,
is conservative over
.
- Although it is fairly straightforward that
is conservative over
for first order statements, we need that this is provable within
. This can be done in a few ways. See, for example, Joseph Shoenfield, Mathematical Logic, A K Peters (2001).
From the above, it follows that arguing within , we can implement Woodin’s proof.
Typeset using LaTeX2WP. Here is a printable version of this post.
Just FYI, the arithmetized completeness theorem was proven for PA by Feferman in 1960, and I believe the result was known long before that. Nowadays, it’s known that one can prove it already in Q. Indeed, a good proof shows that the resulting model is always of fairly low complexity: \Delta_2.