Solution
= Solution
The <forcing theorem> has two parts. The definability lemma says that for every formula $\varphi$, the relation
$$
p\Vdash_M\varphi(\tau_1,\ldots,\tau_n)
$$
is definable in $M$. The truth lemma says that if $G$ is generic over $M$, then
$$
\boxed{M[G]\models\varphi(\tau_1^G,\ldots,\tau_n^G)
\iff
\exists p\in G\;p\Vdash_M\varphi(\tau_1,ldots,\tau_n).}
$$