Forcing theorem

The forcing theorem identifies truth in a generic extension with the forcing relation: a formula is true in $M[G]$ exactly when some condition in $G$ forces it.

For a name with finitely many possible values, record which value each condition forces, using an extra marker for undecided conditions. Equal patterns mean that any condition deciding one entry decides all entries with that pattern identically.

A generic extension of a transitive model has exactly the same ordinals as its ground model. Rank induction on names bounds every value; transitivity and agreement on membership make ordinalhood absolute.

A formula holds in a generic extension exactly when some condition in the generic filter forces it for names of its parameters.

For each formula, its forcing relation on names and conditions is uniformly first-order definable inside the ground model. This permits ground-model separation and replacement using forcing predicates.

For a countable transitive model $M$, semantic forcing declares $p⊩\phi$ when every generic filter $G$ over $M$ containing $p$ gives $M[G]\models \phi$.

The syntactic forcing relation is defined recursively inside the ground model from the ranks of forcing names and the logical complexity of $\phi$. The forcing theorem proves that it agrees with the semantic forcing relation.

For forcing names $\sigma ,\tau$ and a generic filter $G$, ${\sigma }^G\in {\tau }^G$ exactly when some $p\in G$ syntactically forces $\sigma \in \tau$. Assuming the equality truth lemma, interpreted membership supplies an active pair $(\rho ,r)\in \tau$ and a condition in $G$ forcing $\sigma =\rho$; a common strengthening forces membership. Conversely the defining equality witnesses occur dense below a forcing condition forcing membership. The dense-below generic meeting lemma supplies one in $G$, and the equality truth lemma recovers interpreted membership.

For the usual recursive syntactic forcing relation, $p{⊩}^{\ast }\exists x\phi (x)$ means that conditions $q\le p$ forcing $\phi (\sigma )$ for some forcing name $\sigma$ are dense below a forcing condition $p$. This density clause proves the existential step of the forcing theorem from the truth lemma for each named instance. A generic filter containing $p$ meets that dense set after it is augmented by conditions incompatible with $p$.

Let $\dot{x},{\dot{a}}_1,\dots ,{\dot{a}}_n$ be forcing names and let $\phi$ be a formula. The namebelongs to the ground model by axiom schema of separation. The forcing theorem shows that its value in a generic extension is exactlyConsequently every generic extension satisfies the separation schema.