= Solution
For a countable transitive ground model, the <semantic forcing relation> is
$$
\boxed{q\Vdash_{\mathbb Q}\varphi(\vec\tau)
\ \Longleftrightarrow\
M[H']\models\varphi(\vec\tau^{H'})
\text{ for every }M\text{-generic }H'\ni q.}
$$
The <forcing theorem> identifies this with the recursively defined relation inside $M$ and makes it definable there. In particular, if $r\ge q$ is stronger, then $q\Vdash\varphi$ implies $r\Vdash\varphi$. The names are interpreted in each relevant <generic filter>, not replaced by their value in one fixed extension in the definition.
Back to article page
