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?

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

2 Answers 2

Reset to default
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.

Improve this answer
$\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]}$

Improve this answer
$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .