3
$\begingroup$

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?

$\endgroup$
5
  • $\begingroup$ Since $M$ is definable in $M[G]$, everything that is definable in $M$ will be also definable in $M[G]$. $\endgroup$ – Yair Hayut Oct 14 '14 at 20:42
  • $\begingroup$ and why is M definable in M[G]? $\endgroup$ – user40921 Oct 14 '14 at 20:48
  • $\begingroup$ (it is, if e.g. M satisfies V=L, but I don't think it's generally true) $\endgroup$ – user40921 Oct 14 '14 at 20:54
  • 1
    $\begingroup$ see mathoverflow.net/questions/78751/name-for-the-ground-model $\endgroup$ – Yair Hayut Oct 14 '14 at 20:59
  • $\begingroup$ 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) $\endgroup$ – user40921 Oct 14 '14 at 22:13
3
$\begingroup$

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.

$\endgroup$
3
$\begingroup$

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]}$

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.