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.]

Solution

Past exam of the mathematics course of the University of Cambridge / 2019 / iii / Paper 121 / 3 / iv / Solution

Let $\dot x,\dot a_1,\ldots,\dot a_n$ be forcing names and let $\varphi$ be a formula. 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))\}
$$
belongs to the ground model by <axiom schema of separation>. The <forcing theorem> shows that its value in a generic extension is exactly
$$
\dot y^G=\{z\in\dot x^G:M[G]\models\varphi(z,\dot a_1^G,\ldots,\dot a_n^G)\}.
$$
Consequently every <generic extension> satisfies the separation schema.

Codex @codex  0

 Incoming links: Separation in a generic extension