In the last blog post we set the scene by constructing the extender algebra, and proved that to capture a real x it suffices to make sure that for some countable iteration tree T. Here we provide the construction of T and rounding off the proof.
Recall that we’re trying to prove the following theorem:
Theorem (Woodin). Let M be a countable -iterable mouse and a countable ordinal. Assume that, in M, is Woodin, realised by extenders on the M-sequence. Then there is a -cc forcing such that given any real x there is a countable iteration tree T on M following M’s strategy with last model such that exists and x is -generic over .
We’ll now start the construction of our iteration. This part of the proof is very similar to the proof of the comparison lemma between mice — the strategy is simply to iterate away the extenders we don’t like.
Start by setting , and assume now that has been constructed for some and that the tree so far doesn’t have any drops. Assume without loss of generality that and let E be an extender on the -sequence of minimal length witness this. Player I then plays and the game continues. This strategy for player I determines the tree T. The following technical claim ensures that this is actually an iteration, and that the elementary embeddings exist.
Claim. The above iteration is (a) normal and (b) no drops occur.
Proof. For (a) let ; we have to show that . Assume it’s not the case, so that is on the -sequence since and agree below . Now by construction, violates an axiom of satisfied by x, and this induces an axiom of it violates as well [to see that is an -cardinal, note that since is an -cardinal, any -cardinal is an -cardinal as well. As , the fact that no -cardinals occur in then implies that . To show (b) we need to show that measures all subsets of in . But is an -cardinal, and agrees with below . QED
This finishes the definition of player I’s strategy in the iteration game. All that remains is to show that this process terminates at a countable step, so assume it’s not the case. The following argument again has close similarities with the contradiction in the proof of the comparison lemma. Let
be the uncollapse with sufficiently large and set . We first claim that . Since we get that straight away, using that M is countable. Also, . This means that has limit order type, and any branch of an iteration tree must be closed below its supremum by definition of tree order, so , implying that . We can then conclude that since and the direct limit construction is absolute to H. In particular it holds that , so if we define we get that . This means for any ,
so that and . Letting , we have that and we have an axiom
of induced by which is false of x, meaning that the right hand side is true of x and the left hand side is false of x. But note that and , so since generators aren’t moved along branches of iteration trees, we get that
But as , we get as well since , contradicting the above. This contradiction finishes the proof of our theorem. QED
These genericity iterations can be generalised to capture arbitrary sets of ordinals rather than just reals, and sample applications include various absoluteness results. For more on these generalisations and applications, see “The Extender Algebra and -absoluteness” by Ilijas Farah.