BedrockLocating ordinals in the constructible hierarchy
Read this chapter directly, or use the reading guide and dependency map to choose another route.
Reading guide · Dependency mapAn ordinal's position in the constructible hierarchy is controlled by membership: it appears by its successor stage and cannot appear before its own rank. This chapter proves both directions and gives a bounded formula for recognizing ordinals inside a stage.
One question about the tower is still open, and it is the one the axiom of infinity turns on: given a stage, exactly which ordinals have appeared by then? The answer is as clean as it could be. The ordinals in Lset α are precisely the members of α, so the tower's index and its ordinal content agree, level for level, and an ordinal first appears at the stage after itself.
Both directions require real work. One direction says an ordinal cannot appear early: if it is in Lset α then it is a member of α. That is the harder one, and it goes through rank, which is why the rank construction is needed here. A set in Lset α is a definable subset of some earlier stage, its members therefore have rank below that stage by induction, and so its own rank is bounded; being an ordinal, it is its own rank.
The other direction says an ordinal cannot appear late: every member of α is already in Lset α. That one is a straight induction, given that an ordinal appears at the stage after itself, which is the theorem being proved. The circularity is only apparent: the induction hypothesis supplies the statement for the members, and the members are the only thing needed.
With both halves the ordinals of a stage are carved out of it by a single formula, "is an ordinal", which is Δ₀ because transitivity can be said with bounded quantifiers alone. So α is a definable subset of Lset α, and the definable-power-set clause for the successor stage then applies.
The chapter works inside a fixed universe level ℓ, and everything that follows speaks about sets, membership, and stages of L at that level. We assume excluded middle at level ℓ-suc ℓ. Its sole mathematical use is ordinal trichotomy: for two ordinals, one of membership in either direction or equality is returned. Every later conclusion inherits this classicality through the two comparison lemmas built in the next section.
{-# OPTIONS --cubical --safe --guardedness #-} open import Base.Prelude open import Base.Classical using ( LEM ) module L.Ordinal.Stages {ℓ : Level} (lem : LEM (ℓ-suc ℓ)) where
Two kinds of vocabulary meet here. From the ambient hierarchy V come the basic moves: membership ∈ˢ on the set S, the von Neumann successor sucV, induction and irreflexivity along membership. From the constructible side come the stages Lset α themselves, the definable-subset layer 𝒟ₒ, and the two directions Lset-in and Lset-out relating membership in a stage to membership in its definable power set. The chapter's statement lives entirely in this intersection: it asks where an ordinal sits among the Lset α.
open import FOL.ZFStructure using ( module hPropStructure ) open import FOL.Syntax using ( Formula; var; _∈̇_; _∧̇_; ∀̇∈ ) open import FOL.LevyHierarchy using ( Δ₀; δ-∈; δ-∧; δ-∀∈ ) open import FOL.Manipulation.ConstantMapping using ( mapFo ) open import V.Hierarchy {ℓ} using ( 𝒮ᵥ; ∈-induction; ∈-irrefl )
Ordinals enter as the predicate IsOrd: a set is an ordinal exactly when it is transitive and all of its members are transitive. This is the von Neumann reading, where the ordinal α is the set of all smaller ordinals, so asking whether an ordinal has appeared at a stage is literally a membership question. Also from earlier chapters come mem-ord and suc-ord, the closure facts that a member of an ordinal is an ordinal and that the successor of an ordinal is an ordinal; they keep every stage index in the argument an honest ordinal.
open import V.Model {ℓ} using ( ∈sucV-elim; ∈sucV-inl; self∈sucV ) open import L.Definability {ℓ} using ( module DefOf ) open import L.Constructible {ℓ} using ( IsOrd; isTransV; Lset; Lset-layer; layer-trans ; 𝒟ₒ; 𝒟ₒ-intro; 𝒟ₒ-inv; Lset-mono; Lset-in; Lset-out )
The decision procedure behind everything is ord-tri: given two ordinals, each certified to be one, it returns which of the three cases holds, a ∈ b, a = b, or b ∈ a. It uses the stated excluded-middle assumption. The comparison returns a sum of three cases; impossible branches land in the empty type. Separately, propositional truncation ∣_∣₁ records that the earlier stage witnessing a stage decomposition merely exists.
open import L.Ordinal {ℓ} using ( mem-ord; suc-ord ) open import L.Ordinal.Linear {ℓ} lem using ( ord-tri ) open import L.Rank {ℓ} using ( rank; rank-upper; rank-ord; rank-fix ) open import Cubical.Data.Sum as Sum using ( _⊎_; inl; inr ) import Cubical.Data.Empty as Empty
The rank construction supplies three properties. For a set x, rank x is an ordinal collecting how deep x sits in the cumulative hierarchy; rank-ord certifies it is an ordinal, rank-fix identifies the rank of an ordinal with the ordinal itself, and rank-upper bounds the rank of a set from bounds on the ranks of its members. These are the facts needed for the harder direction.
import Cubical.HITs.PropositionalTruncation as PT open PT using ( ∣_∣₁ ) open import Cubical.HITs.CumulativeHierarchy.Properties using ( ∈∈ₛ; ∈-asFiber; ⟪_⟫; ⟪_⟫↪; extensionality; _⊆_ ) open import Cubical.HITs.CumulativeHierarchy.Constructions
To connect ambient membership with formulas over a stage, a set A has a chosen presentation ⟪ A ⟫, and ∈-asFiber passes from membership in A to an index naming that member. Mutual inclusion gives equality through extensionality. Formula satisfaction is interpreted directly in hProp: each formula denotes an hProp. These identifications let the argument pass between sets, their indices and bounded formulas.
using ( module InfinitySet ) open InfinitySet using ( sucV ) open hPropStructure 𝒮ᵥ
Comparison, twice
Trichotomy leaves exactly three mathematical possibilities. If a belongs to b, it belongs to the successor of b; if a = b, then a belongs to that successor as its new top element. The only remaining possibility, b ∈ a, will be ruled out by the inclusion a ⊆ b.
Suppose a ⊆ b for sets a and b, and compare them by trichotomy. If a is a member of b, the first helper applies ∈sucV-inl: a member of b is automatically a member of sucV b, since the successor is b together with its singleton. If a equals b, the second helper transports the fact self∈sucV b, that b belongs to its own successor, along the path a ≡ b. Two of the three cases are already closed.
private ∈-case : (a b : S) → ⟨ a ∈ˢ b ⟩ → ⟨ a ∈ˢ sucV b ⟩ ∈-case a b a∈b = ∈sucV-inl a∈b ≡-case : (a b : S) → a ≡ b → ⟨ a ∈ˢ sucV b ⟩ ≡-case a b a≡b = subst (λ w → ⟨ w ∈ˢ sucV b ⟩) (sym a≡b) (self∈sucV b)
The remaining case is b ∈ a, which inclusion rules out: b ∈ a and a ⊆ b would give b ∈ b, contradicting ∈-irrefl. From this contradiction the desired conclusion a ∈ sucV b follows. Hence for ordinals a and b, inclusion a ⊆ b forces a ∈ sucV b.
wit-case : (a b : S) → ((y : S) → ⟨ y ∈ˢ a ⟩ → ⟨ y ∈ˢ b ⟩) → ⟨ b ∈ˢ a ⟩ → ⟨ a ∈ˢ sucV b ⟩ wit-case a b a⊆b b∈a = Empty.rec (∈-irrefl b (a⊆b b b∈a)) ⊆→∈suc : (a b : S) → IsOrd a → IsOrd b → ((y : S) → ⟨ y ∈ˢ a ⟩ → ⟨ y ∈ˢ b ⟩) → ⟨ a ∈ˢ sucV b ⟩
This is the first use of the classical comparison. Everything done after the trichotomy result is returned is constructive; the second successor comparison below uses the same principle once more.
⊆→∈suc a b orda ordb a⊆b = Sum.rec (∈-case a b) (Sum.rec (≡-case a b) (wit-case a b a⊆b)) (ord-tri a orda b ordb)
Now suppose β ∈ α. Trichotomy compares sucV β with α, so either the successor still lies inside α, it equals α, or α lies inside sucV β. The type Out β α records the first two alternatives; the third will contradict β ∈ α.
The impossible case is discharged inside overshoot, whose premises are exactly the two facts that cannot hold at once: α belongs to sucV β while β belongs to the ordinal α. Unfolding a member of sucV β with ∈sucV-elim gives two subcases: α ∈ β, or α = β. The elimination principle demands that the target be a proposition, and the empty type ⊥* is one, so both branches may end in a contradiction.
private Out : S → S → Type (ℓ-suc ℓ) Out β α = ⟨ sucV β ∈ˢ α ⟩ ⊎ (sucV β ≡ α) overshoot : (β α : S) → IsOrd α → ⟨ β ∈ˢ α ⟩ → ⟨ α ∈ˢ sucV β ⟩ → Out β α overshoot β α ordα β∈α α∈sβ = Empty.rec*
In the first subcase we have the membership chain α ∈ β ∈ α. Transitivity of α, its first component ordα .fst, composes the chain to α ∈ α. In the second, α = β transports β ∈ α along the reversed path and again yields α ∈ α. Both contradict ∈-irrefl, so the impossible third alternative entails the required conclusion Out β α.
(∈sucV-elim {A = β} {x = α} {P = Empty.⊥* {ℓ-suc ℓ}} Empty.isProp⊥* α∈sβ (λ α∈β → lift (∈-irrefl α (ordα .fst α∈β β∈α))) (λ α≡β → lift (∈-irrefl α (subst (λ w → ⟨ w ∈ˢ α ⟩) (sym α≡β) β∈α)))) suc∈or≡ : (β α : S) → IsOrd β → IsOrd α → ⟨ β ∈ˢ α ⟩ → ⟨ sucV β ∈ˢ α ⟩ ⊎ (sucV β ≡ α)
The lemma proper now runs the trichotomy between sucV β and α, both certified ordinals, sucV β via suc-ord. The first two cases already have the required shape, membership or equality, and are returned directly.
suc∈or≡ β α ordβ ordα β∈α = go (ord-tri (sucV β) (suc-ord ordβ) α ordα) where go : (⟨ sucV β ∈ˢ α ⟩ ⊎ ((sucV β ≡ α) ⊎ ⟨ α ∈ˢ sucV β ⟩)) → Out β α go (inl s∈α) = inl s∈α go (inr (inl s≡α)) = inr s≡α
The third case, α ∈ sucV β, is precisely the premise of overshoot, and feeding it the standing hypothesis β ∈ α closes the analysis. The conclusion suc∈or≡ is the sharp form of "no overshoot": below α, the successor stages of members of α are never strictly beyond α.
go (inr (inr α∈sβ)) = overshoot β α ordα β∈α α∈sβ
And the cumulation lemma it is used for: an ordinal that has appeared at its own successor stage has appeared at every later stage, where later means the index is above it.
This is the bridge between the pointwise statement "β appears at sucV β" and the stage-level statement "every member of α is in Lset α". Given β ∈ α, the successor sucV β sits inside α or coincides with it, and either way membership in the smaller stage transports into membership in Lset α.
The membership branch uses monotonicity of stages: Lset-mono says that if γ ∈ δ then Lset γ is included in Lset δ, so a member of the earlier stage is a member of the later one. Here γ = sucV β and δ = α, exactly the first case of suc∈or≡.
private cumul-∈ : (β α : S) → ⟨ sucV β ∈ˢ α ⟩ → ⟨ β ∈ˢ Lset (sucV β) ⟩ → ⟨ β ∈ˢ Lset α ⟩ cumul-∈ β α s∈α = Lset-mono {α = α} {β = sucV β} s∈α {x = β} cumul-≡ : (β α : S) → sucV β ≡ α → ⟨ β ∈ˢ Lset (sucV β) ⟩ → ⟨ β ∈ˢ Lset α ⟩
The equality branch is the degenerate one: when sucV β is not strictly below but equal to α, membership in Lset (sucV β) is already membership in Lset α, and the transport along the path makes this literally so. The statement of Lset-cumul takes the two ordinal certificates and the appearance hypothesis, and dispatches on suc∈or≡.
cumul-≡ β α s≡α = subst (λ w → ⟨ β ∈ˢ Lset w ⟩) s≡α Lset-cumul : (β α : S) → IsOrd β → IsOrd α → ⟨ β ∈ˢ α ⟩ → ⟨ β ∈ˢ Lset (sucV β) ⟩ → ⟨ β ∈ˢ Lset α ⟩ Lset-cumul β α ordβ ordα β∈α β∈Lsβ = Sum.rec (λ s∈α → cumul-∈ β α s∈α β∈Lsβ)
Note the shape of the result: it does not say that β ∈ Lset α for all β ∈ α outright, since that appearance at the successor stage is still a hypothesis. The final theorem will supply that hypothesis by induction, and this lemma is exactly the step that turns it into stage content.
(λ s≡α → cumul-≡ β α s≡α β∈Lsβ) (suc∈or≡ β α ordβ ordα β∈α)
Nothing appears before its rank
If a set belongs to Lset α, its rank is bounded by α. Applied to an ordinal, whose rank agrees with itself, this shows that the ordinal cannot occur at an earlier stage.
The harder half. By induction on the stage index: a set in Lset α lies in the definable subsets of Lset β for some β in α, so it is a subset of Lset β; each of its members therefore has rank in β by the inductive hypothesis; so its own rank, which is the union of the successors of those ranks, is included in β; comparison puts it inside the successor of β, and that is inside α.
One notational point about the induction: membership in a truncated existential is itself truncated, and the induction is stated over the truncated form β ∈ᵗ α rather than over explicit members. The goal, a membership statement, is a proposition, so eliminating that truncation with PT.rec is legitimate.
The statement quantifies over all ordinals α at once, and ∈-induction is applied to the whole predicate as a function of α, with the ordinal certificate carried along as an argument. The induction is on membership in α, so the inductive hypothesis at α speaks about members β of α, not about earlier stages by any list order.
rank-Lset : (α : S) → IsOrd α → (x : S) → ⟨ x ∈ˢ Lset α ⟩ → ⟨ rank x ∈ˢ α ⟩ rank-Lset = ∈-induction {P = λ α → IsOrd α → (x : S) → ⟨ x ∈ˢ Lset α ⟩ → ⟨ rank x ∈ˢ α ⟩} step where step : (α : S)
The key step exposes what x ∈ Lset α means: by Lset-out, x merely belongs to a definable-subset layer over some β ∈ α. The layer membership is again truncated, but the conclusion rank x ∈ α is a proposition, so PT.rec may eliminate the truncation and work with the fiber β, β∈α, x∈𝒟ₒLβ as if it were given.
→ (∀ β → β ∈ᵗ α → IsOrd β → (x : S) → ⟨ x ∈ˢ Lset β ⟩ → ⟨ rank x ∈ˢ β ⟩) → IsOrd α → (x : S) → ⟨ x ∈ˢ Lset α ⟩ → ⟨ rank x ∈ˢ α ⟩ step α IH ordα x x∈Lα = PT.rec (snd (rank x ∈ˢ α)) fromStage (Lset-out α x x∈Lα) where fromStage : Σ[ β ∈ S ] (⟨ β ∈ˢ α ⟩ × ⟨ x ∈ˢ 𝒟ₒ (Lset β) ⟩) → ⟨ rank x ∈ˢ α ⟩
Inside the fiber, everything needed to run the induction hypothesis is recovered. The member β of the ordinal α is itself an ordinal by mem-ord, which is what lets the inductive hypothesis fire at β.
fromStage (β , β∈α , x∈𝒟ₒLβ) = rankx∈α where ordβ : IsOrd β ordβ = mem-ord {A = α} ordα β β∈α x⊆Lβ : (y : S) → ⟨ y ∈ˢ x ⟩ → ⟨ y ∈ˢ Lset β ⟩
Definability of x over Lset β means x is a subset of it: 𝒟ₒ-inv unpacks the certificate and DefOf.Def∋⊆A turns it into the inclusion x ⊆ Lset β. Composing with the inductive hypothesis, every member y of x has rank in β. Then rank-upper, given exactly such bounds on member ranks, includes rank x itself into β.
x⊆Lβ = DefOf.Def∋⊆A (Lset β) x (𝒟ₒ-inv (Lset β) x x∈𝒟ₒLβ) ry∈β : (y : S) → ⟨ y ∈ˢ x ⟩ → ⟨ rank y ∈ˢ β ⟩ ry∈β y y∈x = IH β β∈α ordβ y (x⊆Lβ y y∈x) rankx⊆β : (z : S) → ⟨ z ∈ˢ rank x ⟩ → ⟨ z ∈ˢ β ⟩ rankx⊆β = rank-upper x β ordβ ry∈β
What remains is to lift rank x ∈ sucV β into rank x ∈ α. Both rank x and β are ordinals, the former by rank-ord, and ⊆→∈suc from the first section applies to their inclusion, placing rank x in the successor of β. The elimination ∈sucV-elim then compares with the known β ∈ α: if rank x is a member of β, transitivity of α lifts the membership one step; if rank x equals β, the path transports β ∈ α directly. Either way the rank lands in α, completing the induction.
rankx∈α : ⟨ rank x ∈ˢ α ⟩
rankx∈α = ∈sucV-elim {A = β} {x = rank x} (snd (rank x ∈ˢ α))
(⊆→∈suc (rank x) β (rank-ord x) ordβ rankx⊆β)
(λ rx∈β → ordα .fst rx∈β β∈α)
(λ rx≡β → subst (λ w → ⟨ w ∈ˢ α ⟩) (sym rx≡β) β∈α)
For an ordinal the conclusion simplifies, because rank fixes it: an ordinal in Lset α is a member of α. This is the lower bound of the chapter's characterization in its usable form.
The step is a transport: rank-fix x ordx gives the path rank x ≡ x, and substituting along it converts the rank bound rank x ∈ α into the membership x ∈ α. Note the direction, which the induction above guarantees: appearance in a stage forces membership in the index, not the converse.
ord∈Lset→∈ : (α : S) → IsOrd α → (x : S) → IsOrd x → ⟨ x ∈ˢ Lset α ⟩ → ⟨ x ∈ˢ α ⟩ ord∈Lset→∈ α ordα x ordx x∈Lα = subst (λ w → ⟨ w ∈ˢ α ⟩) (rank-fix x ordx) (rank-Lset α ordα x x∈Lα)
Being an ordinal, said with bounded quantifiers
Being a transitive set all of whose members are transitive can be expressed with bounded quantifiers. The formula therefore recognizes ordinals absolutely between a transitive stage and the ambient universe.
The predicate is two clauses, and both are already bounded: a set is transitive when every member of every member of it is a member of it, and its members are transitive when the same holds one level down. No unbounded quantifier appears, so the formula is Δ₀, and no constant appears either, which spares the whole relabelling apparatus.
The indices are de Bruijn: each bounded quantifier binds a fresh variable 0 and pushes the earlier ones outward, so after two binders the candidate ordinal is at index 2.
The first clause says transitivity. Its bounded quantifier ∀̇∈ ranges over members of the value bound one step out; reading the de Bruijn indices, after one binder the members live at index 0 and the candidate at index 1, and inside the second binder the atomic formula demands y ∈ x with y at 0 and x pushed to 2. The formula is polymorphic in the alphabet K of constants but uses none, so the same syntax serves every interpretation.
φ-ord : ∀ {ℓk} {K : Type ℓk} → Formula K 1 φ-ord = (∀̇∈ (var zero) (∀̇∈ (var zero) (var zero ∈̇ var (suc (suc zero))))) ∧̇ (∀̇∈ (var zero)
The second clause stacks one more quantifier: a member x of the candidate, a member y of x, and a member z of y must land back in the candidate, which says each member of the candidate is transitive. Three binders later, the innermost variable is at 0 and the candidate at 3. The certificate φ-ord-Δ₀ is built from the same three primitive certificates, δ-∈ for atomic membership, δ-∀∈ for bounded quantifiers, and δ-∧ for the conjunction, mirroring the formula's construction step by step.
(∀̇∈ (var zero) (∀̇∈ (var zero) (var zero ∈̇ var (suc (suc zero)))))) φ-ord-Δ₀ : ∀ {ℓk} {K : Type ℓk} → Δ₀ (φ-ord {K = K}) φ-ord-Δ₀ = δ-∧ (δ-∀∈ (δ-∀∈ δ-∈)) (δ-∀∈ (δ-∀∈ (δ-∀∈ δ-∈)))
The ordinals of a stage
Separation by the bounded ordinal formula collects exactly the ordinals belonging to a stage. Its membership specification is available both internally and in the ambient universe.
Fix a stage. Using bounded absoluteness for the transitive stage, satisfaction of the formula in the ambient hierarchy unfolds to exactly the two clauses of the ordinal predicate, so the two are interchangeable by reshuffling arguments. Then the definable subset it carves is α itself: a member of it is an ordinal of the stage, hence a member of α by the rank half; and a member of α is an ordinal that has already appeared, by cumulation, so it satisfies the formula.
Cumulation needs, for each member of α, that it appears at its own successor stage. That is the theorem itself, so it enters here as a hypothesis, and the induction below is what supplies it.
Fix the ordinal α with its certificate. The stage A = Lset α is a layer, and layer-trans upgrades that to transitivity of A as a set, the only hypothesis under which the Δ₀ formula will be absolute between A's internal satisfaction and the ambient universe. The definability machinery of the chapter on L.Definability is opened relative to A, so defSet φ below always means the subset φ defines out of A.
module OrdAt (α : S) (ordα : IsOrd α) where private A = Lset α Atrans = layer-trans (Lset-layer α) module DefA = DefOf A
Members of A present themselves through the fiber ⟪ A ⟫: an index m names the element ⟪ A ⟫↪ m of A. The formula φ is our φ-ord instantiated at the carrier ⟪ A ⟫, so it has one free-variable slot, occupied by the environment ⟪ A ⟫↪ m ∷ []. Because φ has no constants, mapFo DefA.ι φ merely relabels through the constant interpretation ι, which for this formula changes nothing syntactically. The satisfaction sign ⊨ᵛ here is the ambient one, from the absoluteness refinement.
module RefA = DefA.Refine Atrans open RefA.Abs using ( _⊨ᵛ_ ) φ : Formula ⟪ A ⟫ 1 φ = φ-ord {K = ⟪ A ⟫} ⊨ᵛ→ord : (m : ⟪ A ⟫) → ⟨ (⟪ A ⟫↪ m ∷ []) ⊨ᵛ (mapFo DefA.ι φ) ⟩
The first direction reads satisfaction into the ordinal predicate. The satisfaction of a conjunction is a pair, and its first component is exactly the first bounded clause applied to x = B, the presented element: every y ∈ x with x ∈ B lands back in B. That is the transitivity condition for B, so the pair's first projection is a certificate that B is transitive.
→ IsOrd (⟪ A ⟫↪ m) ⊨ᵛ→ord m sat = transB , memTransB where B = ⟪ A ⟫↪ m transB : isTransV B
The second component is the second clause, with the quantifiers nested one deeper: for x ∈ B, y ∈ x and z ∈ y, the element z lands in B. That says precisely that every member x of B is itself transitive, so together with the first projection the satisfaction data is exactly an IsOrd certificate for B.
transB {x} {y} y∈x x∈B = sat .fst x x∈B y y∈x memTransB : (x : S) → ⟨ x ∈ˢ B ⟩ → isTransV x memTransB x x∈B {y} {z} z∈y y∈x = sat .snd x x∈B y y∈x z z∈y ord→⊨ᵛ : (m : ⟪ A ⟫) → IsOrd (⟪ A ⟫↪ m) → ⟨ (⟪ A ⟫↪ m ∷ []) ⊨ᵛ (mapFo DefA.ι φ) ⟩
The converse direction assembles a satisfaction from an ordinal certificate. Its first component must accept x ∈ B and y ∈ x and return y ∈ B, and transitivity of B, the first component of the IsOrd pair, does exactly that with the arguments in the right order.
ord→⊨ᵛ m ord = c1 , c2 where B = ⟪ A ⟫↪ m c1 : (x : S) → ⟨ x ∈ˢ B ⟩ → (y : S) → ⟨ y ∈ˢ x ⟩ → ⟨ y ∈ˢ B ⟩ c1 x x∈B y y∈x = ord .fst y∈x x∈B
The second component must chain three memberships back into B, and the second clause of the IsOrd pair is exactly that chain. So satisfaction of φ and the ordinal predicate are interchangeable in both directions; the two formulations express the same mathematical condition. With this equivalence established, the main statement takes shape: the definable subset selected by φ equals α, proved by extensionality from two inclusions, and stated under the explicit hypothesis α⊆A that every member of α has already appeared in A.
c2 : (x : S) → ⟨ x ∈ˢ B ⟩ → (y : S) → ⟨ y ∈ˢ x ⟩ → (z : S) → ⟨ z ∈ˢ y ⟩ → ⟨ z ∈ˢ x ⟩ c2 x x∈B y y∈x z z∈y = ord .snd x x∈B z∈y y∈x defSet-φ-ord : ((β : S) → ⟨ β ∈ˢ α ⟩ → ⟨ β ∈ˢ A ⟩) → DefA.defSet φ ≡ α defSet-φ-ord α⊆A = extensionality (DefA.defSet φ) α (sub₁ , sub₂)
The inclusion from the definable subset to α is where the rank half of the chapter earns its keep. Membership in a definable subset unfolds by ∈∈ₛ into a presentation-level fact, so sub₁ takes y with a proof that y belongs to defSet φ and must produce y ∈ α.
where sub₁ : ⟨ DefA.defSet φ ⊆ α ⟩ sub₁ y y∈ₛ = ∈∈ₛ {a = y} {b = α} .fst (y∈α (∈∈ₛ {a = y} {b = DefA.defSet φ} .snd y∈ₛ)) where
Three conversions stack here. Membership of y in the definable subset yields membership in A by defSet⊆A, since the subset is contained in the stage. The chosen presentation turns this membership proof, via ∈-asFiber, into an index m and a path q identifying y with the element named by m.
y∈α : ⟨ y ∈ˢ DefA.defSet φ ⟩ → ⟨ y ∈ˢ α ⟩ y∈α y∈def = ord∈Lset→∈ α ordα y ordy y∈A where y∈A = DefA.defSet⊆A φ y y∈def fib = ∈-asFiber {a = y} {b = A} y∈A
The path q transports membership from y to the presented element ⟪ A ⟫↪ m. Because φ is Δ₀ and A is transitive, abs-defSet identifies the hProp of membership in defSet φ with the hProp of ambient satisfaction of mapFo ι φ at the one-element environment. Substitution along these paths yields the required inhabitant sat; path transport itself imposes no propositionality condition.
m = fib .fst q = fib .snd sat : ⟨ (⟪ A ⟫↪ m ∷ []) ⊨ᵛ (mapFo DefA.ι φ) ⟩ sat = subst ⟨_⟩ (RefA.abs-defSet φ φ-ord-Δ₀ m) (subst (λ w → ⟨ w ∈ˢ DefA.defSet φ ⟩) (sym q) y∈def)
From sat, the implication ⊨ᵛ→ord returns an IsOrd certificate for the presented element, and transporting along q turns it into one for y itself. Then ord∈Lset→∈, the rank half, places y inside α. So an arbitrary member of the definable subset is an ordinal of the stage, and the stage index contains it.
ordy : IsOrd y ordy = subst IsOrd q (⊨ᵛ→ord m sat) sub₂ : ⟨ α ⊆ DefA.defSet φ ⟩ sub₂ y y∈ₛ = ∈∈ₛ {a = y} {b = DefA.defSet φ} .fst (y∈def (∈∈ₛ {a = y} {b = α} .snd y∈ₛ))
The reverse inclusion runs the same circuit backward. A member y of α arrives with its ordinal certificate already in hand, from mem-ord. The hypothesis α⊆A presents y inside the stage via a fiber m, q, and ord→⊨ᵛ gives ambient satisfaction of φ at that environment.
where y∈def : ⟨ y ∈ˢ α ⟩ → ⟨ y ∈ˢ DefA.defSet φ ⟩ y∈def y∈α = subst (λ w → ⟨ w ∈ˢ DefA.defSet φ ⟩) q (subst ⟨_⟩ (sym (RefA.abs-defSet φ φ-ord-Δ₀ m)) sat) where
Absoluteness now converts in the other direction: ambient satisfaction of the Δ₀ formula is membership of ⟪ A ⟫↪ m in defSet φ, and transporting along q lands the membership on y itself, inside the definable subset. No choice is made anywhere: each fiber m, q is used locally, on the very y that produced it.
ordy = mem-ord {A = α} ordα y y∈α y∈A = α⊆A y y∈α fib = ∈-asFiber {a = y} {b = A} y∈A m = fib .fst q = fib .snd
The two inclusions close, and defSet-φ-ord states the conclusion: the subset the bounded formula carves out of Lset α is exactly α. Everything so far is conditional on α⊆A; the next section removes the condition, and with it the chapter's main theorem falls into place.
sat : ⟨ (⟪ A ⟫↪ m ∷ []) ⊨ᵛ (mapFo DefA.ι φ) ⟩ sat = ord→⊨ᵛ m (subst IsOrd (sym q) ordy)
An ordinal appears at its successor
Every ordinal is a definable subset of itself, selected by the bounded ordinal formula. Hence α belongs to the definable power set of Lset α, which is the successor stage.
The remaining gap is the inclusion α ⊆ Lset α, which the previous section had to assume. It is filled by induction on membership: the induction hypothesis states the theorem for each member β of α, so β appears in Lset (sucV β), and cumulation from the first section raises it into Lset α. Once every member has accumulated, α is carved out of Lset α by the formula, and one branch of the union in the definition of the next stage contains it. The circularity is only apparent, because the induction hypothesis concerns the members, not α itself.
Two small facts are packaged before the induction. The first is a one-way bridge from definable power set to stage: a certificate that α lies in 𝒟ₒ (Lset α), meaning α is a definable subset of Lset α, is exactly the data Lset-in needs, once combined with self∈sucV α, which says α belongs to its own successor. The second line begins the theorem itself, and the induction principle for membership is applied directly: the statement being proved by induction is the theorem, relativized to each ordinal.
private 𝒟ₒ→Lset-suc : (α : S) → ⟨ α ∈ˢ 𝒟ₒ (Lset α) ⟩ → ⟨ α ∈ˢ Lset (sucV α) ⟩ 𝒟ₒ→Lset-suc α α∈𝒟ₒ = Lset-in (sucV α) α α (self∈sucV α) α∈𝒟ₒ ord∈Lset-suc : (α : S) → IsOrd α → ⟨ α ∈ˢ Lset (sucV α) ⟩ ord∈Lset-suc = ∈-induction
The induction step receives, for every member β of α, the theorem's conclusion at β, and must produce it at α. Since the previous section already reduced the goal to the single hypothesis α ⊆ Lset α, all the step does is assemble that inclusion and hand the result to the bridge lemma. Nothing about α beyond its ordinalhood and the induction hypothesis is used.
{P = λ α → IsOrd α → ⟨ α ∈ˢ Lset (sucV α) ⟩} step where step : (α : S) → (∀ β → β ∈ᵗ α → IsOrd β → ⟨ β ∈ˢ Lset (sucV β) ⟩) → IsOrd α → ⟨ α ∈ˢ Lset (sucV α) ⟩ step α IH ordα = 𝒟ₒ→Lset-suc α α∈𝒟ₒ
The inclusion is built member-by-member. For each β in α, being a member of the ordinal α makes β an ordinal in its own right, and the induction hypothesis places it in Lset (sucV β); the cumulation lemma of the first section, whose second comparison was designed for exactly this shape, then lifts it to Lset α. This is where the earlier comparison lemmas pay off: a single case split on whether sucV β lies in α or equals it covers every member at once.
where α⊆A : (β : S) → ⟨ β ∈ˢ α ⟩ → ⟨ β ∈ˢ Lset α ⟩ α⊆A β β∈α = Lset-cumul β α ordβ ordα β∈α (IH β β∈α ordβ) where ordβ = mem-ord {A = α} ordα β β∈α
With α ⊆ Lset α in hand, the previous section's conclusion applies verbatim: the definable subset of Lset α selected by φ-ord is α itself. The certificate is supplied merely, by truncation, since a member of 𝒟ₒ needs only some defining formula and proof of agreement, and the pair of φ-ord with the extensionality argument from OrdAt is exactly such a witness. The bridge lemma then moves α into Lset (sucV α), completing the induction and the theorem.
α∈𝒟ₒ : ⟨ α ∈ˢ 𝒟ₒ (Lset α) ⟩ α∈𝒟ₒ = 𝒟ₒ-intro (Lset α) α ∣ φ-ord {K = ⟪ Lset α ⟫} , OrdAt.defSet-φ-ord α ordα α⊆A ∣₁
Recap
Ordinals now have exact stage bounds: α appears in Lset (sucV α), and appearance in Lset β forces α ∈ β. The bounded ordinal formula makes these facts available to later internal arguments.
ord∈Lset-suc says an ordinal appears at the stage after itself, and ord∈Lset→∈ says it appears no earlier. Together the ordinals of Lset α are exactly the members of α. The chapter is classical, through the two comparisons of its first section, and everything else it uses was constructive. The module L.Stage applies this result to ω, completing the proof of the axiom of infinity.