= Solution
Fix <forcing names> $\tau,\tau_1,\ldots,\tau_n\in M$ for the set $w$ and the parameters. Define a name
$$
\sigma=\{(\eta,p):\exists q\ ((\eta,q)\in\tau,\ p\leq q,
\ p\Vdash\varphi(\eta,\tau,\tau_1,\ldots,\tau_n))\}.
$$
Only $\eta$ appearing in $\tau$ and $p\in\mathbb P$ are needed, so this is a subset of a ground-model set. The <forcing definability lemma> makes its defining predicate a formula of $M$. Ground-model <axiom schema of separation> therefore gives $\sigma\in M$.
If $(\eta,p)\in\sigma$ with $p\in G$, the accompanying $q\geq p$ belongs to $G$, so $\eta_G\in\tau_G$. The <forcing theorem> gives $\varphi(\eta_G,\tau_G,(\tau_1)_G,\ldots,(\tau_n)_G)$.
Conversely, if $u\in\tau_G$ satisfies this formula, choose $(\eta,q)\in\tau$ with $q\in G$ and $\eta_G=u$. The <forcing truth lemma> supplies $r\in G$ forcing the formula for these names. Directedness gives $p\in G$ with $p\leq q,r$. Then $(\eta,p)\in\sigma$, and $u\in\sigma_G$. Thus
$$
\boxed{\sigma_G=\{u\in w:\varphi(u,w,v_1,\ldots,v_n)\}.}
$$
This proves the instance of the <axiom schema of separation> in the <generic extension>, without assuming that instance there in order to construct the name.
Back to article page
