A sentence of type is a sentence of the form , where is some fixed real parameter and all the quantifiers occuring in are ranging over the reals or naturals. A particularly famous such sentence is the continuum hypothesis , which is known to be highly non-absolute: we can always both force and force its negation. But it turns out that actually turns out to determine the -truths in models, in that any two forcing extensions in which holds have the same -truths. This is a theorem due to Woodin and Steel independently. My full write-up can be found here, but in this post I’ll just focus on the statement and the key ideas used in the proof(s).
This theorem was first proven using stationary tower forcing, but later also by using genericity iterations. By their very nature the proofs are quite different in terms of style, but their overall strategy seems to be the same – I’ll get back to this later. Firstly, let’s actually state the theorem in question. It turns out to not be exactly the same theorem, where the version proven using genericity iterations require stronger hypotheses, but whose conclusion is stronger as well. We start chronologically with the stationary tower version.
Theorem 1 (Woodin, Steel). Assume there exists a measurable Woodin cardinal and let be a -formula, a real and forcing notions such that and . Then .
In particular, if holds then any sentence in a small forcing extension reflects down to . Note the restriction here to small forcings. The next version is very similar:
Theorem 2 (Woodin, Steel). Assume that is a transitive model of a suitable fragment of , where is an extender sequence witnessing that a countable is measurable Woodin in . Assume furthermore that is -iterable in every forcing extension. Let be a -formula, a real and forcing notions such that and . Then .
Here our extra assumption is iterability of this model , but we get the stronger conclusion that it holds for all (set-sized) forcing notions. In this regard, none of the two theorems replace the other – both can be useful in different situations.
The proof strategies in the two theorems are very similar. For simplicity we will assume that is trivial, which amounts to assuming in . Both of them use the simple fact that if and contains all the reals, then -sentences are reflected upwards from to . Thus to get a statement from a forcing extension down to , we need to find a model inside , containing all the reals and somehow capturing enough of the forcing extension so that it also satisfies the given -statement.
The strategy is then to find such a model with this property. This is where the stationary tower method and the genericity iteration method diverges. I’m going to try to briefly sketch the main ideas of the two proofs below, so that the similarities hopefully becomes apparent.
Brief sketch of the stationary tower proof (Theorem 1)
In this case we start out by finding some (full) stationary tower embedding such that there is a -generic inside , plus some extra properties. These extra properties will allow us to construct generics inside , where captures the ‘th real (i.e. that the real is in ) and all the ‘s lie nested into each other. Setting to be the limit of these ‘s we get that satisfies and contains all the reals of . As , this is reflected up to , and then by elementarity of we get that holds in as well. QED
Brief sketch of the genericity iteration proof (Theorem 2)
This proof is a two-step procedure. We first transfer the truth of from to some model which we don’t necessarily know is an inner model of . Next step is then to transfer the truth from this model to an actual inner model of , and then reflect up to .
First step is to look at inside of , pick a witness to the truth of and then perform a genericity iteration to capture both and . In the extender algebra extension we then have that holds. This is the end of step one.
By elementarity we can find a condition in the extender algebra down in which forces . We then perform -many genericity iterations (recall that is assumed to hold in ), each capturing a single real each time, but making sure that is in the resulting extender algebra generic each time. In the end we wind up with an iteration such that has all the reals and satisfies . The thing to note here is that now ! This means that the truth of is reflected down to and we’re done. QED
Although both methods results in some inner model acting as a middleman between the forcing extension and , the paths toward this goal are very different. A key feature used in the stationary tower method is that we don’t have to find an inner model of containing all reals — we can instead find an inner model of containing all ‘s reals. And given that we can manipulate to have all sorts of structure, by tinkering around with stationary sets, this gives us the necessary tools to actually prove this. The genericity iteration method has the notable feature that the extender algebra generic is definable, so that the resulting generic extension will always be an inner model. This means that if we can just code up everything we want in a subset of , we can capture all of these things inside an inner model.
This is just one application in which both the stationary tower and the genericity iteration can supply us with a proof. One other such application is the proof of the derived model theorem, which is a tool to go from a model of +Large Cardinals to a model of determinacy. I’ll most probably make a post about that in the not-too-distant future. Until next time, have a happy new year!