In a previous post we proved that whenever a countable mouse M has n Woodins it understands sets, implying that whenever A is such a set it holds that . As we mentioned back then, this is not as good as being correct about these sets, which would mean that whenever A of course is non-empty as well. Another way to phrase this is to say that iff for every -sentence. Now, what does it then take for a mouse to be projectively correct?
Recall what it means for M to understand a set of reals A at some ordinal . Roughly speaking, we got a forcing term in M for the collapse of to be countable, which represents A in the sense that whenever is M-generic. Now, M captures A if it understands it and absorbs reals at , roughly meaning that we can do genericity iterations at , as if it was a Woodin cardinal.
Using this terminology, M captures all sets of reals if M has n Woodins. Simply capturing won’t do to yield correctness though — here we further require the forcing terms witnessing the capturing to be of the form , where is a tree on for some X. We call this Suslin capturing. Let’s firstly show that this suffices for what we want to do.
Lemma. Let M be a countable mouse, A a set of reals and assume that M Suslin-captures A. Then implies .
Proof. Assume M Suslin-captures A at via , and let . Use that M absorbs reals at to get an iteration and a generic such that . But since M understands A at M we get that , so that . Then absoluteness of wellfoundedness and elementarity implies that . But note that by applying understanding with and g trivial, so that . QED
This then means that if M Suslin-captures both and then M is correct about sentences. Okay, brilliant, Suslin-capturing suffices! But how do we know whether our favorite mouse actually Suslin-captures some (perhaps complicated) set of reals? This is where the following theorem helps us out.
Theorem. Let M be a countable mouse, and assume that M Suslin-captures A at . Then M also Suslin-captures and at every .
Before we commence with the proof let’s just note a few considerable corollaries. Firstly note that every M Suslin-understands sets of reals, by the proof of Shoenfield’s absoluteness theorem. The above theorem then implies that M Suslin-captures every set of reals whenever M has n Woodins. A first consequence of this is then that M is -correct whenever M has n Woodins (and thus projectively correct when it has a limit of Woodins). A second consequence, using the corollary from my last post, is that the existence of a countable mouse with Woodins implies that every set of reals is determined. Now, on with the proof. Buckle up.
Proof. Let witness the Suslin-capturing of A and fix a . We’ll start by showing that M Suslin-captures at , and it will turn out that a slightly simpler argument shows the corresponding fact for . To Suslin-capture we need to build a tree which witnesses that whenever is an iteration of M and is N-generic. Purely for notational convenience we’ll assume that in the following.
The construction of the tree U
Our tree will be a tree on , where satisfies that and (Kripke-Platek set theory). Instead of going into the gritty details of the construction, we’ll simply describe a blueprint.
Let be the language of premice along with countably many constant symbols . U is then the tree of attempts to construct a quadruple satisfying the following.
- y encodes a complete Henkin theory of a pointwise definable -structure such that , where is the -sentence ;
- z encodes a proof of the sentence saying that there exists an -generic such that and ;
- is an elementary embedding such that .
Now, let’s see that this actually works, so let . We need to show that , so let be arbitrary. By definition of U we have an embedding such that, letting for every , there’s an R-generic such that and whenever is -generic it holds that .
We now want to apply elementarity of j to move this scenario over to the M-side. We firstly need to be sure that the universal quantifier appearing in includes as well though, so we first need to catch this real. If we let be M’s iteration strategy then the pullback strategy makes R iterable, so that we can absorb y at , meaning that there’s an iteration and a P-generic such that . We also ensure that , so that we don’t change any of the above forcing facts about R.
Let be the iteration of M corresponding to and the lift of . Then elementarity of yields that there’s a Q-generic such that and, letting correspond to , . But , so in particular . As M understands A via T and y was arbitrary this means that .
Now, for the other inclusion, let — we want to show that . Since M Suslin-captures A at via T we get that , where , where and is some condition. As it can define wellfounded parts of relations belonging to it, so that as well. Now, working in M[g] we can find with R countable and everything relevant in . Let , encode a proof of and encode the -theory of R. It’s then clear that
The proof of the case is nearly identical. We simply replace the universal quantifier in with an existential one, and without having to catch . QED