Woodin’s proof of the second incompleteness theorem for set theory

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

502 – The Banach-Tarski paradox

1. Non-measurable sets

In these notes I want to present a proof of the Banach-Tarski paradox, a consequence of the axiom of choice that shows us that a naive understanding of the concept of volume can lead to contradictions. A good reference for this topic is the very nice book The Banach-Tarski paradox by Stan Wagon.

502 – Exponentiation

This is the last homework assignment of the term: Assume Evaluate the cardinal number the size of the set of all functions

502 – The constructible universe

In this set of notes I want to sketch Gödel’s proof that is consistent with the other axioms of set theory. Gödel’s argument goes well beyond this result; his identification of the class of constructible sets eventually led to the development of inner model theory, one of the main areas of active research within set theory nowadays.

A good additional reference for the material in these notes is Constructibility by Keith Devlin.

1. Definability

The idea behind the constructible universe is to only allow those sets that one must necessarily include. In effect, we are trying to find the smallest possible transitive class model of set theory.

is defined as

where for limit, and where

The first question that comes to mind is whether this definition even makes sense. In order to formalize this, we need to begin by coding a bit of logic inside set theory. The recursive constructions that we did at the beginning of the term now prove useful.

502 – Equivalents of the axiom of choice

The goal of this note is to show the following result:

Theorem 1 The following statements are equivalent in

1. The axiom of choice: Every set can be well-ordered.
2. Every collection of nonempty set admits a choice function, i.e., if for all then there is such that for all
3. Zorn’s lemma: If is a partially ordered set with the property that every chain has an upper bound, then has maximal elements.
4. Any family of pairwise disjoint nonempty sets admits a selector, i.e., a set such that for all in the family.
5. Any set is a well-ordered union of finite sets of bounded size, i.e., for every set there is a natural an ordinal and a function such that for all and
6. Tychonoff’s theorem: The topological product of compact spaces is compact.
7. Every vector space (over any field) admits a basis.

502 – Cantor-Bendixson derivatives

Given a topological space and a set let be the set of accumulation points of i.e., those points of such that any open neighborhood of meets in an infinite set.

Suppose that is closed. Then Define for closed compact by recursion: and for limit. Note that this is a decreasing sequence, so that if we set there must be an such that for all  

[The sets are the Cantor-Bendixson derivatives of In general, a derivative operation is a way of associating to sets some kind of “boundary.”]

502 – The Löwenheim-Skølem theorem

In this note I sketch the proof of the Löwenheim-Skølem (or Löwenheim-Skølem-Tarski) theorem for first order theories. This basic result of model theory is really a consequence of a set theoretic combinatorial lemma, as the proof will demonstrate.

Let be a first order language, understood as a set of constant, function, and relation symbols. Let

so is unless is finite, in which case we take Talking about rather than simplifies the presentation slightly.

The Löwenheim-Skølem theorem is concerned with the possible infinite sizes of models of first order theories. Of course, a theory could only have finite models; the result does not say anything about if that is the case.

Theorem 1 If is a first order theory in a language and there is at least one infinite model of then there are models of of size for all

We will prove a more precise statement. Before stating it, note that it is possible to have a theory in some uncountable language such that has models of certain infinite sizes, but not all. Theorem 1 does not say anything about infinite models of of size What cardinals in this range are the possible sizes of models of is actually a rather difficult problem, and we will not address it.

502 – Cancellation laws

Two homework problems. The first one is easier, so you can consider the second one to be extra credit. A proof of these results can be found in different places, for example, the paper Division by three, by Conway and Doyle. (Please don’t look at the paper while working on the homework, of course.) Unfortunately, the paper could use a serious trimming and editing, so I cannot really recommend it, but the proof is carefully written there.

1. Without using the axiom of choice, show that if and are sets, and then
2. Same as 1., but now with instead of  

502 – More on tilings

In class I mentioned without proof that there is a finite set of squares with which we can tile the plane, but not periodically. Hao Wang was the first to study the question of whether there are such tilings. He conjectured that the answer was not. In 1966, his student Robert Berger disproved the conjecture. He explained how tiles could be used to code the workings of a formalized computer (a Turing machine), in a way that one could solve recursively the Halting Problem if it were the case that any set that tiles can do so periodically. Since it is a well-known result from computability theory that the halting problem cannot be solved recursively, it follows that Wang’s conjecture is false.

Examining the tiling given by Berger, one finds that he requires 20426 tiles to do his coding. The number has been substantially reduced since. I believe the currently known smallest set of tiles that can only cover the plane aperiodically has size 13. It was exhibited by Karel Culik II in his paper An aperiodic set of 13 Wang tiles, Discrete Mathematics 160 (1996), 245-251. The Wikipedia entry on Wang tiles displays his example. Once again, the proof of aperiodicity uses the halting problem.

(I would be curious to know of improved bounds.)

502 – Ordinal exponentiation

The exercise I mentioned in class is the following: Let denote ordinal exponentiation. For ordinals , define as the set consisting of those functions such that there are only finitely many such that  

(We haven’t formally defined “finite” yet, but we can take this to mean that the order type of the set is a natural number, using our formalized notion of natural number.)

For functions in set iff for largest such that

Then is a well-ordered set, and its order type is precisely