Past exam of the mathematics course of the University of Cambridge / 2015 / iii / Paper 24 / 6 / a / ii

The forcing definability lemma states that for each formula $\phi (v_1,\dots ,v_n)$ there is a first-order formula ${\mathrm{Force}}_{\phi }$, depending on $\phi$ but not on the chosen names, such that for $p\in P$ and forcing names ${\tau }_i\in M$,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.