Cohen forcing: independence of the Continuum Hypothesis

In 1900 David Hilbert listed the Continuum Problem as first among 23 major mathematical challenges. In 1963 a 29-year-old Paul Cohen proved its undecidability from ZFC -- the only mathematician to receive the Fields Medal for work in mathematical logic.

• Forcing is used in program verification: forcing extensions model nondeterminism.
• In complexity theory, forcing-style arguments appear in oracle separation results (Baker-Gill-Solovay 1975).

Partially ordered sets and forcing conditions

Paul Cohen received the Fields Medal in 1966 for proving the independence of CH from ZFC. His forcing method builds a new model V[G] from the base model V by adding a 'generic' element G -- a filter over a partially ordered set (poset) P. In the extended universe one can control the cardinality of 2^aleph_0, proving ZFC does not fix its value.

Independence of CH: proof structure

Two ingredients are needed: (1) consistency of CH with ZFC (Godel 1938: in the constructive universe L, CH holds); (2) consistency of negCH with ZFC (Cohen 1963: forcing adds aleph_2 new subsets of omega). Together: Con(ZFC) => (Con(ZFC + CH) and Con(ZFC + negCH)).

Key results

• Forcing builds extension V[G] by adding generic filter G over poset P.
• The forcing relation ||- is definable in V and controls truth in V[G].
• Cohen (1963) + Godel (1938) together give full independence of CH from ZFC.
• Easton's theorem: 2^aleph_0 can equal any aleph with uncountable cofinality.