= Solution
The <forcing theorem> has two central clauses. \b[Definability:] for each <first-order formula> $\varphi$, the relation $p\Vdash\varphi(\vec\tau)$ on conditions and ground-model names is first-order definable in $M$. \b[Truth lemma:] for every $M$-generic $G$ and every tuple of names in $M$,
$$
\boxed{M[G]\models\varphi(\vec\tau^G)
\quad\Longleftrightarrow\quad
\exists p\in G\ (p\Vdash\varphi(\vec\tau)).}
$$
<Forcing> is monotone under strengthening and agrees with the generic-extension semantics. Together with the generic model construction, $M[G]$ is a <transitive model> of <ZFC> containing $M$ with the same <ordinals>. The definability and truth clauses are the auxiliary parts used when proving individual extension axioms.
Back to article page
