In this very first blog post I thought that I would start out with something that really intrigued me when I first read it: Woodin’s invention of *genericity iterations*. The statement is very surprising, and the proof seems so distinct from anything else I’ve seen in set theory. The theorem more or less says that *any* real is at most an iteration and a forcing away! (given that you’re living in an iterable structure and assuming a large cardinal hypothesis)

The more precise statement is the following:

Theorem (Woodin).LetMbe a countable -iterable mouse and a countable ordinal. Assume that, inM, is Woodin, realised by extenders on theM-sequence. Then there is a -cc forcing such that given any realxthere is a countable iteration treeTonMfollowingM’s strategy with last model such that exists andxis -generic over .

The proof I’ll give is more or less the proof in Steel’s handbook article. The surprising thing about the proof is that the elements of is really infinitary formulas! Let be the language of propositional logic with many variables , where we furthermore allow conjunctions and disjunctions of size .

Provability of this logic is just using the usual logical axioms and deduction rules, where we’re furthermore also allowed to infer if holds for every , for some . We can interpret any real as a model of this language by stipulating that iff and then recursively expand this to the other formulas. Note that the logic is sound with respect to all reals. We’re going to consider the following theory , consisting of the axioms

,

where *E* is on the *M*-sequence, and is a cardinal in *M* such that . To this theory we consider the so-called *Lindenbaum algebra*, which is a Boolean algebra consisting of equivalence classes of -formulas, where two formulas and are equivalent iff , and we set iff . This particular instance of the Lindenbaum algebra is called the *extender algebra* and is denoted by . An important feature of is the following.

Proposition.The extender algebra is -cc inMand therefore also a complete Boolean algebra inM.

**Proof.** Assume it’s not the case and let be an antichain in . Fix some which is *A*-reflecting, witnessed by an extender *F* on the *M*-sequence. Let be large enough so that and let *E* be the trivial completion of . It then holds that , so that

and then . But this means that for some , a contradiction. Finally, since for , is closed under -sums and every sum is of size since is -cc. **QED**

The first step towards “capturing” our real *x* is the following.

Proposition.For any realx, if then is a -generic ultrafilter overMand .

**Proof****.** We need to make sure that is well-defined on equivalence classes: if then iff by soundness of our logic. It’s not too hard to show that is an ultrafilter, so towards showing that it’s generic let be a maximal antichain. Then as is -cc, so . In particular , so for some . Soundness then entails that , meaning that . Lastly, to show that we note that iff , making *x* definable from . **QED**

The strategy now is then to somehow make an arbitrary real *x* satisfy , so that the above proposition supplies us with what we want. This is exactly what the genericity iteration is about. We’re going to iterate *M* to some which satisfies , so that the above propositions relativised to proves the theorem. The construction of this iteration is the content of the next blog post. Stay tuned!