= Solution
The <forcing definability lemma> states that for each formula $\varphi(v_1,\ldots,v_n)$ there is a first-order formula $\mathrm{Force}_\varphi$, depending on $\varphi$ but not on the chosen names, such that for $p\in P$ and <forcing names> $\tau_i\in M$,
$$
\boxed{p\Vdash_M\varphi(\tau_1,\ldots,\tau_n)
\iff M\models\mathrm{Force}_\varphi(p,\tau_1,\ldots,\tau_n,\mathbb P).}
$$
The order relation of $\mathbb P$ is included in its set code. Thus each instance of the forcing relation is definable inside the ground model, allowing the uses of ground-model <axiom schema of separation> and replacement in the forcing arguments.
Back to article page
