Proof that Forcing Extensions Model ZFC

A central fact of forcing is that the generic extension $M[G]$ satisfies ZFC whenever the ground model $M$ does. We outline the verification of the key axioms.

Statement

Theorem7.3Generic Extension Models ZFC

Let $M$ be a countable transitive model of ZFC, $\mathbb{P} \in M$ a forcing notion, and $G$ an $M$ -generic filter on $\mathbb{P}$ . Then $M[G]$ is a countable transitive model of ZFC with $M \subseteq M[G]$ and $G \in M[G]$ .

Proof Outline

Proof

$M[G]$ is defined as $\{\tau_G : \tau \in M^{\mathbb{P}}\}$ where $\tau$ ranges over $\mathbb{P}$ -names in $M$ and $\tau_G$ is the evaluation of $\tau$ by $G$ .

Extensionality and Foundation: $M[G]$ is transitive (by construction), so these axioms hold.

Pairing and Union: Given $\mathbb{P}$ -names $\sigma, \tau$ , one constructs names for $\{\sigma_G, \tau_G\}$ and $\bigcup \sigma_G$ within $M$ .

Power Set: For a name $\sigma$ , the name for $\mathcal{P}(\sigma_G) \cap M[G]$ exists because every subset of $\sigma_G$ in $M[G]$ has a "nice name" (a name built from antichains), and the collection of nice names is a set in $M$ .

Infinity: The name for $\omega$ is $\check{\omega}$ , and $\omega \in M[G]$ .

Replacement: If $\varphi$ defines a function in $M[G]$ , the Forcing Theorem ensures that for each input there is a condition forcing the output. Using the maximum principle (for c.c.c. forcings) or mixing lemma, one collects these outputs into a set.

Separation: Follows from the forcing relation being definable in $M$ .

Choice: The well-ordering of the ground model can be extended to $M[G]$ using the forcing relation and the fact that every element of $M[G]$ has a name in $M$ . $\square$

■

Key Tools

Definition7.4The Forcing Theorem (Truth Lemma)

For any formula $\varphi$ and $M$ -generic $G$ : $M[G] \models \varphi$ if and only if there exists $p \in G$ such that $p \Vdash_\mathbb{P} \varphi$ . Moreover, the forcing relation $\Vdash$ is definable in $M$ .

RemarkWhy Genericity is Needed

The requirement that $G$ meet every dense set in $M$ is essential. Without genericity, $M[G]$ might fail Separation or Replacement. Genericity ensures that the forcing relation correctly predicts truth in the extension. The existence of generic filters follows from $M$ being countable (and hence having only countably many dense sets).

ExampleBoolean-Valued Models

An alternative approach avoids generic filters entirely: replace the 2-valued truth in set theory with truth values in a complete Boolean algebra $\mathbb{B}$ . The Boolean-valued model $V^{\mathbb{B}}$ is an inner model where every statement has a truth value in $\mathbb{B}$ , and the quotient by an ultrafilter on $\mathbb{B}$ recovers the generic extension. This approach, due to Scott and Solovay, avoids the need for countable ground models.