Past exam of the mathematics course of the University of Cambridge / 2013 / iii / Paper 19 / 4 / ii

The generic extension is $M[G]=\{{\tau }^G:\tau \in M\text{ is a forcing name}\}$. It is transitive: if $x\in {\tau }^G$, an active pair in $\tau$ supplies a subname $\sigma \in M$ with $x={\sigma }^G$. Ground sets belong to it by their canonical names. Without assuming a weakest condition, use $\check{a}=\{(\check{b},p):b\in a,p\in P\}$; nonemptiness of $G$ gives ${\check{a}}^G=a$.

Induction on forcing name rank gives $\mathrm{rank}({\tau }^G)\le \mathrm{nrk}(\tau )$. The right side is an ordinal of $M$. If $\alpha \in M[G]$ is an ordinal, its rank equals $\alpha$, so it is at most a ground-model ordinal. Transitivity of $M$ then implies $\alpha \in M$. Conversely every ground ordinal remains the same ordinal in the transitive extension, since membership is unchanged. HenceThis proves forcing preserves ordinals directly from ranks, without assuming cardinal preservation.

We use only the definability and truth clauses of the forcing theorem. For every formula, its forcing relation on names is definable inside $M$; forcing is preserved by strengthening; and $M[G]\models \phi ({\vec{\tau }}^G)$ exactly when some condition in $G$ forces $\phi (\vec{\tau })$. These clauses do not presuppose the Separation axiom we are proving.

Let $a={\tau }^G$ and let ${\vec{\sigma }}^G$ be the parameters in the desired instance. In $M$, form the nameThis is a set in $M$ by its Separation axiom and forcing definability, using the subnames of $\tau$ and $P$ as a set-sized bound.

If $x\in {\rho }^G$, some $q\in G$ activates $(\nu ,q)$ and $q\ge p$ activates $(\nu ,p)\in \tau$. Thus $x={\nu }^G\in a$, and the forcing theorem gives $\phi (x,{\vec{\sigma }}^G)$. Conversely, if $x\in a$ satisfies that formula, choose an active pair $(\nu ,p)\in \tau$ with $x={\nu }^G$ and a condition $r\in G$ forcing the formula. Directedness gives $q\in G$ stronger than both $p$ and $r$. Monotonicity puts $(\nu ,q)\in \rho$, so $x\in {\rho }^G$.

ThereforeEvery requested instance of separation in a generic extension follows.