Generic extension

If $G$ is a generic filter over a countable transitive model $M$, the generic extension $M[G]$ consists of the interpretations by $G$ of all forcing names in $M$.

Let $M_{n+1}=M_n[G_n]$ for a fixed atomless forcing order $\mathbb{P}$, and $N={\bigcup }_{n<\omega }{M}_n$. If a set $A\in N$ were its internal power set of $\mathbb{P}$, choose $n$ with $A\in M_n$. The next generic filter $G_n$ belongs to $N$, so $G_n\in A$; transitivity of $M_n$ implies $G_n\in M_n$, contradicting generic filter for an atomless order is new. The chain is increasing but need not be an elementary chain.

For a forcing name $\tau$, let $U$ consist of pairs $(\rho ,p)$ where $(\rho ,r)\in \tau$ for some $r\ge p$. Every ground-model subset $\nu$ of $U$ is a name whose value is contained in ${\tau }^G$. Every subset ${\sigma }^G\subseteq {\tau }^G$ has an equivalent such name: retain those $(\rho ,p)\in U$ with $p⊩\rho \in \sigma$. The atomic membership truth lemma for forcing proves equality of values. Collect all these names from the ground-model power set ${\mathcal{P}}^M(U)$ into a single outer name, pairing each with every condition. Its value is the full internal power set, without presupposing that power set in the extension.

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.