Forcing and independence

MotivationH

After Gödel, the other half

Gödel's constructible universe (see axiomatic set theory) showed that the continuum hypothesis cannot be refuted from ZFC, if ZF is consistent. For twenty-five years nobody could show that it cannot be proved. The difficulty is that $L$ is the smallest possible model; to make $2^{\aleph_0}$ large one must build models with more sets, and there was no method for adding sets to a model of ZFC while keeping all the axioms true.

In 1963 Paul Cohen found one. Starting from a countable transitive model $M$ , he adjoined a new set $G$ — a generic filter on a partial order of "conditions" — and showed that the resulting model $M[G]$ still satisfies ZFC, has the same ordinals as $M$ , and can be arranged to satisfy $2^{\aleph_0} = \aleph_2$ . The method, forcing, has since shown hundreds of natural statements to be independent of ZFC, in set theory, topology, algebra and analysis.

IntuitionH

Adjoining a generic object

We want to add to $M$ a new real number $g : \omega \to 2$ . We cannot describe $g$ inside $M$ — then it would already be in $M$ . Instead we describe the finite pieces of information about $g$ : the conditions are finite partial functions $p$ from $\omega$ to $2$ , and $p$ is stronger than $q$ if it extends it. A set $D$ of conditions is dense if every condition can be strengthened into $D$ : dense sets are requirements that a good $g$ should meet, such as " $g(17)$ is decided" or " $g$ differs from the real $x$ somewhere". A filter $G$ is generic if it meets every dense set that $M$ can see. Then $g = \bigcup G$ is total and different from every real in $M$ .

Statements about the new model are controlled by conditions: $p$ forces $\varphi$ if $\varphi$ holds in $M[G]$ for every generic $G$ containing $p$ . The miracle of forcing is that this relation can be computed inside $M$ , so $M$ "knows" what its extensions will look like without being able to name the generic object.

Analogy, not a formal construction

Adjoining $\sqrt 2$ to $\Q$ produces the smallest field containing $\Q$ and $\sqrt 2$ , and every element of $\Q(\sqrt 2)$ has a name $a + b\sqrt 2$ with $a, b \in \Q$ . Similarly $M[G]$ is the smallest transitive model of ZFC containing $M$ and $G$ , and every element of $M[G]$ has a name in $M$ . The analogy is loose: $\sqrt 2$ satisfies an equation over $\Q$ , whereas a generic $G$ is characterised by satisfying no special property describable in $M$ — it is "transcendental" over $M$ in the strongest sense.

Cohen conditions form the binary tree of finite strings; stronger conditions lie lower. A generic filter is a branch through the tree (gold) that meets every dense set of the ground model; its union is the Cohen real $g$.

DefinitionsH

Definitions

Definition— independence and relative consistency

A sentence $\varphi$ is independent of ZFC if $\mathsf{ZFC} \nvdash \varphi$ and $\mathsf{ZFC} \nvdash \neg\varphi$ . Since an inconsistent theory proves everything, independence implies $\mathrm{Con}(\mathsf{ZFC})$ , which ZFC cannot prove. So set theorists prove relative consistency statements such as $\mathrm{Con}(\mathsf{ZFC}) \to \mathrm{Con}(\mathsf{ZFC} + \neg\mathsf{CH})$ , and "CH is independent" means: if ZFC is consistent, it neither proves nor refutes CH.

Definition— forcing notion, dense sets, generic filters

A forcing notion is a preorder $(P, \le, \mathbb 1)$ with a largest element $\mathbb 1$ ; $p \le q$ means " $p$ is stronger than $q$ ". Conditions $p, q$ are compatible if some $r$ satisfies $r \le p$ and $r \le q$ ; an antichain is a set of pairwise incompatible conditions. A set $D \subseteq P$ is dense if every $p \in P$ has some $q \le p$ in $D$ . A filter is a non-empty $G \subseteq P$ that is upward closed and in which any two elements have a common extension in $G$ . If $M$ is a model containing $P$ , a filter $G$ is $M$ -generic if it meets every dense set $D \subseteq P$ with $D \in M$ .

Definition— countable transitive model

A countable transitive model (ctm) is a countable set $M$ , transitive ( $x \in M \Rightarrow x \subseteq M$ ), such that $(M, \in)$ satisfies the axioms in question (all of ZFC, or a large enough finite part — see the remark on metamathematics). Transitivity makes $\omega$ , ordinals, functions and finite sets mean the same in $M$ as in $V$ .

Definition— names and the generic extension

By recursion, a $P$ -name is a set of pairs $(\sigma, p)$ where $\sigma$ is a $P$ -name and $p \in P$ ; let $M^P$ be the set of $P$ -names in $M$ . For a filter $G$ , the interpretation of a name is $\tau^G = \{\sigma^G : (\sigma, p) \in \tau \text{ for some } p \in G\}$ , and the generic extension is $M[G] = \{\tau^G : \tau \in M^P\}$ . Each $x \in M$ has the check name $\check x = \{(\check y, \mathbb 1) : y \in x\}$ with $\check x^G = x$ , and $\dot G = \{(\check p, p) : p \in P\}$ satisfies $\dot G^G = G$ .

Definition— the forcing relation

For $p \in P$ , a formula $\varphi$ and names $\tau_1, \dots, \tau_n \in M^P$ , $p \Vdash \varphi(\tau_1, \dots, \tau_n)$ means: for every $M$ -generic $G$ with $p \in G$ , $M[G] \models \varphi(\tau_1^G, \dots, \tau_n^G)$ .

Definition— Cohen forcing and the ccc

For a set $I$ , $\mathrm{Fn}(I, 2)$ is the set of finite partial functions from $I$ to $2$ , ordered by reverse inclusion ( $p \le q$ iff $p \supseteq q$ ), with $\mathbb 1 = \varnothing$ . Cohen forcing adding $\kappa$ reals is $\mathrm{Add}(\omega, \kappa) = \mathrm{Fn}(\kappa \times \omega, 2)$ . A forcing notion has the countable chain condition (ccc) if every antichain is countable.

Worked examplesH

Generic filters: existence, non-examples, Cohen reals

Theorem— Rasiowa–Sikorski lemma

If $P$ is a preorder, $p \in P$ , and $\mathcal D$ is a countable family of dense subsets of $P$ , there is a filter $G$ with $p \in G$ meeting every $D \in \mathcal D$ . In particular, if $M$ is a ctm and $P \in M$ , then $M$ -generic filters exist.

Proof

Enumerate $\mathcal D = \{D_0, D_1, \dots\}$ . Put $p_0 = p$ and, using density, choose $p_{n+1} \le p_n$ with $p_{n+1} \in D_n$ . Then $G = \{q \in P : p_n \le q \text{ for some } n\}$ is a filter (two members lie above $p_n$ and $p_m$ , hence both above $p_{\max(n, m)} \in G$ ) and meets each $D_n$ at $p_{n+1}$ . If $M$ is countable, so is the family of dense sets belonging to $M$ .

∎

Example— Trivial forcing

If $P$ is finite, every filter $G$ contains a common extension $r$ of its finitely many members, and then $G = \{q : q \ge r\}$ ; so $G \in M$ and $M[G] = M$ . Forcing does something only when conditions keep splitting, as the next lemma shows.

Theorem— Lemma (generic filters are new)

Suppose every condition of $P$ has two incompatible extensions, and $G$ is $M$ -generic. Then $G \notin M$ .

Proof

If $G \in M$ , then $D = P \setminus G$ is in $M$ , and it is dense: any $p$ has incompatible extensions $q, r$ , and a filter cannot contain both, so one of them is in $D$ . But $G$ does not meet $D$ , contradicting genericity.

∎

The lemma also explains why we cannot simply force over the whole universe $V$ : there is no filter meeting every dense set, because $P \setminus G$ is always dense. A ctm has only countably many dense sets, which Rasiowa–Sikorski can meet.

Theorem— Theorem (Cohen reals)

Let $M$ be a ctm, $P = \mathrm{Fn}(\omega, 2)$ and $G$ an $M$ -generic filter. Then $g = \bigcup G$ is a function from $\omega$ to $2$ , and $g \notin M$ .

Proof

Any two members of $G$ are compatible, so $\bigcup G$ is a function. For $n \in \omega$ , $D_n = \{p : n \in \operatorname{dom} p\}$ is dense and in $M$ , so $G$ meets it and $n \in \operatorname{dom} g$ . For $x \in M \cap {}^\omega 2$ , the set $E_x = \{p : p(n) \neq x(n) \text{ for some } n \in \operatorname{dom} p\}$ is dense (extend $p$ at a new point $n$ by $1 - x(n)$ ) and in $M$ ; a condition $p \in G \cap E_x$ shows $g \neq x$ .

∎

ProofH

The generic extension and the failure of CH

Theorem— Generic model theorem (Cohen 1963)

Let $M$ be a ctm of ZFC, $P \in M$ a forcing notion and $G$ an $M$ -generic filter. Then $M[G]$ is a ctm of ZFC, $M \subseteq M[G]$ , $G \in M[G]$ , $M$ and $M[G]$ have the same ordinals, and every transitive model of ZF containing $M \cup \{G\}$ contains $M[G]$ .

Theorem— Forcing theorem

(Truth) $M[G] \models \varphi(\tau_1^G, \dots, \tau_n^G)$ if and only if $p \Vdash \varphi(\tau_1, \dots, \tau_n)$ for some $p \in G$ . (Definability) For each $\varphi$ , the relation $p \Vdash \varphi(\tau_1, \dots, \tau_n)$ — for $p \in P$ and $\tau_i \in M^P$ — is definable in $M$ .

Both are proved by defining, inside $M$ , a relation $\Vdash^*$ by recursion on formulas and on the ranks of names — for atomic formulas by a simultaneous recursion, and then $p \Vdash^* \neg\varphi$ iff no $q \le p$ forces $\varphi$ , $p \Vdash^* \forall x\, \varphi$ iff $p \Vdash^* \varphi(\tau)$ for every name $\tau$ — and showing by induction that $\Vdash^*$ agrees with $\Vdash$ , using genericity at the negation step. The ZFC axioms in $M[G]$ then follow: pairing, union and infinity by explicit names; separation and power set from definability of forcing; replacement from reflection in $M$ . Kunen (1980, chapter VII) gives every detail.

To make CH fail we need two more ingredients: a combinatorial lemma, and the fact that ccc forcing does not collapse cardinals.

Theorem— Δ-system lemma

Every uncountable family $\mathcal A$ of finite sets has an uncountable subfamily $\mathcal B$ that is a Δ-system: there is a finite set $R$ (the root) with $a \cap b = R$ for all distinct $a, b \in \mathcal B$ .

Proof

Uncountably many members of $\mathcal A$ have the same size $n$ , so assume all do, and induct on $n$ . For $n = 1$ , distinct singletons are pairwise disjoint (root $\varnothing$ ). For $n \gt 1$ : if some point $x$ lies in uncountably many members, apply the induction hypothesis to $\{a \setminus \{x\} : x \in a \in \mathcal A\}$ and add $x$ back to the root. Otherwise every point lies in only countably many members; then choose $a_\xi$ for $\xi \lt \omega_1$ by recursion, each disjoint from $\bigcup_{\eta \lt \xi} a_\eta$ — possible because this union is countable and only countably many members meet it. The $a_\xi$ are pairwise disjoint.

∎

Theorem— Lemma (Cohen forcing is ccc)

For every set $I$ , $\mathrm{Fn}(I, 2)$ has the countable chain condition.

Proof

Let $\{p_\xi : \xi \lt \omega_1\}$ be uncountably many conditions. By the Δ-system lemma, uncountably many of the domains $\operatorname{dom} p_\xi$ form a Δ-system with root $R$ . There are only $2^{|R|}$ functions $R \to 2$ , so uncountably many of these $p_\xi$ agree on $R$ . Any two of them agree where their domains overlap, so their union is a common extension: they are compatible. Hence there is no uncountable antichain.

∎

A ccc forcing preserves cardinals (and cofinalities). In outline: if $f \in M[G]$ maps $A$ into $B$ (with $A, B \in M$ ), fix a name $\dot f$ and a condition $p_0 \in G$ forcing that $\dot f$ is such a function. In $M$ let $F(a)$ be the set of $b$ for which some $q \le p_0$ forces $\dot f(\check a) = \check b$ . Conditions forcing different values are incompatible, so by the ccc each $F(a)$ is countable, and $f(a) \in F(a)$ by the truth lemma. If in $M[G]$ some $f$ mapped an infinite $\mu$ onto an $M$ -cardinal $\lambda \gt \mu$ , then in $M$ the countable sets $F(\alpha)$ , $\alpha \lt \mu$ , would cover $\lambda$ , giving $\lambda \le |\mu| \cdot \aleph_0 \lt \lambda$ .

Theorem— Cohen (1963): Con(ZFC) implies Con(ZFC + ¬CH)

Let $M$ be a ctm of ZFC, let $\kappa = \aleph_2^M$ , and let $G$ be $M$ -generic for $P = \mathrm{Fn}(\kappa \times \omega, 2)^M$ . Then $M[G] \models 2^{\aleph_0} \ge \aleph_2$ .

Proof

Let $g = \bigcup G : \kappa \times \omega \to 2$ (a function, total by density) and $g_\alpha(n) = g(\alpha, n)$ . For $\alpha \neq \beta$ in $\kappa$ the set of conditions $p$ with $p(\alpha, n) \neq p(\beta, n)$ for some $n$ is dense and in $M$ , so $g_\alpha \neq g_\beta$ . Hence $\alpha \mapsto g_\alpha$ is an injection, in $M[G]$ , of $\kappa$ into ${}^\omega 2$ . By the ccc, $P$ preserves cardinals, so $\kappa = \aleph_2^M = \aleph_2^{M[G]}$ , and $M[G] \models 2^{\aleph_0} \ge \aleph_2$ .

∎

Counting "nice names" shows more precisely that $M[G] \models 2^{\aleph_0} = \kappa$ whenever $M \models \kappa^{\aleph_0} = \kappa$ . Combined with Gödel's $L$ : if ZFC is consistent, it neither proves nor refutes CH.

Note

Metamathematics. We do not know that a ctm of ZFC exists — its existence implies $\mathrm{Con}(\mathsf{ZFC})$ . The relative consistency proof avoids it: if $\mathsf{ZFC} + \neg\mathsf{CH}$ proved a contradiction, the proof would use finitely many axioms $\Phi$ . By reflection, Löwenheim–Skolem and the Mostowski collapse, ZFC proves that every finite fragment of ZFC has a ctm; choosing a fragment large enough that the argument above makes $M[G]$ satisfy $\Phi \cup \{\neg\mathsf{CH}\}$ , ZFC would prove that $\Phi \cup \{\neg\mathsf{CH}\}$ has a model, hence is consistent — contradicting the assumed proof of a contradiction. Alternatively, Boolean-valued models (Scott, Solovay, Vopěnka) force over $V$ itself without any countable model.

ExplanationH

What forcing has shown

The continuum function. Easton (1970): for regular cardinals, $\kappa \mapsto 2^\kappa$ can be any class function $F$ that is non-decreasing and satisfies $\operatorname{cf}(F(\kappa)) \gt \kappa$ (König's restriction) — forced by a class-sized product of Cohen-type forcings. At singular cardinals the picture is subtler (Silver, Shelah's pcf theory, and Magidor's and Gitik's large-cardinal forcing constructions).
Suslin's hypothesis (a complete dense linear order without endpoints in which every family of pairwise disjoint open intervals is countable is isomorphic to $\R$ ) is independent: Jech (1967) and Tennenbaum (1968) forced a Suslin line, and Solovay and Tennenbaum (1971) used iterated ccc forcing to make Suslin's hypothesis true.
Martin's axiom (Martin and Solovay, 1970) — "for every ccc forcing and fewer than $2^{\aleph_0}$ dense sets there is a filter meeting them all" — is consistent with $\neg$ CH and settles many questions of topology and analysis.
Choice and measurability. Cohen also showed that AC is independent of ZF (using symmetric submodels). Solovay (1970), starting from an inaccessible cardinal, built a model of $\mathsf{ZF} + \mathsf{DC}$ in which every set of reals is Lebesgue measurable.
Algebra and analysis. Shelah's solution of Whitehead's problem (1974) and the Dales–Esterle / Solovay–Woodin results on automatic continuity show that questions of pure algebra and analysis can be independent.
Forcing axioms. Shelah's proper forcing and the forcing axioms PFA and MM (Baumgartner; Foreman, Magidor and Shelah) decide many such questions; PFA implies $2^{\aleph_0} = \aleph_2$ (Todorčević; Veličković).

Formal mathematicsF

The combinatorics of genericity in Lean

Mathlib does not formalise forcing over models of ZFC. The Lean module formalises the combinatorial core of Cohen forcing, using conditions that are finite binary strings (equivalent, as a forcing, to $\mathrm{Fn}(\omega, 2)$ ). It uses the extension order, in which p ≤ q means "q extends p"; in that order Mathlib's Order.Cofinal sets are the dense sets and Mathlib's Order.Ideals are the filters.

CohenLean 4Formally verified

/-- **Cohen forcing**: a condition is a finite binary string `p = (p₀, …, p_{k-1})`, a finite
approximation to an infinite binary sequence ("a real"). -/
structure Cohen where
  /-- The finite binary string. -/
  bits : List Bool

Axioms used: No axiomsformal/Lumenary/Forcing.leanTry it in the Lean web editor

instPreorderLean 4Formally verified

/-- The extension order: `p ≤ q` iff `p` is an initial segment (prefix) of `q`, i.e. `q` carries
at least as much information as `p`. -/
instance instPreorder : Preorder Cohen where
  le p q := p.bits <+: q.bits
  le_refl p := List.prefix_refl p.bits
  le_trans _ _ _ := List.IsPrefix.trans

Axioms used: propextformal/Lumenary/Forcing.leanTry it in the Lean web editor

bitLean 4Formally verified

/-- The `i`-th bit decided by the condition `p`, if `p` is long enough. -/
def bit (p : Cohen) (i : ℕ) : Option Bool := p.bits[i]?

Axioms used: propextformal/Lumenary/Forcing.leanTry it in the Lean web editor

bit_monoLean 4Proved here from basic factsFormally verified

/-- Stronger conditions keep the decisions of weaker ones: if `p ≤ q` and `p` says bit `i` is
`b`, so does `q`. -/
theorem bit_mono {p q : Cohen} (h : p ≤ q) {i : ℕ} {b : Bool} (hb : bit p i = some b) :
    bit q i = some b := by
  obtain ⟨hi, rfl⟩ := List.getElem?_eq_some_iff.mp hb
  exact List.prefix_iff_getElem?.mp h i hi

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/Forcing.leanTry it in the Lean web editor

The two families of dense sets used in the proof of the Cohen-real theorem:

decides_denseLean 4Proved here from basic factsFormally verified

/-- For each `n`, the set of conditions that decide bit `n` is **dense**: any condition can be
extended (by padding with zeros) to one of length greater than `n`. -/
theorem decides_dense (n : ℕ) : IsCofinal {p : Cohen | (bit p n).isSome} := by
  intro p
  refine ⟨⟨p.bits ++ List.replicate (n + 1) false⟩, ?_, List.prefix_append _ _⟩
  show (p.bits ++ List.replicate (n + 1) false)[n]?.isSome
  rw [Option.isSome_iff_ne_none, Ne, List.getElem?_eq_none_iff, not_le,
    List.length_append, List.length_replicate]
  omega

Axioms used: propext, Quot.soundformal/Lumenary/Forcing.leanTry it in the Lean web editor

avoids_denseLean 4Proved here from basic factsFormally verified

/-- For each real `x : ℕ → Bool`, the set of conditions that **disagree with `x` somewhere** is
dense: extend `p` by one bit, the opposite of `x` at position `length p`. Meeting this set is
how a generic real escapes `x` — a diagonal argument, one step at a time. -/
theorem avoids_dense (x : ℕ → Bool) : IsCofinal {p : Cohen | ∃ i, bit p i = some (!x i)} := by
  intro p
  refine ⟨⟨p.bits ++ [!x p.bits.length]⟩, ⟨p.bits.length, ?_⟩, List.prefix_append _ _⟩
  show (p.bits ++ [!x p.bits.length])[p.bits.length]? = _
  simp

Axioms used: propextformal/Lumenary/Forcing.leanTry it in the Lean web editor

decidesLean 4Formally verified

/-- The dense set "bit `n` is decided", bundled as a Mathlib `Order.Cofinal`. -/
def decides (n : ℕ) : Order.Cofinal Cohen := ⟨{p | (bit p n).isSome}, decides_dense n⟩

Axioms used: propext, Quot.soundformal/Lumenary/Forcing.leanTry it in the Lean web editor

avoidsLean 4Formally verified

/-- The dense set "disagrees with `x` somewhere", bundled as a Mathlib `Order.Cofinal`. -/
def avoids (x : ℕ → Bool) : Order.Cofinal Cohen :=
  ⟨{p | ∃ i, bit p i = some (!x i)}, avoids_dense x⟩

Axioms used: propextformal/Lumenary/Forcing.leanTry it in the Lean web editor

Mathlib proves the Rasiowa–Sikorski lemma (Order.idealOfCofinals):

rasiowa_sikorskiLean 4Applies a library theoremFormally verified

/-- **The Rasiowa–Sikorski lemma**: for any *countable* family of dense sets in a preorder there
is a filter (here: an `Order.Ideal` of the extension order) meeting all of them. Its proof
builds a sequence `p₀ ≤ p₁ ≤ ⋯` with `p_{n+1}` in the `n`-th dense set. This applies Mathlib's
`Order.idealOfCofinals` and `Order.cofinal_meets_idealOfCofinals`. -/
theorem rasiowa_sikorski {P : Type*} [Preorder P] (p : P) {ι : Type*} [Encodable ι]
    (D : ι → Order.Cofinal P) : ∃ G : Order.Ideal P, p ∈ G ∧ ∀ i, ∃ q ∈ D i, q ∈ G :=
  ⟨Order.idealOfCofinals p D, Order.mem_idealOfCofinals p D,
    Order.cofinal_meets_idealOfCofinals p D⟩

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/Forcing.leanTry it in the Lean web editor

A filter meeting every decides n determines a real, and meeting avoids x makes it different from x. With the countable list standing for the reals of a ctm $M$ , this is the Cohen-real theorem:

generic_realLean 4Proved here from basic factsFormally verified

/-- **A generic filter determines a real.** If a filter `G` meets every dense set `decides n`,
the conditions in `G` are compatible finite approximations of a single real `g`: every bit
decided by a member of `G` is the corresponding bit of `g`.
Proof: choose `pₙ ∈ G` deciding bit `n` and let `g n` be that bit. If `p ∈ G` decides bit `n`
as `b`, then `p` and `pₙ` have a common extension `r ∈ G` (directedness), which decides bit `n`
both as `b` and as `g n`. -/
theorem generic_real (G : Order.Ideal Cohen) (hG : ∀ n, ∃ p ∈ decides n, p ∈ G) :
    ∃ g : ℕ → Bool, ∀ p ∈ G, ∀ i b, bit p i = some b → g i = b := by
  choose q hqD hqG using hG
  -- `q n ∈ G` decides bit `n`; read that bit off.
  have hsome : ∀ n, ∃ b, bit (q n) n = some b := fun n => Option.isSome_iff_exists.mp (hqD n)
  choose g hg using hsome
  refine ⟨g, fun p hp i b hb => ?_⟩
  obtain ⟨r, -, hpr, hqr⟩ := G.directed p hp (q i) (hqG i)
  have h1 : bit r i = some b := bit_mono hpr hb
  have h2 : bit r i = some (g i) := bit_mono hqr (hg i)
  exact Option.some.inj (h2.symm.trans h1)

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/Forcing.leanTry it in the Lean web editor

cohen_real_not_in_listLean 4Proved here from basic factsFormally verified

/-- **Cohen reals are new.** For every countable list `x₀, x₁, …` of reals there is a real `g`
different from all of them — obtained, as in forcing, from a filter meeting the countably many
dense sets `decides n` and `avoids xₖ`. With the list taken to be the reals of a countable
transitive model `M`, this is the statement that the Cohen real of `M[G]` is not in `M`.
(Cantor's diagonal argument, rebuilt from genericity.) -/
theorem cohen_real_not_in_list (xs : ℕ → ℕ → Bool) : ∃ g : ℕ → Bool, ∀ k, g ≠ xs k := by
  obtain ⟨G, -, hG⟩ := rasiowa_sikorski (⟨[]⟩ : Cohen)
    (fun j : ℕ ⊕ ℕ => Sum.elim decides (fun k => avoids (xs k)) j)
  obtain ⟨g, hg⟩ := generic_real G (fun n => hG (Sum.inl n))
  refine ⟨g, fun k hk => ?_⟩
  obtain ⟨p, ⟨i, hi⟩, hpG⟩ := hG (Sum.inr k)
  have := hg p hpG i _ hi
  rw [hk] at this
  exact Bool.not_ne_self (xs k i) this.symm

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/Forcing.leanTry it in the Lean web editor

And the reason forcing starts from a countable model — no filter meets every dense set:

no_filter_meets_every_denseLean 4Proved here from basic factsFormally verified

/-- **No filter meets every dense set.** For any filter `G`, the complement of `G` is dense, and
`G` does not meet it. Proof: any `p` has the two incompatible extensions `p⌢0` and `p⌢1`; a
filter cannot contain both (they have no common extension), so one lies outside `G`. This is why
forcing begins with a *countable* model `M`: we only ask `G` to meet the dense sets that belong
to `M`, and then `G ∉ M`. -/
theorem no_filter_meets_every_dense (G : Order.Ideal Cohen) :
    ∃ D : Set Cohen, IsCofinal D ∧ ∀ p ∈ D, p ∉ G := by
  refine ⟨(G : Set Cohen)ᶜ, ?_, fun p hp => hp⟩
  intro p
  by_contra h
  push Not at h
  -- Both one-bit extensions of `p` would lie in `G` ...
  have hin : ∀ b : Bool, (⟨p.bits ++ [b]⟩ : Cohen) ∈ (G : Set Cohen) := by
    intro b
    by_contra hb
    exact h _ hb (List.prefix_append _ _)
  -- ... so they would have a common extension `r`, forcing `p⌢1 = p⌢0`.
  obtain ⟨r, -, h1, h2⟩ := G.directed _ (hin true) _ (hin false)
  have hpre := List.prefix_of_prefix_length_le h1 h2 (by simp)
  have heq := hpre.eq_of_length (by simp)
  simp at heq

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/Forcing.leanTry it in the Lean web editor

Not formalised here: names, the forcing relation and the forcing theorem, $M[G] \models \mathsf{ZFC}$ , the Δ-system lemma, the ccc and preservation of cardinals. The full independence of CH has been formalised elsewhere: in Lean 3 by Jesse Michael Han and Floris van Doorn (the Flypitch project, 2019–2020, with Boolean-valued models) and in Isabelle/ZF by Emmanuel Gunther, Miguel Pagano, Pedro Sánchez Terraf and Matías Steinberg (with countable transitive models).

ComputationC

Building a generic real

The experiment runs the Rasiowa–Sikorski construction against a finite stand-in for a ground model: a list of reals given by rules (primes, squares, the Thue–Morse sequence, the binary digits of $\sqrt 2$ , and every eventually periodic sequence with short preperiod and period). It meets the dense sets "decide bit $n$ " and "disagree with $x$ " in turn, and checks that the resulting condition disagrees with every listed real. Then it checks the other half: the filter of initial segments of a real $g$ misses the dense set "disagree with $g$ ".

A Cohen generic real escapes a list of ground-model realsPythonExact computationExhaustive finite checkComputationally tested

"""Building a Cohen generic real against a list of "ground model" reals.

In Cohen forcing a condition is a finite binary string, and a stronger
condition extends it. A dense set is a requirement that every condition can
be extended to meet: "decide bit n", or "disagree with the real x somewhere".
A filter meeting countably many dense sets is built step by step (the
Rasiowa-Sikorski lemma): extend the current condition into the next dense
set, forever.

Here the "ground model" is a finite stand-in: a list of reals given by rules
(some famous sequences, and every eventually periodic sequence with short
preperiod and period). We meet the dense sets "avoid x" for each listed real
and "decide bit n" for n < 32, interleaved, and check that the resulting
condition disagrees with every listed real - the generic real is new. Then
we check the other half of the story: the filter of initial segments of any
real g misses the dense set "disagree with g", so no filter meets every dense
set.

Runs unchanged in the browser (Pyodide) using only the standard library.
"""

from itertools import product
from math import isqrt
import textwrap

def _prime(n):
    """Trial-division primality test."""
    return n >= 2 and all(n % d for d in range(2, isqrt(n) + 1))

def _eventually_periodic(pre, cycle):
    """The real pre + cycle + cycle + ... as a rule."""
    return lambda n: pre[n] if n < len(pre) else cycle[(n - len(pre)) % len(cycle)]

def ground_reals():
    """A list of (name, rule) pairs standing in for the reals of a model M."""
    reals = [
        ("primes", lambda n: int(_prime(n))),
        ("squares", lambda n: int(isqrt(n) ** 2 == n)),
        ("Thue-Morse", lambda n: bin(n).count("1") % 2),
        ("sqrt 2 digits", lambda n: isqrt(2 << (2 * (n + 1))) & 1),
    ]
    for pre_len in range(3):
        for cycle_len in range(1, 4):
            for bits in product((0, 1), repeat=pre_len + cycle_len):
                pre, cycle = bits[:pre_len], bits[pre_len:]
                name = "".join(map(str, pre)) + "(" + "".join(map(str, cycle)) + ")"
                reals.append((name, _eventually_periodic(pre, cycle)))
    return reals

def meet_decide(p, n):
    """Extend p (if needed) so that it decides bit n, padding with zeros."""
    return p + (0,) * max(0, n + 1 - len(p))

def disagreement(p, x):
    """A position where condition p disagrees with the real x, or None."""
    return next((i for i, b in enumerate(p) if b != x(i)), None)

def meet_avoid(p, x):
    """Extend p (if needed) so that it disagrees with x somewhere."""
    if disagreement(p, x) is not None:
        return p
    return p + (1 - x(len(p)),)

def build_generic(reals, bits):
    """Meet 'avoid x_k' and 'decide n' alternately; return the final condition
    and the list of conditions p_0 <= p_1 <= ... that were built."""
    p, chain = (), [()]
    for step in range(max(len(reals), bits)):
        if step < len(reals):
            p = meet_avoid(p, reals[step][1])
            chain.append(p)
        if step < bits:
            p = meet_decide(p, step)
            chain.append(p)
    return p, chain

def is_chain(conditions):
    """Is each condition an initial segment of the next (a descending chain)?"""
    return all(q[:len(p)] == p for p, q in zip(conditions, conditions[1:]))

def main():
    reals = ground_reals()
    g, chain = build_generic(reals, 32)
    print(f"Ground reals listed: {len(reals)} rules (some repeat a real)")
    print(f"Dense sets met: {len(reals)} of the form 'avoid x', 32 'decide bit n'")
    print(f"Conditions built: {len(chain)}, each extending the last: {is_chain(chain)}")
    print(f"Generic condition, {len(g)} bits:")
    text = "".join(map(str, g))
    for start in range(0, len(text), 64):
        print("   " + text[start:start + 64])
    positions = [disagreement(g, x) for _, x in reals]
    print(f"Disagrees with every listed real: {all(i is not None for i in positions)}")
    for name, x in reals[:6]:
        print(f"   {name:<14} first disagreement at bit {disagreement(g, x)}")
    print(f"   ... and {len(reals) - 6} eventually periodic reals")
    print()
    real_g = _eventually_periodic(g, (0,))
    misses = all(disagreement(g[:k], real_g) is None for k in range(len(g) + 1))
    print("The filter of initial segments of g (padded with zeros) contains no")
    print(f"condition disagreeing with g: {misses} - it misses that dense set.")
    print()
    print(textwrap.fill(
        "Epistemic status: exact computation for a finite list of reals and "
        "finitely many dense sets. It illustrates the Rasiowa-Sikorski "
        "construction and why a generic real is new; the real theorem - that "
        "for a countable transitive model M a generic G exists, G is not in M, "
        "and M[G] satisfies ZFC - is proved in the lesson, not here.",
        width=78,
    ))

if __name__ == "__main__":
    main()

Runs entirely in your browser, in an isolated worker. Nothing is sent to a server.

This is exact evidence about one finite construction; the theorems — existence of generics over a ctm, $G \notin M$ , $M[G] \models \mathsf{ZFC}$ — are proved above.

Explore

Explore: genericity is diagonalisation

Meeting the dense set "disagree with $x_k$ " is one step of a diagonal argument. In the widget, the flipped diagonal escapes every listed sequence; a Cohen generic does the same against all the reals of $M$ , one dense set at a time, and also meets every other requirement that $M$ can formulate.

The diagonal machine

Here is a list of infinite 0–1 sequences (we can only show the start). The gold sequence d flips the diagonal.

s1											…
s2											…
s3											…
s4											…
s5											…
s6											…

d	1	0	1	0	0	1	?	?	?	?	…

Point at (or tab to) a row to see where d differs from it. Click any digit to change the list.

Add d to the list and a new d appears that is different again. No list — however long — can contain every sequence.

Notice the difference from Cantor's argument: Cantor builds one particular sequence from the list, whereas a generic real is not built from anything in $M$ ; any real that meets the countably many dense sets of $M$ will do.

Exercises

1. Forcing and independence

Warm-upHuman

In Cohen forcing $\mathrm{Fn}(\omega, 2)$ (finite partial functions, stronger = larger), which of these sets are dense? Choose all that apply.

Choose all that apply

\{p : 5 \in \operatorname{dom} p\}

\{p : p(n) = 1 \text{ for some even } n \in \operatorname{dom} p\}

\{p : p(0) = 1\}

\{p : |\operatorname{dom} p| \le 3\}

2. Forcing and independence

Warm-upHuman

How many conditions does $\mathrm{Fn}(3, 2)$ have, i.e. how many partial functions from $\{0, 1, 2\}$ to $\{0, 1\}$ are there (including the empty function $\mathbb 1$ )?

3. Forcing and independence

CoreHuman

Why does the classical presentation of forcing start from a countable transitive model $M$ ?

Choose one

So that

M

has only countably many dense sets, and the Rasiowa–Sikorski lemma gives an

M

-generic filter.So that

M

contains only countably many reals, making CH false in

M

.Because only countable models satisfy the countable chain condition.Because ZFC proves that a countable transitive model of ZFC exists.

4. Forcing and independence

CoreHuman

In the proof that an $M$ -generic filter $G$ (for a forcing in which every condition has two incompatible extensions) is not in $M$ , which dense set does $G$ fail to meet if $G \in M$ ?

Choose one

P \setminus G

G

itself

\{p : n \in \operatorname{dom} p\}

\varnothing

5. Forcing and independence

CoreHuman

The proof that $\mathrm{Fn}(I, 2)$ has the countable chain condition takes uncountably many conditions $p_\xi$ . What is the key step?

Choose one

Apply the Δ-system lemma to their domains, then use that only finitely many functions exist on the finite root.Apply the Rasiowa–Sikorski lemma.Note that

\mathrm{Fn}(I, 2)

is countable.Use König's theorem.

6. Forcing and independence

StretchHuman

Assuming ZFC is consistent, which of these statements are independent of ZFC? Choose all that apply.

Choose all that apply

The continuum hypothesisSuslin's hypothesisEvery Whitehead group is free

2^{\aleph_0} \neq \aleph_\omega

Every set of reals is Lebesgue measurable

7. Forcing and independence

CoreFormal

The Lean file orders Cohen conditions by extension: p ≤ q means q extends p. In this order, what does Mathlib's Order.Ideal Cohen correspond to in forcing?

Choose one

A filter of conditions (closed under weakening, any two members have a common extension in it)A dense setA maximal antichainA name

8. Forcing and independence

CoreFormal

The theorem no_filter_meets_every_dense (G : Order.Ideal Cohen) : ∃ D : Set Cohen, IsCofinal D ∧ ∀ p ∈ D, p ∉ G is proved with which witness D?

Choose one

(G : Set Cohen)ᶜ, the complement of GSet.univavoids x for some real xdecides 0

9. Forcing and independence

StretchComputational

Write escape(reals, n): given a list of reals (functions from naturals to $\{0, 1\}$ ) and $n$ , return a tuple of bits $p$ of length at least $n$ that disagrees with every listed real at some position. This is the Rasiowa–Sikorski construction for the dense sets 'decide bit $k$ ' ( $k \lt n$ ) and 'disagree with $x$ '.

Runs entirely in your browser, in an isolated worker. Nothing is sent to a server.

Common misconceptionsH

Common misconceptions

Misconception

"If CH is independent, the question is meaningless." Independence means that ZFC does not settle it. Some set theorists regard CH as having a definite truth value to be found by new, justified axioms (Gödel's view; Woodin's programme), others as having no single answer (Hamkins's multiverse view). Mathematically, independence is a precise theorem about provability.

Misconception

"Forcing needs a countable transitive model of ZFC to exist." Formal relative consistency proofs use ctms of finite fragments, which ZFC proves to exist, or Boolean-valued models, which need no countable model at all. The ctm presentation is a convenient fiction that can always be eliminated.

Misconception

" $M[G]$ is $M$ with one new element." $M[G]$ contains $G$ and everything definable from it and parameters in $M$ — the interpretations of all names — for instance $\aleph_2$ many new reals in Cohen's model. It is the least transitive model of ZF containing $M \cup \{G\}$ .

Misconception

"Forcing shows that CH is false." Forcing produces models of $\neg$ CH; $L$ is a model of CH. Neither shows what is true "in $V$ "; together they show that ZFC proves neither.

ViewpointsH

Many ways of seeing

Topology— Generic means comeagre

Give $2^\omega$ the product topology. A dense set $D$ of Cohen conditions determines the open set $U_D = \bigcup_{p \in D} [p]$ , where $[p]$ is the basic clopen set of reals extending $p$ , and $U_D$ is dense in $2^\omega$ . Meeting $D$ means $g \in U_D$ . So a Cohen real over $M$ lies in the intersection of countably many dense open sets, and the Rasiowa–Sikorski lemma is the Baire category theorem in disguise. Precisely, $g$ is Cohen-generic over $M$ if and only if $g$ belongs to no meagre Borel set coded in $M$ (Solovay). In general a forcing notion $P$ carries a topology whose regular open sets form the complete Boolean algebra $\mathrm{RO}(P)$ , and forcing with $P$ is forcing with $\mathrm{RO}(P)$ .

Probability— Random reals

Replace "meagre" by "measure zero": random forcing (Solovay, 1970) has as conditions the Borel subsets of $[0, 1]$ of positive Lebesgue measure, ordered by inclusion. A random real over $M$ lies in no null Borel set coded in $M$ — it is "typical" in the sense of probability, passing every statistical test that $M$ can describe. Adding $\aleph_2$ random reals also makes CH fail, but the resulting model differs from Cohen's: for instance, random forcing adds no Cohen real. The duality between category and measure (Oxtoby) becomes a duality between forcings.

Analysis— Independence in analysis

Is every algebra homomorphism from $C(X)$ (continuous functions on a compact Hausdorff space) into a Banach algebra continuous? Kaplansky asked this. Dales and Esterle (independently, around 1976–78) showed that under CH there is a discontinuous one; Solovay and Woodin showed that it is consistent with ZFC that every such homomorphism is continuous. Forcing thus settled a question of functional analysis by showing it undecidable. Solovay's model, in which every set of reals is Lebesgue measurable (in $\mathsf{ZF} + \mathsf{DC}$ ), shows that the use of choice in constructing non-measurable sets is unavoidable (see measure theory).

Category theory— Sheaves on the poset of conditions

Lawvere and Tierney recast Cohen's proof in topos theory (Tierney, 1972): take the category of sheaves on the poset $\mathrm{Fn}(\aleph_2 \times \omega, 2)$ for the double-negation (dense) topology. This is a Boolean topos with a natural number object $N$ and a monomorphism from the constant object on $\aleph_2$ into the power object of $N$ , in which the internal continuum hypothesis fails. Mac Lane and Moerdijk (1992, chapter VI) present the independence of CH in this way. The topos has no points, the categorical form of "no filter meets every dense set": a generic filter is a point that exists only from the outside. See elementary topoi.

Logic— Boolean-valued models

Scott, Solovay and Vopěnka (1965–67) replaced the generic filter by truth values: for a complete Boolean algebra $B$ , the universe $V^B$ of $B$ -valued sets assigns to each sentence $\varphi$ a value $[\![\varphi]\!] \in B$ , with every axiom of ZFC receiving value $1$ . For $B = \mathrm{RO}(\mathrm{Fn}(\aleph_2 \times \omega, 2))$ , $[\![\neg\mathsf{CH}]\!] = 1$ . Forcing becomes order: $p \Vdash \varphi$ corresponds to $p \le [\![\varphi]\!]$ . Quotienting $V^B$ by any ultrafilter gives a two-valued (possibly ill-founded) model; over a ctm with a generic ultrafilter one recovers $M[G]$ .

Wonder Trails

Wonder Trail

Cantor's diagonal argument — the first step of every genericity argument — is explored for younger learners here.

Wonder Trail · Optional · never gradedHow many infinities?There are infinitely many counting numbers and infinitely many infinite 0–1 sequences. Are these two infinities the same size?Follow the trail

History & global context

History and context

Paul Cohen announced the independence of CH and AC in 1963 (published in the Proceedings of the National Academy of Sciences, 1963–64) and received the Fields Medal in 1966; his book Set Theory and the Continuum Hypothesis appeared in 1966.
Robert Solovay, Dana Scott and, independently in Prague, Petr Vopěnka developed Boolean-valued models (1965–67). Solovay's random reals and his measurable model followed in 1970.
William Easton (1970) determined the possible values of $2^\kappa$ at regular cardinals. Donald A. Martin and Solovay (1970) introduced Martin's axiom, and Solovay and Stanley Tennenbaum (1971) proved the consistency of Suslin's hypothesis; Thomas Jech and Tennenbaum had forced Suslin lines in 1967–68.
Saharon Shelah developed proper forcing and solved Whitehead's problem (1974); Myles Tierney and F. William Lawvere reformulated the independence of CH in topos theory (1972); Stevo Todorčević, Boban Veličković and others analysed forcing axioms.

After Gödel, the other half

Adjoining a generic object

Definitions

Generic filters: existence, non-examples, Cohen reals

The generic extension and the failure of CH

What forcing has shown

The combinatorics of genericity in Lean

Building a generic real

Explore: genericity is diagonalisation

Exercises

Common misconceptions

Many ways of seeing

Wonder Trail

History and context

Further reading