= Solution
Fix names $\dot x,\dot a_1,\ldots,\dot a_n\in M$ and a <first-order formula> $\varphi$. Using the <syntactic forcing relation>, form in $M$ the name
$$
\dot y=\{(\tau,r):\exists q\,((\tau,q)\in\dot x\land r\leq q\land r\Vdash^*\varphi(\tau,\dot a_1,\ldots,\dot a_n))\}.
$$
This is a set by the <axiom schema of separation> in $M$. If $(\tau,r)\in\dot y$ and $r\in G$, then the <forcing theorem> gives both $\tau^G\in\dot x^G$ and $\varphi(\tau^G,\dot a_1^G,\ldots,\dot a_n^G)$. Conversely, if $z\in\dot x^G$ satisfies $\varphi$, choose $(\tau,q)\in\dot x$ with $q\in G$ and $\tau^G=z$. The truth direction of the forcing theorem supplies $s\in G$ forcing $\varphi(\tau,\dot a_1,\ldots,\dot a_n)$; directedness of $G$ gives $r\in G$ below both $q$ and $s$, so $(\tau,r)\in\dot y$.
Thus
$$
\dot y^G=\{z\in\dot x^G:M[G]\models\varphi(z,\dot a_1^G,\ldots,\dot a_n^G)\}.
$$
Every instance has such a witness, so <separation in a generic extension> proves \b[$M[G]\models$ Separation.]
Back to article page
