Genericity iterations I

In this very first blog post I thought that I would start out with genitsomething 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). Let M be a countable (\omega,\omega_1+1)-iterable mouse and \delta a countable ordinal. Assume that, in M\delta  is Woodin, realised by extenders on the M-sequence. Then there is a \delta-cc forcing \mathbb Q\subset V_\delta^M such that given any real x there is a countable iteration tree T on M following M’s strategy with last model M_\alpha such that i_{0,\alpha}^T exists and x is i_{0,\alpha}^{\mathcal T}(\mathbb Q)-generic over M_\alpha.

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 \mathbb Q is really infinitary formulas! Let \mathcal L_{\delta,\omega} be the language of propositional logic with \omega many variables v_n, where we furthermore allow conjunctions and disjunctions of size <\delta.

Provability of this logic is just using the usual logical axioms and deduction rules, where we’re furthermore also allowed to infer \bigwedge_{\xi<\kappa}\varphi_\xi if \varphi_\xi holds for every \xi<\kappa, for some \kappa<\delta. We can interpret any real as a model of this language by stipulating that x\models v_n iff n\in x 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 \Gamma, consisting of the axioms

\bigvee_{\alpha<\kappa}\varphi_\alpha\leftrightarrow\bigvee_{\alpha<\lambda} i_E(\left<\varphi_\xi\mid\xi<\kappa\right>)_\alpha,

where E is on the M-sequence, \text{crit }E=\kappa\leq\lambda and \nu_E is a cardinal in M such that i_E(\left<\varphi_\xi\mid\xi<\kappa\right>)\upharpoonright\lambda\in M|\nu_E. To this theory \Gamma we consider the so-called Lindenbaum algebra, which is a Boolean algebra consisting of equivalence classes of \mathcal L_{\delta,\omega}-formulas, where two formulas \varphi and \psi are equivalent iff \Gamma\vdash\varphi\leftrightarrow\psi, and we set [\varphi]\leq[\psi] iff \Gamma\vdash\varphi\to\psi. This particular instance of the Lindenbaum algebra is called the extender algebra and is denoted by \mathbb Q. An important feature of \mathbb Q is the following.

Proposition. The extender algebra is \delta-cc in M and therefore also a complete Boolean algebra in M.

Proof. Assume it’s not the case and let A:=\left<\varphi_\alpha|\alpha<\delta\right> be an antichain in \mathbb Q. Fix some \kappa<\delta which is A-reflecting, witnessed by an extender F on the M-sequence. Let \lambda\in(\kappa,\delta) be large enough so that \varphi_\kappa\in V_\lambda^M and let E be the trivial completion of F\upharpoonright\lambda. It then holds that i_E(A)\upharpoonright\kappa+1=A\upharpoonright\kappa+1, so that

i_E(\bigvee_{\alpha<\kappa}\varphi_\alpha)\upharpoonright\kappa+1=\bigvee_{\alpha\leq\kappa}\varphi_\alpha

and then \Gamma\vdash\bigvee_{\alpha<\kappa}\varphi_\alpha\leftrightarrow\bigvee_{\alpha\leq\kappa}\varphi_\alpha. But this means that [\varphi_\kappa]\leq[\bigvee_{\alpha<\kappa}\varphi_\alpha]\leq[\varphi_\xi] for some \xi<\kappa, a contradiction. Finally, since \sum_{\alpha<\kappa}[\varphi_\alpha]=[\bigvee_{\alpha<\kappa}\varphi_\alpha] for \kappa<\delta, \mathbb Q is closed under <\delta-sums and every sum is of size <\delta since \mathbb Q is \delta-cc. QED

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

Proposition. For any real x, if x\models\Gamma then G_x:=\{[\varphi]\mid x\models\varphi\} is a \mathbb Q-generic ultrafilter over M and x\in M[G_x].

Proof. We need x\models\Gamma to make sure that G_x is well-defined on equivalence classes: if \Gamma\vdash\varphi\leftrightarrow\psi then x\models\varphi iff x\models\psi by soundness of our logic. It’s not too hard to show that G_x is an ultrafilter, so towards showing that it’s generic let \left<[\varphi_\alpha]\mid\alpha<\gamma\right> be a maximal antichain. Then \gamma<\delta as \mathbb Q is \delta-cc, so [\bigvee_{\alpha<\gamma}\varphi_\alpha]=1. In particular \Gamma\vdash\bigvee_{\alpha<\gamma}\varphi_\alpha, so \Gamma\vdash\varphi_\xi for some \xi<\gamma. Soundness then entails that x\models\varphi_\xi, meaning that [\varphi_\xi]\in G_x. Lastly, to show that x\in M[G_x] we note that i\in x iff [v_i]\in G_x, making x definable from G_xQED

The strategy now is then to somehow make an arbitrary real x satisfy x\models\Gamma, 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 M_\alpha which satisfies x\models i_{0,\alpha}(\Gamma), so that the above propositions relativised to M_\alpha proves the theorem. The construction of this iteration is the content of the next blog post. Stay tuned!