Projectively Correct Mice

In a previous post we proved that whenever a countable mouse M has n Woodins it understands $\bf\Pi^1_{n+1}$ sets, implying that whenever A is such a set it holds that $A\cap M\in M$. As we mentioned back then, this is not as good as being correct about these sets, which would mean that $A\cap M\neq\emptyset$ whenever A of course is non-empty as well. Another way to phrase this is to say that $V\models\sigma$ iff $M\models\sigma$ for every $\bf\Pi^1_{n+1}$-sentence. Now, what does it then take for a mouse to be projectively correct?

This post is part of a series on genericity iterations:

Recall what it means for M to understand a set of reals A at some ordinal $\eta < o(M)$. Roughly speaking, we got a forcing term $\tau$ in M for the collapse of $\eta$ to be countable, which represents A in the sense that $A\cap M[g]=\tau^g$ whenever $g\subseteq\text{Col}(\omega,\eta)^M$ is M-generic. Now, M captures A if it understands it and absorbs reals at $\eta$, roughly meaning that we can do genericity iterations at $\eta$, as if it was a Woodin cardinal.

Using this terminology, M captures all $\bf\Pi^1_{n+1}$ 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 $p[\check T]$, where $T\in M$ is a tree on $\omega\times X$ 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 $A\neq\emptyset$ implies $M\cap A\neq\emptyset$.

Proof. Assume M Suslin-captures A at $\eta < o(M)$ via $T\in M$, and let $x\in A$. Use that M absorbs reals at $\eta$ to get an iteration $i:M\to N$ and a generic $g\subseteq\text{Col}(\omega,i(\eta))^N$ such that $x\in N[g]$. But since M understands A at M we get that $N[g]\cap A=p[T]$, so that $x\in p[T]$. Then absoluteness of wellfoundedness and elementarity implies that $M\models p[T]\neq\emptyset$. But note that $A\cap M=p[T]$ by applying understanding with $i=\text{id}$ and g trivial, so that $A\cap M\neq\emptyset$. QED

This then means that if M Suslin-captures both $A$ and $\lnot A$ then M is correct about ${\bf\Sigma^1_1}(A)$ 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, $A\subseteq\mathbb R^2$ and assume that M Suslin-captures A at $\eta < o(M)$. Then M also Suslin-captures $\exists^{\mathbb R}A$ and $\forall^{\mathbb R}A$ at every $\xi<\eta$.

Before we commence with the proof let’s just note a few considerable corollaries. Firstly note that every M Suslin-understands $\Sigma^1_1$ sets of reals, by the proof of Shoenfield’s absoluteness theorem. The above theorem then implies that M Suslin-captures every $\bf\Sigma^1_{n+1}$ set of reals whenever M has n Woodins. A first consequence of this is then that M is $\bf\Sigma^1_{n+1}$-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 $n>1$ Woodins implies that every $\bf\Sigma^1_{n+1}$ set of reals is determined. Now, on with the proof. Buckle up.

Proof. Let $T\in M$ witness the Suslin-capturing of A and fix a $\xi<\eta$. We’ll start by showing that M Suslin-captures $\forall^{\mathbb R}A$ at $\xi$, and it will turn out that a slightly simpler argument shows the corresponding fact for $\forall^{\mathbb R}A$. To Suslin-capture $\forall^{\mathbb R}A$ we need to build a tree $U\in M$ which witnesses that $\forall^{\mathbb R}A\cap N[g]=p[i(U)]$ whenever $i:M\to N$ is an iteration of M and $g\subseteq\text{Col}(\omega,i(\xi))^N$ is N-generic. Purely for notational convenience we’ll assume that $i=\text{id}$ in the following.

The construction of the tree U
Our tree will be a tree on $\omega^3\times M|(\gamma+1)$, where $\gamma < o(M)$ satisfies that $T\in M|\gamma$ and $M|\gamma\models\textsf{KP}$ (Kripke-Platek set theory). Instead of going into the gritty details of the construction, we’ll simply describe a blueprint.
Let $L$ be the language of premice along with countably many constant symbols $\langle c_n\mid n<\omega\rangle$. U is then the tree of attempts to construct a quadruple $\langle x,y,z,j\rangle$ satisfying the following.
$x,y,z\in\mathbb R$;
y encodes a complete Henkin theory $S_y$ of a pointwise definable $L$-structure $R_y$ such that $\sigma\in S_y$, where $\sigma$ is the $L$-sentence $c_4\Vdash_{\text{Col}(\omega,c_0)}(1\Vdash_{\text{Col}(\omega,c_1)}\forall v\langle c_3,v\rangle\in p[c_2])$;
z encodes a proof of the $\Sigma^1_1(x,y)$ sentence saying that there exists an $R_y$-generic $h\subseteq\text{Col}(\omega,c_0)^{R_y}$ such that $x=(c_3^{R_y})^h$ and $c_4^{R_y}\in h$;
$j:R_y\to M|(\gamma+1)$ is an elementary embedding such that $j(\langle c_0^{R_y},c_1^{R_y},c_2^{R_y}\rangle)=\langle \xi,\eta,T \rangle$.

Now, let’s see that this actually works, so let $x\in p[U]$. We need to show that $x\in\forall^{\mathbb R}A$, so let $y\in\mathbb R$ be arbitrary. By definition of U we have an embedding $j:R\to M$ such that, letting $\bar p:=j^{-1}(p)$ for every $p\in\text{ran}(j)$, there’s an R-generic $\bar g\subseteq\text{Col}(\omega,\bar\xi)^R$ such that $x\in R[\bar g]$ and whenever $\bar h\subseteq\text{Col}(\omega,\bar\eta)^{R[\bar g]}$ is $R[\bar g]$-generic it holds that $R[\bar g,\bar h]\models\forall v\langle x,v\rangle\in p[\bar T]$.

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 $\sigma$ includes $y$ as well though, so we first need to catch this real. If we let $\Sigma$ be M’s iteration strategy then the pullback strategy $\Sigma^j$ makes R iterable, so that we can absorb y at $\bar\eta$, meaning that there’s an iteration $\tilde i:R\to P$ and a P-generic $\bar h\subseteq\text{Col}(\omega,\tilde i(\bar\eta))^P$ such that $y\in P[\bar h]$. We also ensure that $\text{crit}(\tilde i)>\bar\xi$, so that we don’t change any of the above forcing facts about R.

Let $i:M\to Q$ be the iteration of M corresponding to $\tilde i:R\to P$ and $\tilde j:P\to Q$ the lift of $j:R\to M$. Then elementarity of $\tilde j$ yields that there’s a Q-generic $g\subseteq\text{Col}(\omega,\xi)^Q$ such that $x\in Q[g]$ and, letting $h\subseteq\text{Col}(\omega,i(\eta))^Q$ correspond to $\bar h$, $Q[g,h]\models\forall v\langle x,v\rangle\in p[i(T)]$. But $y\in Q[g,h]$, so in particular $\langle x,y\rangle\in p[i(T)]$. As M understands A via T and y was arbitrary this means that $x\in\forall^{\mathbb R}A$.

Now, for the other inclusion, let $x\in\forall^{\mathbb R}A\cap M[g]$ — we want to show that $x\in p[U]$. Since M Suslin-captures A at $\eta$ via T we get that $M\models\sigma$, where $\langle c_0^M,c_1^M,c_2^M,c_3^M,c_4^M\rangle=\langle \xi,\eta,T,\tau,p\rangle$, where $x=\tau^g$ and $p\in g$ is some condition. As $M|\gamma\models\textsf{KP}$ it can define wellfounded parts of relations belonging to it, so that $M|(\gamma+1)\models\sigma$ as well. Now, working in M[g] we can find $\tilde j:R[g]\to M|(\gamma+1)[g]$ with R countable and everything relevant in $\text{ran}(j)$. Let $j:=\tilde j\upharpoonright R$, $z\in\mathbb R$ encode a proof of $x=(c_3^R)^g$ and $y\in\mathbb R$ encode the $L$-theory of R. It’s then clear that $\langle x,y,z,j\rangle\in[U]$

The proof of the $\exists^{\mathbb R}A$ case is nearly identical. We simply replace the universal quantifier in $\sigma$ with an existential one, and without having to catch $y$. QED