Forcing (source code)
= Forcing
{wiki=Forcing_(mathematics)}
<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\leq 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>.
Back to article page
