/-- **Cohen forcing**: a condition is a finite binary string `p = (p₀, …, p_{k-1})`, a finiteapproximation to an infinite binary sequence ("a real"). -/structure Cohen where /-- The finite binary string. -/ bits : List Bool
/-- The extension order: `p ≤ q` iff `p` is an initial segment (prefix) of `q`, i.e. `q` carriesat 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
Cohen.bit_monotheoremProved here from basic factspropext, Classical.choice, Quot.sound
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
Cohen.decides_densetheoremProved here from basic factspropext, Quot.sound
decides_denseLean 4Proved here from basic factsFormally verified
/-- For each `n`, the set of conditions that decide bit `n` is **dense**: any condition can beextended (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
Cohen.avoids_densetheoremProved here from basic factspropext
avoids_denseLean 4Proved here from basic factsFormally verified
/-- For each real `x : ℕ → Bool`, the set of conditions that **disagree with `x` somewhere** isdense: extend `p` by one bit, the opposite of `x` at position `length p`. Meeting this set ishow 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
/-- 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⟩
/-- 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⟩
rasiowa_sikorskitheoremApplies a library theorempropext, Classical.choice, Quot.sound
rasiowa_sikorskiLean 4Applies a library theoremFormally verified
/-- **The Rasiowa–Sikorski lemma**: for any *countable* family of dense sets in a preorder thereis a filter (here: an `Order.Ideal` of the extension order) meeting all of them. Its proofbuilds 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⟩
generic_realtheoremProved here from basic factspropext, Classical.choice, Quot.sound
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 bitdecided 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)
cohen_real_not_in_listtheoremProved here from basic factspropext, Classical.choice, Quot.sound
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 manydense sets `decides n` and `avoids xₖ`. With the list taken to be the reals of a countabletransitive 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
no_filter_meets_every_densetheoremProved here from basic factspropext, Classical.choice, Quot.sound
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`; afilter cannot contain both (they have no common extension), so one lies outside `G`. This is whyforcing begins with a *countable* model `M`: we only ask `G` to meet the dense sets that belongto `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
/-- For every real `x`, the conditions that disagree with `x` somewhere form a dense set.Hint: extend `p` by the single bit `!x p.bits.length`, i.e. use the condition`⟨p.bits ++ [!x p.bits.length]⟩`; `List.prefix_append` shows it extends `p`, and `simp` computesits bit at position `p.bits.length`. -/theorem avoids_dense (x : ℕ → Bool) : IsCofinal {p : Cohen | ∃ i, bit p i = some (!x i)} := by sorry
Show the compiled solution
avoids_denseLean 4Proved here from basic factsFormally verified
/-- For each real `x : ℕ → Bool`, the set of conditions that **disagree with `x` somewhere** isdense: extend `p` by one bit, the opposite of `x` at position `length p`. Meeting this set ishow 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
/-- Every countable list of reals misses some real. Prove it *by forcing*: apply`rasiowa_sikorski` to the dense sets `decides n` and `avoids (xs k)` (index them by `ℕ ⊕ ℕ`),then use `generic_real`. -/theorem cohen_real_not_in_list (xs : ℕ → ℕ → Bool) : ∃ g : ℕ → Bool, ∀ k, g ≠ xs k := by sorry
Show the compiled solution
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 manydense sets `decides n` and `avoids xₖ`. With the list taken to be the reals of a countabletransitive 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