9.1 Forcing

Forcing is a method for constructing new models of set theory from old ones by adjoining new sets in a controlled way, and its main purpose is to show that certain statements cannot be decided from a given list of axioms, such as ZFC, provided those axioms are consistent.

The guiding idea is that we begin with a model $M$ of set theory and a partially ordered set $\mathbb{P}$ whose elements are called conditions, where a condition gives finite or partial information about a new object that we want to add to the model.

Definition 9.1 (Forcing Poset)

A forcing poset is a partially ordered set:

whose elements are called conditions.

If $p,q \in \mathbb{P}$ and:

then $q$ is called stronger than $p$.

The order is read this way because $q$ gives at least as much information as $p$, and usually it gives more information.

Example 9.2 (Adding a New Subset of Natural Numbers)

Let:

be the set of all finite binary sequences.

For $p,q \in 2^{<\omega}$, define:

if and only if $q$ extends $p$ as a sequence.

Thus:

because the longer sequence gives more information about the infinite binary sequence being constructed.

A generic filter through this poset will determine an infinite binary sequence:

and this can be identified with a subset of $\omega$.

Definition 9.3 (Compatible Conditions)

Two conditions $p,q \in \mathbb{P}$ are compatible if there exists a condition $r \in \mathbb{P}$ such that:

If no such $r$ exists, then $p$ and $q$ are incompatible.

Compatibility means that the information given by $p$ and the information given by $q$ can be combined into a single stronger condition.

Definition 9.4 (Dense Set)

A subset $D \subseteq \mathbb{P}$ is dense if for every $p \in \mathbb{P}$ there exists $q \in D$ such that:

Thus a dense set is a set of conditions that cannot be avoided by strengthening a condition.

Dense sets express requirements that a generic object should meet.

Definition 9.5 (Filter)

A subset $G \subseteq \mathbb{P}$ is a filter if it satisfies the following conditions.

First, $G$ is upward closed in the forcing order:

where $q$ is weaker than $p$.

Second, $G$ is directed:

The first condition says that if a filter contains a strong condition, then it also contains every weaker condition that is already implied by it.

The second condition says that any two pieces of information in the filter can be combined.

Definition 9.6 (Generic Filter)

Let $M$ be a model of set theory, and let $\mathbb{P} \in M$ be a forcing poset.

A filter $G \subseteq \mathbb{P}$ is $M$ generic if:

for every dense set $D \subseteq \mathbb{P}$ such that $D \in M$.

The filter $G$ is usually not an element of $M$. Instead, it is chosen outside $M$ while meeting every dense requirement that $M$ can describe.

Lemma 9.7 (Existence of Generic Filters for Countable Models)

Let $M$ be a countable model of a sufficiently large finite fragment of ZFC, and let $\mathbb{P} \in M$ be a forcing poset. If $p_0 \in \mathbb{P}$, then there exists an $M$ generic filter $G \subseteq \mathbb{P}$ such that:

Proof

Since $M$ is countable, the collection of dense subsets of $\mathbb{P}$ that belong to $M$ is also countable from the outside.

List them as:

We build a descending sequence of conditions:

such that:

for each $n$.

Assume $p_n$ has been chosen. Since $D_n$ is dense, there exists:

such that:

Now define:

This set contains $p_0$, because $p_0 \leq p_0$.

It is upward closed by definition. If $q \in G$ and $q \leq r$, then for some $n$ we have $p_n \leq q$, and therefore $p_n \leq r$, so $r \in G$.

It is directed. If $q,r \in G$, then there exist $m,n$ such that:

Let $k$ be larger than both $m$ and $n$. Since the sequence is descending:

so:

and $p_k \in G$.

Finally, $G$ meets each dense set $D_n$, because $p_{n+1} \in D_n$ and $p_{n+1} \in G$.

Hence $G$ is an $M$ generic filter containing $p_0$.

Definition 9.8 (Forcing Names)

Let $M$ be a model of set theory and let $\mathbb{P} \in M$ be a forcing poset.

A $\mathbb{P}$ name is a set $\tau$ whose elements are ordered pairs:

where $\sigma$ is a $\mathbb{P}$ name and $p \in \mathbb{P}$.

Names are defined recursively. Intuitively, a name is a formal description of an object that may appear in the forcing extension.

The condition $p$ attached to $\sigma$ says that $\sigma$ should be included in the interpretation of $\tau$ if $p$ belongs to the generic filter.

Definition 9.9 (Interpretation of Names)

Let $G \subseteq \mathbb{P}$ be a filter. The interpretation of a name $\tau$ by $G$ is defined recursively by:

Thus a name becomes an actual set once a generic filter has been chosen.

Definition 9.10 (Canonical Names)

For each set $x \in M$, define its canonical name $\check{x}$ recursively by:

where $1_{\mathbb{P}}$ is the weakest condition, if the forcing poset has one.

The name $\check{x}$ is the formal name for the old set $x$ inside the forcing extension.

Lemma 9.11 (Canonical Names Interpret Correctly)

For every $x \in M$ and every generic filter $G$ containing $1_{\mathbb{P}}$:

Proof

We prove the statement by induction on the rank of $x$.

By definition:

Since $1_{\mathbb{P}} \in G$, the interpretation is:

By the induction hypothesis:

for every $y \in x$.

Therefore:

This proves the claim.

Definition 9.12 (The Generic Extension)

Let $M$ be a model of set theory, let $\mathbb{P} \in M$, and let $G$ be an $M$ generic filter.

The forcing extension $M[G]$ is defined by:

The model $M[G]$ contains every old set from $M$ through its canonical name, and it also contains new sets whose names are interpreted using $G$.

Lemma 9.13

If $M$ is a model of set theory, $\mathbb{P} \in M$, and $G$ is $M$ generic, then:

Proof

Let $x \in M$. By Definition 9.10, there is a canonical name $\check{x} \in M$.

By Lemma 9.11:

Since $M[G]$ contains the interpretations of all names in $M$, it follows that:

Thus:

Example 9.14 (The Generic Real)

Let:

ordered by extension.

If $G$ is an $M$ generic filter, define:

Since every condition in $G$ is a finite binary sequence and any two elements of $G$ are compatible, the union $g$ is a function.

The dense sets:

ensure that $g$ is defined at every natural number.

Each $D_n$ is dense, because any finite sequence can be extended to decide the value at $n$.

Since $G$ is generic, it meets every $D_n$, so:

Thus:

and $g$ is an infinite binary sequence.

This $g$ is called the generic real.

Lemma 9.15 (The Generic Real is Total)

Let $\mathbb{P}=2^{<\omega}$ ordered by extension, and let $G$ be $M$ generic. Then:

is a total function from $\omega$ to $2$.

Proof

First, $g$ is a function. If two finite sequences $p,q \in G$ assign values to the same input $n$, then directedness gives some $r \in G$ such that:

Since $r$ extends both $p$ and $q$, the values assigned by $p$ and $q$ at $n$ must agree. Therefore the union is functional.

Second, $g$ is total. For each $n \in \omega$, define:

This set is dense. Given any finite binary sequence $p$, we may extend it to a finite binary sequence $q$ whose domain includes $n$, and then:

Since $G$ is $M$ generic and $D_n \in M$, we have:

Thus some condition in $G$ assigns a value to $n$, so $n \in \mathrm{dom}(g)$.

Since this holds for every $n$, the function $g$ has domain $\omega$.

Definition 9.16 (The Forcing Relation)

The forcing relation is written:

and read as:

It means that the condition $p$ contains enough information to guarantee that $\varphi$ will be true in every generic extension containing $p$.

More precisely, if $\varphi$ is a formula in the forcing language with names as parameters, then:

means that for every $M$ generic filter $G$ with $p \in G$:

This is the semantic reading. In formal development, the forcing relation is defined recursively inside $M$, so that one can reason about forcing without quantifying over all external generic filters.

Lemma 9.17 (Monotonicity of Forcing)

If:

and:

then:

Proof

Assume:

and:

Let $G$ be any $M$ generic filter such that:

Since $G$ is upward closed and $q \leq p$, it follows that:

Because $p \Vdash \varphi$, every generic extension by a generic filter containing $p$ satisfies $\varphi$.

Therefore:

Since $G$ was arbitrary among generic filters containing $q$, we conclude:

Lemma 9.18 (Density Principle)

Let $D \subseteq \mathbb{P}$ be dense below $p$, meaning that for every $q \leq p$ there exists $r \leq q$ such that $r \in D$.

If every condition in $D$ forces $\varphi$, then:

Proof

Let $G$ be an $M$ generic filter such that:

Since $D$ is dense below $p$, the set:

is dense in $\mathbb{P}$, where $q \perp p$ means that $q$ is incompatible with $p$.

Because $G$ is generic, it meets $E$.

Since $p \in G$, no condition in $G$ can be incompatible with $p$, because $G$ is directed.

Therefore $G$ must meet $D$.

Choose:

By assumption:

Since $r \in G$, it follows from the meaning of forcing that:

Thus every generic extension containing $p$ satisfies $\varphi$, so:

Definition 9.19 (Forcing Extension Theorem)

The fundamental theorem of forcing says that if $M$ is a suitable model of ZFC, $\mathbb{P} \in M$ is a forcing poset, and $G$ is $M$ generic, then $M[G]$ is again a model of ZFC, and the truth of formulas in $M[G]$ is controlled by the forcing relation.

More precisely, for each formula $\varphi$ and names $\tau_1,\dots,\tau_n \in M$:

if and only if there exists $p \in G$ such that:

This result is often called the truth lemma together with the forcing theorem.

Theorem 9.20 (Truth Lemma)

Let $M$ be a countable transitive model of a sufficiently large fragment of ZFC, let $\mathbb{P} \in M$, and let $G$ be $M$ generic. If:

then there exists $p \in G$ such that:

Proof

The full proof is by induction on the complexity of the formula $\varphi$.

For atomic formulas, one defines the forcing relation recursively for statements of the form:

and:

The definition is arranged so that the truth of these atomic statements in $M[G]$ is reflected by some condition in $G$.

For negation, suppose:

If no condition in $G$ forced $¬\psi$, then every condition in $G$ would have a stronger condition compatible with forcing $\psi$, and by genericity one could find an extension witnessing $\psi$, contradicting:

Thus some condition in $G$ forces $¬\psi$.

For conjunction, suppose:

Then:

and:

By the induction hypothesis, there exist $p,q \in G$ such that:

and:

Since $G$ is directed, there exists $r \in G$ with:

By monotonicity:

and:

Hence:

For existential quantification, suppose:

Then there is some object $a \in M[G]$ such that:

By the definition of $M[G]$, there is a name $\sigma \in M$ such that:

By the induction hypothesis, there exists $p \in G$ such that:

Therefore:

The cases for other connectives and universal quantification are reduced to these by logical equivalences.

Theorem 9.21 (Basic Extension Theorem)

Let $M$ be a countable transitive model of ZFC, let $\mathbb{P} \in M$ be a forcing poset, and let $G$ be an $M$ generic filter. Then:

provided the forcing construction is carried out inside a setting where the required forcing theorem holds for $M$.

Proof

The proof verifies each axiom of ZFC in $M[G]$.

Extensionality holds because equality in $M[G]$ is ordinary equality of interpreted sets.

Empty Set holds because the canonical name $\check{\varnothing}$ belongs to $M$, and:

Pairing holds because if $a,b \in M[G]$, then there are names $\sigma,\tau \in M$ such that:

The name:

belongs to $M$, and:

Union holds by defining, inside $M$, a name whose interpretation collects all elements of elements of a given interpreted name.

Infinity holds because:

and $\omega \in M$.

Separation holds by using the forcing theorem. Given a set $a=\tau^G$ and a formula $\varphi(x)$, one defines a name in $M$ for:

by using conditions that force $\varphi$ of the relevant name.

Replacement is proved similarly but requires more bookkeeping, since one must show that images of sets under definable functions are still represented by names in $M$.

Power Set holds by using names for subsets and the fact that the collection of relevant names can be bounded in rank inside $M$.

Foundation holds because $M[G]$ is built from well founded names interpreted recursively.

Choice is preserved when the forcing extension is built over a model of ZFC, since well orderings in $M$ can be extended to well order the interpreted universe by ranking names and using the well ordering available in $M$.

Thus each axiom of ZFC holds in $M[G]$.

Why Forcing Proves Independence

Forcing proves independence by producing two models of the same axioms in which a statement has different truth values.

Suppose $T$ is a theory such as ZFC and $\varphi$ is a sentence.

If one can build a model:

and another model:

then $T$ cannot prove $\varphi$ and cannot prove $¬\varphi$, assuming $T$ is consistent.

This is because if $T$ proved $\varphi$, then every model of $T$ would satisfy $\varphi$ by soundness.

Similarly, if $T$ proved $¬\varphi$, then every model of $T$ would satisfy $¬\varphi$.

Forcing gives a systematic way to construct such models by choosing different forcing posets and generic filters.

Theorem 9.22 (Independence Pattern)

Let $T$ be a sound first order theory extending enough set theory, and let $\varphi$ be a sentence. Suppose there exist models:

and:

Then neither $\varphi$ nor $¬\varphi$ is provable from $T$.

Proof

Assume first that:

By soundness of first order logic, every model of $T$ satisfies $\varphi$.

But:

so:

This contradicts the conclusion that every model of $T$ satisfies $\varphi$.

Therefore:

Now assume:

Again by soundness, every model of $T$ satisfies $¬\varphi$.

But:

so:

This is a contradiction.

Therefore:

Hence $\varphi$ is independent of $T$.

Cohen Forcing and the Continuum Hypothesis

The original application of forcing was Cohen’s proof that the continuum hypothesis cannot be proved from ZFC, assuming ZFC is consistent.

The continuum hypothesis is the statement:

It says that there is no cardinal strictly between the cardinality of the natural numbers and the cardinality of the real numbers.

Forcing can add new real numbers to a model. By adding sufficiently many reals while preserving the axioms of ZFC, one can build a forcing extension in which:

Thus the continuum hypothesis fails in that extension.

Combined with Gödel’s earlier construction of the constructible universe $L$, where the continuum hypothesis holds, this gives the independence of the continuum hypothesis from ZFC, assuming ZFC is consistent.

Conceptual Summary

The forcing method has four main components.

First, the forcing poset $\mathbb{P}$ describes finite or partial approximations to the object being added.

Second, the generic filter $G$ selects a coherent collection of conditions meeting every dense requirement visible in the ground model.

Third, forcing names provide formal descriptions of objects in the extension before the generic filter has been chosen.

Fourth, the forcing relation $p \Vdash \varphi$ connects conditions with truth in the extension by saying that $p$ guarantees $\varphi$ in every generic extension containing it.