[**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 1For 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 2Suppose . 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 3Suppose 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 4Either 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 5Either 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 6Either 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 1If 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 2Similarly, 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 7There 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 8If 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.