= Solution
{c}
For the reverse implication, suppose $p\in G$ and $M\models p\Vdash^*\exists x\,\varphi(x)$. By the <existential clause of syntactic forcing>, the set
$$
D=\{q\leq p:M\models\exists\sigma\;(q\Vdash^*\varphi(\sigma))\}
$$
is dense below $p$; the existential quantifier ranges over <forcing names> of $M$. Definability of the <syntactic forcing relation> and <axiom schema of separation> put $D$ in $M$.
To apply genericity, augment it to the globally dense set
$$
D'=D\cup\{q\in\mathbb P:q\perp p\}.
$$
A condition compatible with $p$ has an extension below $p$, then one in $D$, and an incompatible condition already lies in $D'$. Thus $D'$ is a <dense subset of a forcing order> in $M$. The <generic filter> meets it. Since $p\in G$, directedness prevents $G$ from containing a condition incompatible with $p$, so some $q\in G\cap D$ exists.
There is consequently a name $\sigma\in M$ with $M\models q\Vdash^*\varphi(\sigma)$. The assumed truth lemma gives $M[G]\models\varphi(\operatorname{val}(\sigma,G))$, and hence
$$
\boxed{\exists p\in G\;M\models p\Vdash^*\exists x\,\varphi(x)\quad\Longrightarrow\quad M[G]\models\exists x\,\varphi(x).}
$$
Together with part (a), this completes the existential step of the <forcing theorem> without assuming the desired existential truth lemma in advance.
Back to article page
