In my previous posts I provided a sketch of how a measurable above a limit of Woodins implies that holds in . The “converse”, saying that implies that there is a model with infinitely many Woodin cardinals, is a lot more complicated. I will try to simplify a lot of these complications here, to give an idea of what is going on. I will only focus on showing the existence of a single Woodin (for now), where the Woodin in question will be inside of . As always, I will be very sketchy in this blog post, but provide more details in my note.

The theorem of interest is the following.

Theorem 1 (Woodin).Assume . Thenis a Woodin cardinal.

The assumption of is not really needed, but it makes the proof a bit more smooth. The proof of this theorem is very related to the following theorem, due to Solovay.

Theorem 2 (Solovay).Assume . Thenis measurable.

To define the given measure on we first need to introduce some terminology. For define the binary relation

,

where is a recursive bijection. Then the key set is

.

Also, setting to be the order-type of , set and define , and and so on in the obvious fashion. Then define the game associated to a subset as

,

with and the rules of the game requiring that for every and . Player I wins iff . We can then define our measure on as

iff Player I wins .

Then is clearly non-principal, upwards closed and ensures that it has the ultra property. It thus only remains to show that it’s normal. Assuming it’s not and letting be a regressive function witnessing the failure of normality, implies that

for every . It then turns out that we can define

- An increasing sequence of countable ordinals;
- A sequence of sets of strategies where consists of winning strategies for player I in for all (where we set for convenience);
- A sequence of reals such that is legal for player II against any and .

These ‘s will then witness that for any , by definition of the games as well as the definition of the ‘s. But this then contradicts that is regressive!

The actual construction of the above sequences requires some tools that relies on the nature of the set . We won’t supply the proofs of neither these tools nor how they entail the existence of the above sequences – if you’re interested you can have a look at my note. The two tools that we need is a boundedness result and a coding result.

Tool 1 (-boundedness; Luzin-Sierpinski).Assume . Then whenever is there is some such that .

Tool 2 (Basic coding; Solovay).Assume and let . Then there is a subset such that is aselectorfor , i.e. that for every it holds that.

Tool 2 is used to construct a specific choice of ‘s such that Tool 1 can be used to construct the ‘s. This finishes the (very rough) sketch of Solovay’s Theorem 2. The same ideas can be used to show that is also measurable in . Here’s the analogy:

Here is a universal set, and just as the ‘s partitioned into -many pieces, the ‘s are defined in such a way that they also partition into -many pieces. We get analogous boundedness and coding tools which are due to Moschovakis, and by using these we can simply copy the proof of Solovay’s theorem to get the following.

Theorem 3 (Moschovakis).Assume . Thenis measurable.

The use of can be avoided, but it is required if we simply want to reuse Solovay’s proof. When we want to not only show measurability, but show *Woodinness*, we have to suddenly construct *extenders* rather than measures to get the desired strength. These will use similar ideas, but a new *reflection** tool* will be needed. More about that next time!

*Here’s a link to the follow-up post*