 Forcing

Forcing constructs a generic extension $M[G]$ of a model of a first-order theory of set theory from a partially ordered set $\mathbb{P}$ in $M$. A condition specifies partial information about a new object; in the standard order, $q\le p$ means that $q$ specifies stronger information. A generic filter $G$ meets every dense subset of a forcing order belonging to $M$. The elements of $M[G]$ are obtained by evaluating forcing names from $M$ using $G$.

For Cohen forcing, conditions are finite partial functions from $\omega$ to $\{0,1\}$. Their union is a new binary sequence. Dense requirements make the sequence total and ensure that it differs from each old binary sequence. When $M$ is a countable transitive model, one can enumerate its dense sets externally and successively choose stronger conditions meeting them. This construction is conditional on having such a model; consistency of ZFC alone does not assert the existence of a countable transitive model.

The forcing theorem makes this method useful for proofs: the forcing relation is definable in the ground model, and truth in the generic extension is witnessed by a condition in the generic filter.