= Solution
Assume the forcing relation and the forcing theorem have been constructed for $\varphi(x,\vec y)$. Define
$$
p\Vdash\exists x\,\varphi(x,\vec\tau)
$$
to mean that
$$
D_p=\{q\le p:\exists\sigma\in M\;q\Vdash\varphi(\sigma,\vec\tau)\}
$$
is dense below $p$. This definition is first-order over $M$, so the definability lemma is preserved.
Suppose $p\in G$ forces the existential statement. Genericity below $p$ gives $q\in G\cap D_p$ and a name $\sigma$ with $q\Vdash\varphi(\sigma,\vec\tau)$. The truth lemma for $\varphi$ yields
$$
M[G]\models\varphi(\sigma^G,\vec\tau^G),
$$
so the existential statement is true. Conversely, if $M[G]\models\exists x\,\varphi(x,\vec\tau^G)$, choose a name $\sigma$ for a witness. The truth lemma for $\varphi$ gives $q\in G$ with $q\Vdash\varphi(\sigma,\vec\tau)$, and then $q\Vdash\exists x\,\varphi(x,\vec\tau)$. This proves both directions of the forcing theorem for the existential formula.
Back to article page
