[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.