Forcing

Origin. Cohen (1963). Proved the independence of the Continuum Hypothesis and the Axiom of Choice from ZFC. A general method for building models of set theory with prescribed properties.

Models. Extend a countable transitive model of ZFC by adjoining a generic filter for a partial order of "conditions." The extension satisfies ZFC and can be made to satisfy or refute a target statement.

Formalism.

Forcing poset: (P, ≤): conditions, with q ≤ p meaning q is stronger (more information).

Generic filter: G ⊆ P a filter meeting every dense set that lies in the ground model M. Exists for countable M (not in M).

Names and interpretation: P-names τ built recursively. val_G(τ) interprets names in the extension M[G].

Forcing relation: p ⊩ φ, definable in M. Truth lemma: M[G] ⊨ φ iff some p ∈ G forces φ.

Cohen forcing: Finite partial functions adding new reals ⟹ M[G] ⊨ ¬CH. Collapsing and Lévy forcing adjust cardinals.

Preservation: ccc (countable chain condition) posets preserve cardinals and cofinalities. Iterated forcing with support builds complex models.

Boolean-valued models: V^B over a complete Boolean algebra B. Truth values in B; generic = ultrafilter.

Symbols.

Symbol	Unicode	Name	Meaning
⊩	U+22A9	Forces	Forcing relation
P, ≤	—	Poset	Conditions
G	—	Generic filter	Meets all dense sets
M[G]	—	Extension	Generic extension
V^B	—	Boolean model	Boolean-valued universe

Metatheory. M[G] satisfies ZFC (forcing preserves the axioms). Con(ZFC) ⟹ Con(ZFC + ¬CH); with the constructible universe giving Con(ZFC + CH), CH is independent. ccc guarantees cardinal preservation; proper forcing generalizes it.

Applies to. Independence and relative-consistency proofs. Cardinal arithmetic. Set-theoretic topology and combinatorics. Large-cardinal and determinacy consistency results.

Limitations. Requires a ground model; yields relative consistency, not truth. Technically intricate (names, genericity, iteration). Does not decide which axioms are "correct."