Forcing
Forcing, introduced by Paul Cohen in 1963, is the primary technique for proving independence results in set theory. It constructs new models of set theory (generic extensions) by adjoining "generic" objects, analogous to field extensions in algebra.
Forcing Posets
A forcing notion (or partial order) is a triple where is a set of conditions, is a partial order on ( means extends/is stronger than ), and is the weakest condition. Two conditions are compatible if there exists with and .
A set is dense if for every , there exists with . A filter is -generic (for a ground model ) if meets every dense set . The generic extension is the smallest model of ZFC containing both and .
Cohen Forcing
Cohen forcing uses : conditions are finite partial functions from to , ordered by reverse inclusion. A generic filter determines a new function (a "Cohen real") not in the ground model. This shows that the continuum hypothesis can fail: by adding many Cohen reals to a model of CH, one obtains a model where .
The forcing relation means "condition forces that holds in the generic extension." This is defined recursively on formulas and satisfies: if and is generic with , then . The truth lemma states: iff some forces .
A forcing satisfies the countable chain condition (c.c.c.) if every antichain in (set of pairwise incompatible conditions) is countable. c.c.c. forcing preserves all cardinals from the ground model, which is crucial for controlling the cardinal structure of the extension.