Grace/Cumulus/Set/Hierarchy.g17

Open in Workbench Download source

Imports

Ordinal · Cumulus.Relation

Declarations

• finite def
• FiniteStage class
• finite.zero theorem derivation
• finite.next theorem derivation
• finite.next_membership theorem derivation
• FiniteStage.membership theorem derivation
• V def
• V.zero theorem derivation
• V.next theorem derivation
• V.limit theorem derivation
• V.history.contains theorem derivation
• V.limit_membership theorem derivation
• rank def
• rank.unfold theorem derivation
• rank.history_characterization theorem derivation
• rank.history.contains theorem derivation
• rank.ordinal theorem derivation
• rank.supremum_ordinal theorem derivation
• rank.member_subset_supremum theorem derivation
• rank.member_bound theorem derivation
• rank.member theorem derivation
• rank.history_empty theorem derivation
• rank.empty theorem derivation
• rank.history_singleton theorem derivation
• rank.singleton theorem derivation
• rank.history_pair theorem derivation
• rank.pair theorem derivation
• Transitive.powerset theorem derivation
• V.subset_next theorem derivation
• V.transitive_and_monotone theorem derivation
• V.transitive theorem derivation
• V.monotone theorem derivation
• rank.membership theorem derivation
• rank.exists theorem derivation
• finite.transitive theorem derivation
• finite.subset_next theorem derivation
• Value predicate
• DomainThrough predicate
• earlierValues def
• StageClause predicate
• Approximation predicate
• Stage predicate
• StageExists predicate
• StageUnique predicate
• HierarchyResolvedThrough predicate
• CumulativeUniverse class
• Ranked class
• CumulativeUniverse.membership theorem derivation
• CumulativeUniverse.eq_Universe_of_rank theorem derivation
• CumulativeUniverse.eq_Universe theorem derivation

Source

1-- The cumulative hierarchy2-- Part of Cumulus, the Grace17 mathematics library.3-- Copyright (c) 2026 Grant Passmore.4-- Released under the Apache License 2.0. See LICENSE in the repository root.5-- Authors: Grant Passmore67module Grace.Cumulus.Set.Hierarchy8import Ordinal9import Cumulus.Relation1011-- Executable finite stages: V_0 = empty and V_(n+1) = P(V_n).12def finite (n : Nat) → Set13  | zero => ∅14  | succ(n) => 𝒫(finite(n))1516class FiniteStage (n : Nat) := { x : Set | x ∈ finite(n) }1718theorem finite.zero19  shows finite(0) = ∅20proof21  simp2223theorem finite.next (n : Nat)24  shows finite(succ(n)) = 𝒫(finite(n))25proof26  simp [finite]2728theorem finite.next_membership (x : Set, n : Nat)29  shows x ∈ finite(succ(n)) ↔ (x ⊆ finite(n))30proof31  simp [finite, set.powerset, Subset]3233theorem FiniteStage.membership (x : Set, n : Nat)34  shows x ∈ FiniteStage(n) ↔ x ∈ finite(n)35proof36  simp [FiniteStage]3738-- The full hierarchy is one noncomputable class-sized recursion.  At a limit,39-- the comprehension denotes the Replacement set of all earlier values.40noncomputable transfinite def V (α : Ordinal) : Set41  | 0 => ∅42  | succ β => 𝒫(V β)43  | limit λ => ⋃ { V β | β < λ }4445theorem V.zero46  shows V(0) = ∅47proof48  simp [V, nat.zero]4950theorem V.next (α : Ordinal)51  shows V(next(α)) = 𝒫(V(α))52proof53  simp [V.equation.successor]5455theorem V.limit (λ : Set)56  requires h : Limit(λ)57  shows V(λ) = ⋃(Relation.range(V.history(λ)))58proof59  simp [V.equation.limit]6061theorem V.history.contains (β λ : Set)62  requires hBeta : β ∈ λ63  shows (β ↦ V(β)) ∈ V.history(λ)64proof65  simp [V.history.membership]6667theorem V.limit_membership (x λ : Set)68  requires hLimit : Limit(λ)69  shows x ∈ V(λ) ↔ ∃ earlier ∈ λ, x ∈ V(earlier)70proof71  constructor72  . intro hx73    have hEquation := V.limit with hLimit74    rw hEquation at hx75    simp [set.union] at hx76    obtain ⟨stage, hStageRange, hxStage⟩ := hx77    simp [Relation.range] at hStageRange78    obtain ⟨hStageBound, index, hPair⟩ := hStageRange79    simp [V.history.membership] at hPair80    obtain ⟨β, hBeta, hEquality⟩ := hPair81    obtain ⟨hIndex, hValue⟩ := Relation.orderedPair.injective with hEquality82    refine ⟨β, hBeta, ?_⟩83    rwa hValue at hxStage84  . intro hEarlier85    obtain ⟨source, hSource, hxSource⟩ := hEarlier86    have hHistory := V.history.contains with hSource87    have hRange := Relation.range.contains with hHistory88    have hEquation := V.limit with hLimit89    rw hEquation90    exact set.union.backward with ⟨V(source), hRange, hxSource⟩9192-- A Foundation-recursive height for every set. The history at x is the93-- Replacement graph of the already-defined heights of exactly the members of94-- x. Taking one successor above their supremum is sufficient for ranking.95noncomputable foundation def rank (x : Set) : Set96  | x using history => next(⋃(Relation.range(history)))9798theorem rank.unfold (x : Set)99  shows rank(x) = next(⋃(Relation.range(rank.history(x))))100proof101  simp [rank.equation]102103theorem rank.history_characterization (p x : Set)104  shows p ∈ rank.history(x) ↔ ∃ y ∈ x, p = (y ↦ rank(y))105proof106  simp [rank.history.membership]107108theorem rank.history.contains (y x : Set)109  requires hy : y ∈ x110  shows (y ↦ rank(y)) ∈ rank.history(x)111proof112  simp [rank.history_characterization]113114theorem rank.ordinal (x : Set)115  shows rank(x) ∈ Ordinal116proof117  induction x using membership118  intros current ih119  rw rank.unfold120  apply Grace.Cumulus.Set.Ordinal.Ordinal.next121  apply Ordinal.union122  intros α hAlpha123  simp [Relation.range] at hAlpha124  cases hAlpha with hBound ∧ hWitness125  obtain ⟨member, hPair⟩ := hWitness126  simp [rank.history_characterization] at hPair127  obtain ⟨source, hSourcePair⟩ := hPair128  cases hSourcePair with hSource ∧ hEquality129  have injective := Relation.orderedPair.injective with hEquality130  cases injective with hMember ∧ hValue131  have hRank := ih with hSource132  rwa hValue133134theorem rank.supremum_ordinal (x : Set)135  shows ⋃(Relation.range(rank.history(x))) ∈ Ordinal136proof137  apply Ordinal.union138  intros α hAlpha139  simp [Relation.range] at hAlpha140  cases hAlpha with hBound ∧ hWitness141  obtain ⟨member, hPair⟩ := hWitness142  simp [rank.history_characterization] at hPair143  obtain ⟨source, hSourcePair⟩ := hPair144  cases hSourcePair with hSource ∧ hEquality145  have injective := Relation.orderedPair.injective with hEquality146  cases injective with hMember ∧ hValue147  rw hValue148  exact rank.ordinal149150theorem rank.member_subset_supremum (y x : Set)151  requires hy : y ∈ x152  shows (rank(y) ⊆ ⋃(Relation.range(rank.history(x))))153proof154  intros z hz155  apply set.union.backward156  witness rank(y)157  constructor158  have hHistory := rank.history.contains with hy159  exact Relation.range.contains with hHistory160  exact hz161162theorem rank.member_bound (y x : Set)163  requires hy : y ∈ x164  shows rank(y) ∈ next(⋃(Relation.range(rank.history(x))))165proof166  simp [rank.member_subset_supremum, Ordinal.subset_bound]167168-- Membership strictly lowers rank. This is the fundamental usable interface169-- to the Foundation-recursive definition above.170theorem rank.member (y x : Set)171  requires hy : y ∈ x172  shows rank(y) ∈ rank(x)173proof174  simp [rank.member_bound, rank.unfold]175176theorem rank.history_empty177  shows rank.history(∅) = ∅178proof179  ext y180  simp [rank.history_characterization, set.empty]181182theorem rank.empty183  shows rank(∅) = next(∅)184proof185  rw [rank.unfold, rank.history_empty, Relation.range.empty, union.empty]186  rfl187188theorem rank.history_singleton (x : Set)189  shows rank.history({x}) = {(x ↦ rank(x))}190proof191  ext y192  simp [set.extensionality, rank.history_characterization, singleton.membership]193194theorem rank.singleton (x : Set)195  shows rank({x}) = next(rank(x))196proof197  rw [rank.unfold, rank.history_singleton, Relation.range.singleton_pair, union.singleton]198  rfl199200theorem rank.history_pair (x y : Set)201  shows rank.history({x, y}) = {(x ↦ rank(x)), (y ↦ rank(y))}202proof203  ext p204  constructor205  . intro hp206    obtain ⟨member, hMember, hValue⟩ := rank.history_characterization.forward with hp207    simp [pair.membership] at hMember208    cases hMember with hMemberX | hMemberY209    . rw hMemberX at hValue210      apply pair.membership.backward211      left212      exact hValue213    . rw hMemberY at hValue214      apply pair.membership.backward215      right216      exact hValue217  . intro hp218    simp [pair.membership] at hp219    cases hp with hFirst | hSecond220    . exact rank.history_characterization.backward with ⟨x, pair.left, hFirst⟩221    . exact rank.history_characterization.backward with ⟨y, pair.right, hSecond⟩222223theorem rank.pair (x y : Set)224  shows rank({x, y}) = next(rank(x) ∪ rank(y))225proof226  rw [rank.unfold, rank.history_pair, Relation.range.pair_of_pairs]227  unfold union2228  rfl229230-- Powersets preserve transitivity: an element of an element of P(A) is231-- already an element of A when A is transitive.232theorem Transitive.powerset (A : Set)233  requires h : Transitive(A)234  shows Transitive(𝒫(A))235proof236  simp [Transitive, Subset, set.powerset]237238theorem V.subset_next (α : Set)239  requires hOrdinal : α ∈ Ordinal240  requires hTransitive : Transitive(V(α))241  shows (V(α) ⊆ V(next(α)))242proof243  have hEquation := V.next with hOrdinal244  rw hEquation245  intros x hx246  apply set.powerset.backward247  exact hTransitive with x, hx248249-- Transitivity and monotonicity mutually support one another at successor250-- stages, so derive them in a single Foundation induction on the ordinal.251theorem V.transitive_and_monotone (β : Set)252  shows β ∈ Ordinal → (Transitive(V(β)) ∧ (∀ α, α ∈ Ordinal → α ∈ next(β) → (V(α) ⊆ V(β))))253proof254  induction β using membership255  intros current ih hCurrentOrdinal256  have hCases := Ordinal.cases with hCurrentOrdinal257  cases hCases with hZero | hNonzero258  . rw hZero259    constructor260    . rw [← nat.zero, V.zero]261      exact Transitive.empty262    . intros α hAlphaOrdinal hAlphaBound263      simp [next.membership] at hAlphaBound264      cases hAlphaBound with hAlphaEmpty | hAlphaEqual265      . exfalso266        rw hZero at hAlphaEmpty267        exact set.empty with hAlphaEmpty268      . rw hAlphaEqual269        exact Subset.reflexive270  . cases hNonzero with hSuccessor | hLimit271    . obtain ⟨γ, hGammaCurrent, hNextCurrent⟩ := hSuccessor272      have hGammaOrdinal := Ordinal.member with hCurrentOrdinal, hGammaCurrent273      obtain ⟨hGammaTransitive, hGammaMonotone⟩ := ih with hGammaCurrent, hGammaOrdinal274      rw ← hNextCurrent275      constructor276      . have hNextEquation := V.next with hGammaOrdinal277        rw hNextEquation278        exact Transitive.powerset with hGammaTransitive279      . intros α hAlphaOrdinal hAlphaBound280        simp [next.membership] at hAlphaBound281        cases hAlphaBound with hAlphaEarlier | hAlphaEqual282        . rw ← hNextCurrent at hAlphaEarlier283          have hAlphaGammaSubset := hGammaMonotone with hAlphaOrdinal, hAlphaEarlier284          have hGammaNextSubset := V.subset_next with hGammaOrdinal, hGammaTransitive285          rw hNextCurrent at hGammaNextSubset286          intros x hx287          exact hGammaNextSubset with x, (hAlphaGammaSubset with x, hx)288        . rw hAlphaEqual289          exact Subset.reflexive290    . constructor291        intros x hx292        have hMembershipAtX := V.limit_membership at x, current with hLimit293        simp [hMembershipAtX] at hx294        obtain ⟨stage, hStageCurrent, hxStage⟩ := hx295        have hStageOrdinal := Ordinal.member with hCurrentOrdinal, hStageCurrent296        obtain ⟨hStageTransitive, hStageMonotone⟩ := ih with hStageCurrent, hStageOrdinal297        intros y hy298        have hxSubset := hStageTransitive with x, hxStage299        have hyStage := hxSubset with y, hy300        have hMembershipAtY := V.limit_membership at y, current with hLimit301        simp [hMembershipAtY]302      . intros α hAlphaOrdinal hAlphaBound303        simp [next.membership] at hAlphaBound304        cases hAlphaBound with hAlphaCurrent | hAlphaEqual305          intros x hx306          have hLimitContainment := V.limit_membership at x, current with hLimit307          simp [hLimitContainment]308        . rw hAlphaEqual309          exact Subset.reflexive310311theorem V.transitive (α : Set)312  requires hOrdinal : α ∈ Ordinal313  shows Transitive(V(α))314proof315  simp [V.transitive_and_monotone]316317theorem V.monotone (α β : Set)318  requires hAlpha : α ∈ Ordinal319  requires hBeta : β ∈ Ordinal320  requires hBound : α ∈ next(β)321  shows (V(α) ⊆ V(β))322proof323  simp [V.transitive_and_monotone, Subset]324325theorem rank.membership (x : Set)326  shows x ∈ V(rank(x))327proof328  induction x using membership329  intros current ih330  rw rank.unfold331  have hSupremumOrdinal := rank.supremum_ordinal at current332  have hSuccessorEquation := V.next with hSupremumOrdinal333  rw hSuccessorEquation334  apply set.powerset.backward335  intros member hMember336  have hMemberRanked := ih with hMember337  have hMemberBound := rank.member_bound with hMember338  have hMonotone := V.monotone at rank(member), ⋃(Relation.range(rank.history(current))) with rank.ordinal at member, hSupremumOrdinal, hMemberBound339  exact hMonotone with member, hMemberRanked340341theorem rank.exists (x : Set)342  shows ∃ α, α ∈ Ordinal ∧ x ∈ V(α)343proof344  refine ⟨rank(x), rank.ordinal at x, rank.membership at x⟩345346theorem finite.transitive (n : Nat)347  shows Transitive(finite(n))348proof349  induction n350  | zero => settle with finite, Transitive.empty351  | succ(k) using ih => settle with finite, Transitive.powerset352353-- Hence every finite stage embeds into its successor stage.354theorem finite.subset_next (n : Nat)355  shows (finite(n) ⊆ finite(succ(n)))356proof357  simp [Subset, finite, set.powerset, finite.transitive, Transitive]358359-- A first-order graph presentation of transfinite hierarchy approximations.360predicate Value (f i x : Set) := (i ↦ x) ∈ f ∧ (∀ y, (i ↦ y) ∈ f → y = x)361predicate DomainThrough (f α : Set) := ∀ β, β ∈ next(α) ↔ ∃ x, (β ↦ x) ∈ f362def earlierValues (f β : Set) : Set := { x ∈ ⋃(⋃(f)) | ∃ γ ∈ β, (γ ↦ x) ∈ f }363predicate StageClause (f β x : Set) := (β = ∅ ∧ x = ∅) ∨ (∃ γ, γ ∈ Ordinal ∧ β = next(γ) ∧ ∃ y, Value(f, γ, y) ∧ x = 𝒫(y)) ∨ (Limit(β) ∧ x = ⋃(earlierValues(f, β)))364predicate Approximation (f α : Set) := DomainThrough(f, α) ∧ (∀ β ∈ next(α), ∃ x, Value(f, β, x) ∧ StageClause(f, β, x))365predicate Stage (α X : Set) := α ∈ Ordinal ∧ ∃ f, Approximation(f, α) ∧ Value(f, α, X)366predicate StageExists (α : Set) := ∃ X, Stage(α, X)367predicate StageUnique (α : Set) := ∀ X, Stage(α, X) → ∀ Y, Stage(α, Y) → X = Y368predicate HierarchyResolvedThrough (α : Set) := ∀ β ∈ next(α), (StageExists(β) ∧ StageUnique(β))369370class CumulativeUniverse (x : Set) := { x | ∃ α, α ∈ Ordinal ∧ x ∈ V(α) }371class Ranked (x : Set) := { x | ∃ α, α ∈ Ordinal ∧ x ∈ V(α) }372373theorem CumulativeUniverse.membership (x : Set)374  shows x ∈ CumulativeUniverse ↔ ∃ α, α ∈ Ordinal ∧ x ∈ V(α)375proof376  simp [CumulativeUniverse]377378theorem CumulativeUniverse.eq_Universe_of_rank379  requires ranks : ∀ x, ∃ α, α ∈ Ordinal ∧ x ∈ V(α)380  shows CumulativeUniverse = Universe381proof382  simp383384theorem CumulativeUniverse.eq_Universe385  shows CumulativeUniverse = Universe386proof387  apply CumulativeUniverse.eq_Universe_of_rank388  intro x389  exact rank.exists390