--- title: "Von Neumann rank" module: L.Rank lang: en site: "Bedrock" description: "Von Neumann rank" stage: "Constructible stages and the axioms" reading_order: 27 canonical: https://bedrock.institute/en/L.Rank.html html: L.Rank.html agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/Rank.lagda.md prerequisites: [Base.Prelude, FOL.ZFStructure, V.Hierarchy, V.Model, L.Constructible, L.Ordinal] routes: [constructible-axioms] translations: [https://bedrock.institute/zh/L.Rank.md, https://bedrock.institute/ja/L.Rank.md] agent_guide: /llms.txt license: CC-BY-NC-SA-4.0 --- # Von Neumann rank The rank of a set is the union, over its members, of the successors of their ranks; in symbols, the computation theorem `rank-compute` identifies `rank x` with `rankStep x (λ y _ → rank y)`. Four facts about it are proved in this chapter: `rank-mono` says that rank strictly increases along membership, `rank-ord` says that rank is always an ordinal, `rank-upper` gives a conditional inclusion of a rank into an ordinal, and `rank-fix` says that rank fixes ordinals. Nothing here needs an external type of ordinals: rank takes values in the hierarchy itself, and the recursion runs on well-founded membership, which regularity directly guarantees. Thus every theorem in this chapter is proved without an excluded-middle parameter. Rank is defined inside the cumulative hierarchy `V ℓ`, with carrier `S`. A membership statement `x ∈ˢ y` is proposition-valued, and regularity makes this membership relation well-founded. The induction principle `∈-induction` can therefore define a value in `S` from values already defined for every member. ```agda {-# OPTIONS --cubical --safe --guardedness #-} open import Base.Prelude module L.Rank {ℓ : Level} where open import FOL.ZFStructure using ( module hPropStructure ) ``` For rank, the value at a set must collect the successor ranks of all its members. The operations `sucV` and small indexed union express this construction. Once the recursive member ranks are known to be ordinals, `suc-ord` and `setUnion-ord` show that the collected value is again an ordinal; `mem-ord` later supplies ordinality for members of an ordinal. ```agda open import V.Hierarchy {ℓ} using ( 𝒮ᵥ; extensionalV; ∈-induction; ∈-induction-compute ) open import V.Model {ℓ} using ( union-family-in; union-family-out; ∈sucV-elim; self∈sucV ) open import L.Constructible {ℓ} using ( IsOrd ) open import L.Ordinal {ℓ} using ( suc-ord; setUnion-ord; mem-ord ) ``` The indexing is genuinely small. Each set `x` has a small member type `⟪ x ⟫` and an embedding `⟪ x ⟫↪` into `S`; `∈ₛ⟪ x ⟫↪ m` proves that the represented set belongs to `x`. Conversely, a given membership proof can be converted by `∈-asFiber` into an index together with a path identifying its represented set with the member. These two directions connect recursion over membership with the small family used by the union. ```agda open import Cubical.Functions.Logic using ( ⇔toPath ) import Cubical.HITs.PropositionalTruncation as PT open import Cubical.HITs.CumulativeHierarchy.Base using ( sett ) open import Cubical.HITs.CumulativeHierarchy.Properties using ( ∈∈ₛ; ∈-asFiber; ⟪_⟫; ⟪_⟫↪; ∈ₛ⟪_⟫↪_ ) ``` The recursive step can now be read mathematically: take the small family of members, replace each member by the successor of its recursively computed rank, and form their union. The next section states this construction as `rankStep` and records its computation path. ```agda open import Cubical.HITs.CumulativeHierarchy.Constructions using ( ⋃_; module InfinitySet ) open InfinitySet using ( sucV ) open hPropStructure 𝒮ᵥ ``` ## The recursion The step takes the union, over the members of `x`, of the successors of their ranks. The recursive calls run over the *small* type of members, and the computation law holds propositionally as a path rather than definitionally, which is what later proofs use. The recursion equation says: to rank a set `x`, rank every member and take the union of the successors. Formally, the family being unioned is indexed by `⟪ x ⟫`, the small type of members, so the expression `⋃ (sett ⟪ x ⟫ …)` is a legal small union; the embedding `⟪ x ⟫↪` turns an index `m` into the actual set `⟪ x ⟫↪ m`, and the helper `mem` supplies the proof that this embedded set really is a member of `x`, which is what the recursive call `rec` demands. Note the shape of the step: it receives the recursive values through a function `rec` rather than calling `rank` directly, which is what makes it usable as the step of `∈-induction`. ```agda rankStep : (x : S) → (∀ y → y ∈ᵗ x → S) → S rankStep x rec = ⋃ (sett ⟪ x ⟫ (λ m → sucV (rec (⟪ x ⟫↪ m) (mem m)))) where mem : (m : ⟪ x ⟫) → ⟪ x ⟫↪ m ∈ᵗ x mem m = ∈∈ₛ {a = ⟪ x ⟫↪ m} {b = x} .snd (∈ₛ⟪ x ⟫↪ m) ``` The rank itself is the membership induction applied to this step: `∈-induction rankStep` turns the step function into a total family on all of `S`. The definition is marked `opaque` to keep the checker from unfolding the well-founded eliminator inside it. What is available instead is the computation law `rank-compute`, which exposes the recursion equation as a propositional path: `rank x` is a path to `rankStep x (λ y _ → rank y)`, the same equation with `rank` itself filling every recursive call. Later proofs rewrite by this path rather than reducing `rank` directly. ```agda opaque rank : S → S rank = ∈-induction rankStep rank-compute : (x : S) → rank x ≡ rankStep x (λ y _ → rank y) rank-compute = ∈-induction-compute rankStep ``` ## Rank strictly increases along membership The theorem `rank-mono` states that if `x ∈ˢ y` then `rank x ∈ˢ rank y`. It follows directly from the shape of the defining union: `rank y` is a union of successors `sucV (rank w)` indexed by the members `w` of `y`, so exhibiting `rank x` as a member of one such successor suffices. No `IsOrd` hypothesis appears anywhere in the statement. Given `x ∈ˢ y`, the goal is `rank x ∈ˢ rank y`. Unfold `rank y` once by `rank-compute`: the goal becomes membership in the union `⋃ (sett ⟪ y ⟫ (λ m → sucV (rank (⟪ y ⟫↪ m))))`. Now it suffices to exhibit `rank x` as a member of one family member, namely `sucV (rank w)` for some member `w` of `y`; `self∈sucV` puts `rank x` inside its own successor, and `union-family-in` lifts that into the union, transport along the computation path included. ```agda rank-mono : (x y : S) → ⟨ x ∈ˢ y ⟩ → ⟨ rank x ∈ˢ rank y ⟩ rank-mono x y x∈y = subst (λ w → ⟨ rank x ∈ˢ w ⟩) (sym (rank-compute y)) (union-family-in ⟪ y ⟫ (λ m → sucV (rank (⟪ y ⟫↪ m))) (fib .fst) (rank x) (subst (λ w → ⟨ rank x ∈ˢ sucV (rank w) ⟩) (sym (fib .snd)) (self∈sucV (rank x)))) where ``` The remaining piece is where the index for the union member comes from. The function `∈-asFiber` turns the given proof `x∈y` into a fiber of the embedding `⟪ y ⟫↪`: a pair whose first component `fib .fst` is an index into `⟪ y ⟫`, and whose second component `fib .snd` is a path saying that the indexed set equals `x`. That path is transported along so that the membership in the successor speaks of `rank x` itself; this is exactly what the code shows. ```agda fib = ∈-asFiber {a = x} {b = y} x∈y ``` ## Rank is an ordinal One membership induction. Unfold once by `rank-compute`; the inductive hypothesis makes each member's rank an ordinal, the closure lemma `suc-ord` makes each successor an ordinal, and the closure lemma `setUnion-ord` makes the union of that family of ordinals an ordinal again. The statement quantifies over all sets, so the proof is a membership induction with the predicate `λ A → IsOrd (rank A)`. The induction hypothesis hands us, for each member `y` of `A`, the certificate that `rank y` is an ordinal. Since `rank-compute A` propositionally identifies `rank A` with the step, the goal is reached by transporting `IsOrd` along the computation path `rank-compute A`, so what remains is to show that the union of the step is an ordinal. ```agda rank-ord : (A : S) → IsOrd (rank A) rank-ord = ∈-induction {P = λ A → IsOrd (rank A)} step where step : (A : S) → (∀ y → y ∈ᵗ A → IsOrd (rank y)) → IsOrd (rank A) step A IH = subst IsOrd (sym (rank-compute A)) ``` That last step composes two closure facts. Each family member `sucV (rank (⟪ A ⟫↪ m))` is the successor of an ordinal, hence an ordinal by `suc-ord`, with the induction hypothesis and the helper `mem` supplying the input certificate. Then `setUnion-ord` closes the small indexed union of ordinals under union. The chain from hypothesis to conclusion: if the ranks of the members are ordinals, so is the rank of the set. ```agda (setUnion-ord ⟪ A ⟫ (λ m → sucV (rank (⟪ A ⟫↪ m))) (λ m → suc-ord (IH (⟪ A ⟫↪ m) (mem m)))) where mem : (m : ⟪ A ⟫) → ⟪ A ⟫↪ m ∈ᵗ A mem m = ∈∈ₛ {a = ⟪ A ⟫↪ m} {b = A} .snd (∈ₛ⟪ A ⟫↪ m) ``` ## Bounding a rank If every member's rank lies in an ordinal, the rank of the set is included in that ordinal. Every member of the defining union lies in a successor of a member's rank; transitivity closes the inclusion. Both ordinal fixed points and bounds on the ranks in a constructible stage use this argument. The statement is a pointwise inclusion, not a strict membership: assuming `IsOrd β` and that every member rank `rank y` lies strictly in `β`, it concludes that every member of `rank A` lies in `β`. The proof eliminates from the shape of the defining union. Membership in the union yields, via `union-family-out`, merely an index `m` with `x ∈ˢ s m`; since the target `x ∈ˢ β` is a proposition, eliminating this truncation is legitimate, and `∈sucV-elim` then splits membership in the successor `s m = sucV (rank (⟪ A ⟫↪ m))` into its two cases. ```agda rank-upper : (A β : S) → IsOrd β → ((y : S) → ⟨ y ∈ˢ A ⟩ → ⟨ rank y ∈ˢ β ⟩) → (x : S) → ⟨ x ∈ˢ rank A ⟩ → ⟨ x ∈ˢ β ⟩ rank-upper A β oβ bound x hx = PT.rec (snd (x ∈ˢ β)) (λ { (m , hm) → ∈sucV-elim (snd (x ∈ˢ β)) hm ``` The two cases of the successor are where ordinality earns its keep. If `x` is a member of `rank (⟪ A ⟫↪ m)`, then since β is transitive and that rank is already in β, so is `x`: this is the branch `oβ .fst h (below m)`. If instead `x` equals `rank (⟪ A ⟫↪ m)` outright, the second branch transports the bound `below m` across that path. Either way the conclusion lands in `x ∈ˢ β`. What the eliminator receives from the union is `hm : ⟨ x ∈ˢ s m ⟩` merely, so the fiber `(m , hm)` is consumed inside a propositional elimination and no index is ever extracted as data. ```agda (λ h → oβ .fst h (below m)) (λ q → subst (λ w → ⟨ w ∈ˢ β ⟩) (sym q) (below m)) }) (union-family-out ⟪ A ⟫ s x (subst (λ w → ⟨ x ∈ˢ w ⟩) (rank-compute A) hx)) where ``` The family `s` is the successor-rank family from the recursion equation, sending an index `m` to `sucV (rank (⟪ A ⟫↪ m))`. The fact `below m` is the hypothesis `bound` applied to the embedded member `⟪ A ⟫↪ m` together with its membership proof, yielding `rank (⟪ A ⟫↪ m) ∈ˢ β`. The whole lemma therefore uses no induction: rewrite by the computation law, take the union apart, and let the ordinal's transitivity absorb the successor. ```agda s : ⟪ A ⟫ → S s m = sucV (rank (⟪ A ⟫↪ m)) below : (m : ⟪ A ⟫) → ⟨ rank (⟪ A ⟫↪ m) ∈ˢ β ⟩ below m = bound (⟪ A ⟫↪ m) (∈∈ₛ {a = ⟪ A ⟫↪ m} {b = A} .snd (∈ₛ⟪ A ⟫↪ m)) ``` ## Ordinals are their own rank Again by membership induction, and this time the proof is an extensionality between `rank A` and `A`. Left to right, an element of `rank A` sits inside the successor of the rank of some member, and that rank *is* the member by the inductive hypothesis, so the element is the member or belongs to it, and either way it belongs to `A` by transitivity. Right to left, a member of `A` is the rank of itself, hence belongs to the successor of that rank, which is one branch of the union. The theorem states that rank fixes every ordinal, as a path rather than an iff. The induction is set up with a predicate that packages the ordinality hypothesis together with the conclusion, `λ A → IsOrd A → rank A ≡ A`, because the step genuinely needs it: to compare rank A with A it must know that members of the ordinal A are themselves ordinals. So the step receives, alongside the recursive equalities `rank y ≡ y`, the certificate `IsOrd A` and returns the equality at `A`. ```agda rank-fix : (A : S) → IsOrd A → rank A ≡ A rank-fix = ∈-induction {P = λ A → IsOrd A → rank A ≡ A} step where step : (A : S) → (∀ y → y ∈ᵗ A → IsOrd y → rank y ≡ y) → IsOrd A → rank A ≡ A ``` The equality itself comes from `extensionalV`, which turns a pointwise equivalence of membership into a path of sets, and `⇔toPath` packages the two directions. the two sets being compared stay folded. The forward direction `toA` is none other than `rank-upper` at `β = A`: the ordinal bound on member ranks is `A` itself, and the bounding hypothesis is produced on the fly from the induction hypothesis. ```agda step A IH ordA = extensionalV (λ x → ⇔toPath (toA x) (fromA x)) where toA : (x : S) → ⟨ x ∈ˢ rank A ⟩ → ⟨ x ∈ˢ A ⟩ toA = rank-upper A A ordA (λ y hy → subst (λ w → ⟨ w ∈ˢ A ⟩) ``` Both bounding directions lean on the same fact, `mem-ord`: a member of the ordinal A is again an ordinal, so the induction hypothesis applies to it. For `toA`, the hypothesis required by `rank-upper` is `rank y ∈ˢ A`; since `rank y ≡ y` by IH and `y ∈ˢ A` is given, the transport lands it. For `fromA`, the reverse holds: `rank-mono x A x∈A` gives `rank x ∈ˢ rank A`, and the path `rank x ≡ x` from the IH transports it to `x ∈ˢ rank A`. Every ingredient is now in place, and the path `rank A ≡ A` follows. ```agda (sym (IH y hy (mem-ord {A = A} ordA y hy))) hy) fromA : (x : S) → ⟨ x ∈ˢ A ⟩ → ⟨ x ∈ˢ rank A ⟩ fromA x x∈A = subst (λ w → ⟨ w ∈ˢ rank A ⟩) (IH x x∈A (mem-ord {A = A} ordA x x∈A)) (rank-mono x A x∈A) ``` ## Recap `rank` measures every set by an ordinal (`rank-ord`) and fixes the ordinals themselves (`rank-fix`), which show that it is an ordinal-valued measure agreeing with each ordinal. Both proofs are membership inductions on regularity, so the chapter uses no additional assumptions. It gives a strict ordinal-valued measure of membership and the fixed-point law needed when the measured set is already an ordinal.