Forcing

Origin. Cohen (1963). Proved the independence of the Continuum Hypothesis from ZFC and of the Axiom of Choice from ZF. The two base theories are different and must be kept apart: AC is one of ZFC's own axioms, so it cannot be independent of ZFC; the choiceless theory ZF is what Cohen's symmetric-submodel argument works over. CH is independent of ZFC proper. 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+00AC	Negation	As in ¬CH, ¬AC
κ	U+03BA	Kappa	A cardinal, in Easton's and König's constraints
τ	U+03C4	Tau	A P-name
φ	U+03C6	Phi	The sentence being forced
ω	U+03C9	Omega	The first infinite ordinal, in ℵ_ω
₄	U+2084	Subscript four	Index in ℵ_{ω₄}
ℵ	U+2135	Aleph	Cardinal notation in the pcf bound
∈	U+2208	Element of	Membership of a condition in G
≤	U+2264	Less than or equal	The order on conditions: q ≤ p, q stronger
⊆	U+2286	Subset of or equal to	G ⊆ P
⊨	U+22A8	Satisfaction	M[G] ⊨ φ
⊩	U+22A9	Forces	The forcing relation p ⊩ φ, definable in M
⟹	U+27F9	Implies	Relative-consistency implication
P	—	Forcing poset	The set of conditions
p, q	—	Conditions	Elements of P; q ≤ p means q decides more
G	—	Generic filter	Meets every dense set lying in M
M	—	Ground model	Countable transitive model of ZFC
M[G]	—	Generic extension	The forced model; same ordinals as M
val_G	—	Valuation	Interprets P-names in M[G]
V	—	Set-theoretic universe	As in V = L and the Boolean-valued V^B
V^B	—	Boolean-valued model	Universe with truth values in a Boolean algebra B
L	—	Constructible universe	Absolute: computed alike in M and M[G]
ccc	—	Countable chain condition	Preserves cardinals and cofinalities
CH, AC	—	Continuum Hypothesis, Choice	The statements shown independent
MA	—	Martin's Axiom	Obtained by iterated ccc forcing
Con	—	Consistency	Con(ZFC) ⟹ Con(ZFC + ¬CH)
cf	—	Cofinality	König's constraint cf(2^κ) > κ
pcf	—	Possible cofinalities	Shelah's theory, source of the bound at ℵ_ω

Metatheory. The forcing theorem is two lemmas, both proved inside the ground model: the definability lemma, that p ⊩ φ is definable in M, and the truth lemma, that M[G] ⊨ φ iff some condition in G forces φ. Together they give M[G] ⊨ ZFC whenever M ⊨ ZFC, which is what makes forcing a consistency proof rather than the construction of a particular set. Cohen (1963) obtained Con(ZFC) ⟹ Con(ZFC + ¬CH), which with Gödel's constructible universe yields the independence of CH, and the symmetric-submodel variant gives Con(ZF) ⟹ Con(ZF + ¬AC). Easton (1970) showed the continuum function on regular cardinals is otherwise arbitrary, subject only to monotonicity and König's cf(2^κ) > κ. Lévy and Solovay (1967) proved that forcing of size below a measurable or supercompact cardinal preserves it, so large-cardinal axioms are immune to small forcing. Solovay and Tennenbaum (1971) introduced iteration and derived Con(MA + ¬CH) and the consistency of Souslin's Hypothesis; Shelah's proper forcing carried iteration past ccc. Laver (2007) and Woodin independently proved ground-model definability: M is definable in M[G] from a parameter.

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

Limitations. Forcing yields relative consistency, never truth and never outright consistency: it presupposes a ground model of ZFC, so by Gödel's second incompleteness theorem every result has the form Con(ZFC) ⟹ Con(ZFC + φ). It is constrained from inside as well. M and M[G] have the same ordinals and therefore the same constructible universe, so forcing can destroy V = L but never establish it. The continuum function is not free: Easton's theorem covers regular cardinals only, and at singulars ZFC itself limits what any forcing can do — Silver's theorem for singulars of uncountable cofinality, and Shelah's pcf bound 2^{ℵ_ω} < ℵ_{ω₄} when ℵ_ω is a strong limit, are theorems rather than artefacts of method. Large cardinals are similarly insulated, since by Lévy–Solovay small forcing leaves them untouched. And the method adjudicates no question of which axioms are correct; it shows only unprovability.