# proof that “small” sets in an extension by iterated forcing already appear in an earlier stage

In Kunen's book (introduction to independence proofs, ) the following lemma is proved (chapter 8, lemma 5.14):

Assume that in M, $\alpha$ is a limit ordinal, $( ( \mathbb{P}_\xi : \xi \leq \alpha) , (\pi_\xi : \xi < \alpha) )$ is an $\alpha$-stage iterated forcing construction with supports in $\mathcal{I}$ , and each element of $\mathcal{I}$ is bounded in $\alpha$. suppose G is $\mathbb{P}_\alpha$-generic over $M \:,\: S \in M \:,\: X\subseteq S \:,\: X \in M[G] \:,\: and \: (|S| < cf(\alpha))^{M[G]}.$ then for some $\eta<\alpha \:,\: X\in M[i_{\eta\alpha}^{-1}(G)].$

the proof seemed very simple at first glance. however:

kunen shows that "for $s \in S \:,\: s \in X$ if and only if there is a $\xi = \xi_s < \alpha$ such that $\exists p \in G_\xi (i_{\xi\alpha}(p)\Vdash_{\mathbb{P}_\alpha}\check{s} \in \sigma )$".

pretty obvious. but then kunen uses this to form, in M[G] , the set $\{\xi_s : s \in X\}$. why is this set in M[G]? the "$\exists p \in G_\xi$" part is ok, since the sequence $(G_\xi : \xi < \alpha)$ is in M[G]. but the "$(i_{\xi\alpha}(p)\Vdash_{\mathbb{P}_\alpha}\check{s} \in \sigma )$" , although it is indeed definable in M by definability of forcing, it is not necessarily definable in M[G].

then he does it again by showing that X = $\{s \in S : \exists p \in G_\eta (i_{\eta\alpha}(p)\Vdash_{\mathbb{P}_\alpha}\check{s} \in \sigma ) \}$ and concluding that $X \in M[G_\eta]$, "since $\Vdash_{\mathbb{P}_\alpha}$ is defined in M " , although not necessarily in M[G].

why are these two arguments valid?

• Since $M$ is definable in $M[G]$, everything that is definable in $M$ will be also definable in $M[G]$. – Yair Hayut Oct 14 '14 at 20:42
• and why is M definable in M[G]? – user40921 Oct 14 '14 at 20:48
• (it is, if e.g. M satisfies V=L, but I don't think it's generally true) – user40921 Oct 14 '14 at 20:54
• – Yair Hayut Oct 14 '14 at 20:59
• Very interesting, thank you! It seems the second part of Joel's answer solves the problem, although one would expect a much simpler explanation (and indeed there is, somehow evading my notice until now). by the way, I didn't quite understand (in the first part of Joel's answer) if (and how) the new predicate $\check{M}$ can be used to define M in M[G] (and not just refer to M in the forcing language) – user40921 Oct 14 '14 at 22:13

Another way to argue is simply that the forcing relation is definable in the ground model $M$, and so the part of it to which you want to appeal forms a set in $M$, and this set still exists in $M[G]$. So you can use this relation in $M[G]$ when constructing other sets.
Just noticed that $p \Vdash^* \phi$ (kunen's auxiliary notation for syntactic forcing ) is absolute for quantifier-free $\phi$. this means that $i_{\xi\alpha}(p)\Vdash_{\mathbb{P}_\alpha}\check{s} \in \sigma$ is equivalent to $(i_{\xi\alpha}(p)\Vdash^*_{\mathbb{P}_\alpha}\check{s} \in \sigma )^{M}$ which by absoluteness is equivalent to $(i_{\xi\alpha}(p)\Vdash^*_{\mathbb{P}_\alpha}\check{s} \in \sigma )^{M[G]}$