diff --git a/ConNF/BaseType/NearLitter.lean b/ConNF/BaseType/NearLitter.lean index 16b8b84231..3601234211 100644 --- a/ConNF/BaseType/NearLitter.lean +++ b/ConNF/BaseType/NearLitter.lean @@ -11,7 +11,6 @@ In this file, we define near-litters, which are sets with small symmetric differ * `ConNF.IsNearLitter`: Proposition stating that a set is near a given litter. * `ConNF.NearLitter`: The type of near-litters. * `ConNF.Litter.toNearLitter`: Converts a litter to its corresponding near-litter. -* `ConNF.localCardinal`: The set of near-litters to a given litter. * `ConNF.NearLitter.IsLitter`: Proposition stating that a near-litter comes directly from a litter: it is of the form `L.toNearLitter` for some litter `L`. -/ @@ -181,32 +180,9 @@ theorem mk_nearLitter : #NearLitter = #μ := by le_rfl Params.μ_isStrongLimit.ne_zero -/-- The *local cardinal* of a litter is the set of all near-litters to that litter. -/ -def localCardinal (L : Litter) : Set NearLitter := - {N : NearLitter | N.1 = L} - -@[simp] -theorem mem_localCardinal {L : Litter} {N : NearLitter} : N ∈ localCardinal L ↔ N.1 = L := - Iff.rfl - -theorem localCardinal_nonempty (L : Litter) : (localCardinal L).Nonempty := - ⟨⟨L, litterSet _, isNearLitter_litterSet _⟩, rfl⟩ - -theorem localCardinal_disjoint : Pairwise (Disjoint on localCardinal) := - fun _ _ h => disjoint_left.2 fun _ h₁ h₂ => h <| h₁.symm.trans h₂ - -theorem localCardinal_injective : Injective localCardinal := by - intro L₁ L₂ h₁₂ - by_contra h - have := (localCardinal_disjoint h).inter_eq - rw [h₁₂, inter_self] at this - exact (localCardinal_nonempty _).ne_empty this - -theorem Litter.toNearLitter_mem_localCardinal (L : Litter) : L.toNearLitter ∈ localCardinal L := - rfl - +/-- There aer `μ` near-litters to a given litter. -/ @[simp] -theorem mk_localCardinal (L : Litter) : #(localCardinal L) = #μ := by +theorem mk_nearLitter_to (L : Litter) : #{N : NearLitter | N.1 = L} = #μ := by refine Eq.trans (Cardinal.eq.2 ⟨⟨?_, fun x => ⟨⟨L, x⟩, rfl⟩, ?_, ?_⟩⟩) (mk_nearLitter' L) · rintro ⟨x, rfl : x.1 = L⟩ exact x.snd @@ -226,6 +202,7 @@ theorem NearLitter.IsLitter.litterSet_eq {N : NearLitter} (h : N.IsLitter) : litterSet N.fst = N.snd := by cases h; rfl +/-- The main induction rule for near-litters that are litters. -/ theorem NearLitter.IsLitter.exists_litter_eq {N : NearLitter} (h : N.IsLitter) : ∃ L : Litter, N = L.toNearLitter := by obtain ⟨L⟩ := h; exact ⟨L, rfl⟩ @@ -266,6 +243,7 @@ theorem symmDiff_union_inter {α : Type _} {a b : Set α} : (a ∆ b) ∪ (a ∩ simp only [mem_union, mem_symmDiff, mem_inter_iff] tauto +/-- Near-litters to the same litter have `κ`-sized intersection. -/ theorem NearLitter.mk_inter_of_fst_eq_fst {N₁ N₂ : NearLitter} (h : N₁.fst = N₂.fst) : #(N₁ ∩ N₂ : Set Atom) = #κ := by rw [← isNear_iff_fst_eq_fst] at h @@ -281,6 +259,7 @@ theorem NearLitter.inter_nonempty_of_fst_eq_fst {N₁ N₂ : NearLitter} (h : N rw [← nonempty_coe_sort, ← mk_ne_zero_iff, mk_inter_of_fst_eq_fst h] exact mk_ne_zero κ +/-- Near-litters to different litters have small intersection. -/ theorem NearLitter.inter_small_of_fst_ne_fst {N₁ N₂ : NearLitter} (h : N₁.fst ≠ N₂.fst) : Small (N₁ ∩ N₂ : Set Atom) := by have := N₁.2.2 diff --git a/ConNF/BaseType/NearLitterPerm.lean b/ConNF/BaseType/NearLitterPerm.lean index 1eb9f697f2..1ca129fec9 100644 --- a/ConNF/BaseType/NearLitterPerm.lean +++ b/ConNF/BaseType/NearLitterPerm.lean @@ -30,9 +30,8 @@ variable [Params.{u}] {L : Litter} /-- A near-litter permutation is a permutation of atoms which sends near-litters to near-litters. -It turns out that the images of near-litters near the same litter are themselves near -the same litter. Hence a near-litter permutation induces a permutation of litters, and we keep that -as data for simplicity. +Then, the images of near-litters near the same litter must be near the same litter. Hence a +near-litter permutation induces a permutation of litters, and we keep that as data for simplicity. This is sometimes called a -1-allowable permutation. The proposition `near` can be interpreted as saying that if `s` is an `L`-near-litter, then its @@ -237,12 +236,6 @@ theorem smul_nearLitter_snd (π : NearLitterPerm) (N : NearLitter) : ((π • N).2 : Set Atom) = π • (N.2 : Set Atom) := smul_nearLitter_coe π N -@[simp] -theorem smul_localCardinal (π : NearLitterPerm) (L : Litter) : - π • localCardinal L = localCardinal (π • L) := by - ext N - simp [mem_smul_set, ← eq_inv_smul_iff] - @[simp] theorem NearLitter.mem_snd_iff (N : NearLitter) (a : Atom) : a ∈ (N.snd : Set Atom) ↔ a ∈ N := Iff.rfl diff --git a/ConNF/BaseType/Params.lean b/ConNF/BaseType/Params.lean index c9fc8ce469..aea5d1bf7b 100644 --- a/ConNF/BaseType/Params.lean +++ b/ConNF/BaseType/Params.lean @@ -26,7 +26,7 @@ used for lambda abstractions. Ordinals and cardinals are represented here as arbitrary types (not sets) with certain properties. For instance, `Λ` is an arbitrary type that has an ordering `<`, which is assumed to be a -well-ordering (the `Λwo` term is a proof of this fact). +well-ordering (the `Λ_isWellOrder` term is a proof of this fact). The prefix `#` denotes the cardinality of a type. -/ @@ -46,9 +46,8 @@ class Params where Λ_isLimit : (Ordinal.type ((· < ·) : Λ → Λ → Prop)).IsLimit /-- The type indexing the atoms in each litter. - Its cardinality is regular, and is larger than `Λ` but smaller than `κ`. - It also has an additive monoid structure, which is covariant in both variables with respect to the - ordering. + It is well-ordered, has regular cardinality, and is larger than `Λ` but smaller than `κ`. + It also has an additive monoid structure induced by its well-ordering. -/ κ : Type u [κ_linearOrder : LinearOrder κ] @@ -80,12 +79,14 @@ class Params where export Params (Λ κ μ) /-! -### Explicit parameters +## Explicit parameters There exist valid parameters for the model. The smallest such parameters are * `Λ := ℵ_0` * `κ := ℵ_1` * `μ = ℶ_{ω_1}`. + +We begin by creating a few instances that allow us to use cardinals to satisfy the model parameters. -/ theorem noMaxOrder_of_ordinal_type_eq {α : Type u} [Preorder α] [Infinite α] [IsWellOrder α (· < ·)] @@ -209,6 +210,8 @@ noncomputable def sub_of_isWellOrder {α : Type _} (Ordinal.typein (· < ·) x - Ordinal.typein (· < ·) y) ((Ordinal.sub_le_self _ _).trans_lt (Ordinal.typein_lt_type _ _)) +/-- The smallest set of valid parameters for the model. +They are instantiated in Lean's minimal universe `0`. -/ noncomputable def minimalParams : Params.{0} where Λ := ℕ Λ_zero_le := zero_le @@ -249,7 +252,7 @@ noncomputable def minimalParams : Params.{0} where variable [Params.{u}] {ι α β : Type u} -/-! The types `Λ`, `κ`, `μ` are inhabited and infinite. -/ +/-! Here, we unpack the hypotheses on `Λ`, `κ`, `μ` into instances that Lean can see. -/ theorem aleph0_le_mk_Λ : ℵ₀ ≤ #Λ := by have := Ordinal.card_le_card (Ordinal.omega_le_of_isLimit Params.Λ_isLimit) @@ -288,6 +291,10 @@ instance : NoMaxOrder μ := by rw [← Params.μ_ord] at this exact noMaxOrder_of_ordinal_type_eq this +/-! +## The ordered structure on `κ` +-/ + def κ_ofNat : ℕ → κ | 0 => 0 | n + 1 => Order.succ (κ_ofNat n) @@ -398,6 +405,10 @@ theorem κ_lt_sub_iff {i j k : κ} : k < i - j ↔ j + k < i := by rw [← Ordinal.typein_lt_typein (α := κ) (· < ·), ← Ordinal.typein_lt_typein (α := κ) (· < ·)] rw [Params.κ_add_typein, Params.κ_sub_typein, Ordinal.lt_sub] +/-! +## Type indices +-/ + /-- Either the base type or a proper type index (an element of `Λ`). The base type is written `⊥`. -/ @[reducible] @@ -413,15 +424,16 @@ instance : WellFoundedRelation Λ := instance : WellFoundedRelation TypeIndex := IsWellOrder.toHasWellFounded +/-- There are exactly `Λ` type indices. -/ @[simp] theorem mk_typeIndex : #TypeIndex = #Λ := mk_option.trans <| add_eq_left aleph0_le_mk_Λ <| one_le_aleph0.trans aleph0_le_mk_Λ -/-- Principal segments (sets of the form `{y | y < x}`) have cardinality `< μ`. -/ +/-- Sets of the form `{y | y < x}` have cardinality `< μ`. -/ theorem card_Iio_lt (x : μ) : #(Set.Iio x) < #μ := card_typein_lt (· < ·) x Params.μ_ord.symm -/-- Initial segments (sets of the form `{y | y ≤ x}`) have cardinality `< μ`. -/ +/-- Sets of the form `{y | y ≤ x}` have cardinality `< μ`. -/ theorem card_Iic_lt (x : μ) : #(Set.Iic x) < #μ := by rw [← Set.Iio_union_right, mk_union_of_disjoint, mk_singleton] -- TODO: This isn't the morally correct proof because it uses the fact `μ` is a limit cardinal. diff --git a/ConNF/BaseType/Small.lean b/ConNF/BaseType/Small.lean index 57eb266037..ffdbcbe326 100644 --- a/ConNF/BaseType/Small.lean +++ b/ConNF/BaseType/Small.lean @@ -29,6 +29,10 @@ def Small (s : Set α) : Prop := theorem Small.lt : Small s → #s < #κ := id +/-! +## Criteria for smallness +-/ + theorem Set.Subsingleton.small {α : Type _} {s : Set α} (hs : s.Subsingleton) : Small s := hs.cardinal_mk_le_one.trans_lt <| one_lt_aleph0.trans_le Params.κ_isRegular.aleph0_le @@ -98,6 +102,10 @@ theorem Small.pFun_image {α β : Type _} {s : Set α} (h : Small s) {f : α → rintro x ⟨y, ⟨z, hz₁, hz₂⟩, rfl⟩ exact ⟨z, hz₁, Part.eq_some_iff.mpr hz₂⟩ +/-! +## Nearness +-/ + /-- Two sets are near if their symmetric difference is small. -/ def IsNear (s t : Set α) : Prop := Small (s ∆ t) diff --git a/ConNF/NewTangle/Cloud.lean b/ConNF/NewTangle/Cloud.lean index f95f73261d..1795217b9e 100644 --- a/ConNF/NewTangle/Cloud.lean +++ b/ConNF/NewTangle/Cloud.lean @@ -47,8 +47,6 @@ variable [TangleDataLt] [PositionedTanglesLt] [TypedObjectsLt] [PositionedObject {γ : TypeIndex} [LtLevel γ] {β : Λ} [LtLevel β] (hγβ : γ ≠ β) --- TODO: Remove `localCardinal` - /-- The cloud map. We map each tangle to all typed near-litters near the `fuzz`ed tangle, and take the union over all tangles in the input. -/ def cloud (s : Set (TSet γ)) : Set (TSet β) := @@ -85,7 +83,7 @@ theorem cloud_nonempty (hγβ : γ ≠ β) : (cloud hγβ s).Nonempty ↔ s.None simp_rw [nonempty_iff_ne_empty, Ne.def, cloud_eq_empty] theorem subset_cloud (t : Tangle γ) (ht : t.set_lt ∈ s) : - typedNearLitter '' localCardinal (fuzz hγβ t) ⊆ cloud hγβ s := by + typedNearLitter '' {N | N.1 = fuzz hγβ t} ⊆ cloud hγβ s := by rintro _ ⟨N, hN, rfl⟩ exact ⟨t, ht, N, hN, rfl⟩ @@ -93,7 +91,7 @@ theorem μ_le_mk_cloud : s.Nonempty → #μ ≤ #(cloud hγβ s) := by rintro ⟨t, ht⟩ obtain ⟨t, rfl⟩ := exists_tangle_lt t refine' (Cardinal.mk_le_mk_of_subset <| subset_cloud t ht).trans_eq' _ - rw [Cardinal.mk_image_eq, mk_localCardinal] + rw [Cardinal.mk_image_eq, mk_nearLitter_to] exact typedNearLitter.inj' theorem subset_of_cloud_subset (s₁ s₂ : Set (TSet γ)) (h : cloud hγβ s₁ ⊆ cloud hγβ s₂) : diff --git a/docs/index.md b/docs/index.md index c88a9d0453..cf7fa771ca 100644 --- a/docs/index.md +++ b/docs/index.md @@ -9,7 +9,7 @@ In 1937, Quine proposed a set theory called "New Foundations", and since 2010, Randall Holmes has claimed to have a proof of its consistency. In this repository, we use the interactive theorem prover Lean to verify the difficult part of his proof, thus proving that New Foundations is indeed consistent. -The proof is now complete, and the theorem statements can be found in `ConNF/Model/Result.lean`. +The proof is now complete, and the theorem statements can be found in `ConNF/Model/Result.lean` ([source](https://github.com/leanprover-community/con-nf/blob/main/ConNF/Model/Result.lean), [docs](https://leanprover-community.github.io/con-nf/doc/ConNF/Model/Result.html)). See [our website](https://leanprover-community.github.io/con-nf/) for more information, the [documentation of our Lean code](https://leanprover-community.github.io/con-nf/doc/), and the [deformalisation paper](https://zeramorphic.github.io/con-nf-paper/main.l.pdf) that translates the Lean definitions into English. @@ -91,4 +91,3 @@ Note, however, that this choice is arbitrary, and any other finite axiomatisatio ## Dependency graph ![dependency graph](https://leanprover-community.github.io/con-nf/depgraph.png) -