 Solution

Assume the forcing relation and the forcing theorem have been constructed for $\phi (x,\vec{y})$. Defineto mean thatis 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⊩\phi (\sigma ,\vec{\tau })$. The truth lemma for $\phi$ yieldsso the existential statement is true. Conversely, if $M[G]\models \exists x\phi (x,{\vec{\tau }}^G)$, choose a name $\sigma$ for a witness. The truth lemma for $\phi$ gives $q\in G$ with $q⊩\phi (\sigma ,\vec{\tau })$, and then $q⊩\exists x\phi (x,\vec{\tau })$. This proves both directions of the forcing theorem for the existential formula.