In the prequel I sketched a proof of how determinacy hypotheses could imply the measurability of both and inside . The latter is really the first step in showing the *much* stronger assertion that is Woodin. I’ll here sketch what main ideas are involved in the proof of this fact.

The main theorem in question is thus the following, due to Woodin.

Theorem (Woodin).Assume ZF+DC+AD. Then.

I should note that the theorem still holds without the use of DC, by using an alternative characterisation of Woodin cardinals – but I’ll stick the following one.

Definition.A cardinal isWoodinif for every there exists a cardinal which isA-reflecting, which is to say that given any we can find an elementary embedding with critical point and satisfying , and .

To show that is Woodin in HOD we can first of all focus on the case where , meaning that we need to find an -reflecting — this will be the case we focus on here in this post, as the case for arbitrary turns out to be a relativisation of this case. This will turn out to be precisely , so to every we need to find an elementary embedding with critical point , and .

The main new gadget that we’re going to use is a *reflection phenomenon* at : there exists a function such that

Given any , and formula , if

then there’s a such that

.

This is constructed analogously to -sequences in , i.e. defining it by least counterexample. To any as above we pick a universal set and for each let be a universal set, obtained by using the same definition as . We now claim that to each -formula and real we can construct a real such that

iff .

To define the note that the right-hand side above is a formula, meaning that the set of ‘s satisfying it is in for some , so that we can define . We can then reformulate the above reflection phenomenon as .

Now to actually define our measure on . Let be arbitrary and fix an OD pre-wellordering of the reals of order-type . Then our desired is going to be . To each we can now define the game as

Here the only rule is that for every . In this case that very rule can be seen as a statement, so the reflection phenomenon applies and there is some such that for every . Then player I wins iff . Analogously to the previous measures we then set

.

Now, what’s special about this measure as opposed to the measure we found in my previous post? The key set is , consisting of all such that , where is a pre-wellordering of the reals of order-type and that satisfies a sufficient chunk of ZFC.

Let () be the ‘th component of (). Furthermore, for every and let be the unique such that and define the functions as . A major theorem is that collapses to the -rank of in the ultrapower. This means straight away that as for every and .

The -strongness of is shown by describing any subset with in terms of the ‘s using a new coding lemma, so that we get a “reflected version” of , which we can use to describe in the ultrapower. See (some) details in my note.