= Solution
We use only the definability and truth clauses of the <forcing theorem>. For every formula, its <forcing> relation on names is definable inside $M$; <forcing> is preserved by strengthening; and $M[G]\models\varphi(\vec\tau^G)$ exactly when some condition in $G$ forces $\varphi(\vec\tau)$. These clauses do not presuppose the Separation axiom we are proving.
Let $a=\tau^G$ and let $\vec\sigma^G$ be the parameters in the desired instance. In $M$, form the name
$$
\rho=\{(\nu,q):\exists p\,[(\nu,p)\in\tau\ \land\ q\ge p
\ \land\ q\Vdash\varphi(\nu,\vec\sigma)]\}.
$$
This is a set in $M$ by its Separation axiom and <forcing> definability, using the subnames of $\tau$ and $P$ as a set-sized bound.
If $x\in\rho^G$, some $q\in G$ activates $(\nu,q)$ and $q\ge p$ activates $(\nu,p)\in\tau$. Thus $x=\nu^G\in a$, and the <forcing> theorem gives $\varphi(x,\vec\sigma^G)$. Conversely, if $x\in a$ satisfies that formula, choose an active pair $(\nu,p)\in\tau$ with $x=\nu^G$ and a condition $r\in G$ <forcing> the formula. Directedness gives $q\in G$ stronger than both $p$ and $r$. Monotonicity puts $(\nu,q)\in\rho$, so $x\in\rho^G$.
Therefore
$$
\boxed{\rho^G=\{x\in a:M[G]\models\varphi(x,\vec\sigma^G)\}.}
$$
Every requested instance of <separation in a generic extension> follows.
Back to article page
