在可构造层级中定位序数

本章在一个固定的宇宙层级 ℓ 内工作，以下关于集合、成员关系与 L 的层的全部论述都在这一层级上。我们假设层级 ℓ-suc ℓ 上的排中律。它在数学上的唯一用途是序数三歧：对两个序数，返回两个方向的成员关系之一或相等这一情形。后文的所有结论都经下一节建立的两次比较引理继承这种经典性。

module L.Ordinal.Stages {ℓ : Level} (lem : LEM (ℓ-suc ℓ)) where

序数在可构造层级中的位置由成员关系控制：它会在自身的后继层出现，却不会早于自身的秩出现。本章证明两个方向，并给出在层内部识别序数的有界公式。

关于塔还有一个问题悬而未决，而无穷公理正系于此：给定一层，到那时为止究竟出现了哪些序数？答案十分简洁。Lset α 中的序数恰是 α 的元素，故塔的索引与它的序数内容逐层一致，而序数首次现身于自身之后的那一层。

两个方向都有实质难度。一个方向说序数不会提前现身：若它在 Lset α 中，则它是 α 的元素。这是较难的一半，要经过秩，而这正是这里需要秩构造的原因。Lset α 中的集合是某个更早层的可定义子集，依归纳其元素的秩低于那一层，故它自身的秩有界；而作为序数，它就是自身的秩。

另一个方向说明序数不会延迟出现：α 的每个元素都已经在 Lset α 中。这一半由直接归纳证明，所用陈述正是序数会在自身之后的层出现。这里没有循环：归纳假设为各个元素提供该陈述，而证明所需的也只有这些元素。

两半齐备，一层中的序数便由单一公式「是序数」从中选出，该公式是 Δ₀ 的，因为传递性只用有界量词就能表述。于是 α 是 Lset α 的可定义子集，后继层的可定义幂集子句随即可以应用。

这里交汇了两类词汇。来自环境层级 V 的是基本动作：集合 S 上的成员关系 ∈ˢ、冯·诺伊曼后继 sucV、沿成员关系的归纳法与成员关系的非自反性。来自可构造一侧的是层 Lset α 本身、可定义子集层 𝒟ₒ，以及把某层中的成员关系与它的可定义幂集中的成员关系联系起来的两个方向 Lset-in 与 Lset-out。本章的陈述完全落在这个交集里：它问的是序数在各个 Lset α 之间的位置。

序数以谓词 IsOrd 进入：一个集合是序数，当且仅当它是传递的且它的每个元素都是传递的。这是冯·诺伊曼式的读法，其中序数 α 就是所有更小序数的集合，因此问序数是否已在某层出现，字面上就是成员关系问题。相应的闭包事实是 mem-ord 与 suc-ord：序数的元素是序数，序数的后继是序数。它们保证论证中的每层指标都是序数。

一切背后的判定程序是 ord-tri：给定两个各自被证明为序数的序数，它回答三种情形中的哪一种成立，即 a ∈ b、a = b 或 b ∈ a。它使用上述排中律假设。三歧比较以和类型返回三个情形，不可能的分支落入空类型。另一方面，命题截断 ∣_∣₁ 记录层分解所需的较早层仅仅存在。

秩构造提供如下三条性质。对集合 x，rank x 是一个序数，刻画 x 在累积层级中所处的深度；rank-ord 证明它是序数，rank-fix 把序数的秩等同于该序数本身，rank-upper 由各元素秩的上界给出该集合秩的上界。这三条正是较难方向所需的事实。

open import Cubical.HITs.CumulativeHierarchy.Properties
  using ( ∈∈ₛ; ∈-asFiber; ⟪_⟫; ⟪_⟫↪; extensionality; _⊆_ )
open import Cubical.HITs.CumulativeHierarchy.Constructions

为了把外围成员关系与层上的公式联系起来，集合 A 有一个选定的呈现 ⟪ A ⟫，∈-asFiber 把 A 中的元素转为指名该元素的指标。互相包含则通过 extensionality 给出集合相等。公式的满足解释直接在 hProp 中：每个公式表示一个 hProp。这些对应使论证可以在集合、其指标与有界公式之间转换。

  using ( module InfinitySet )
open InfinitySet using ( sucV )

open hPropView 𝒮ᵥ

两次比较

三歧比较只留下三个数学情形。若 a ∈ b，则 a 也属于 b 的后继；若 a = b，则 a 作为新增的顶端元素属于该后继。余下的 b ∈ a 将由包含关系 a ⊆ b 排除。

设集合 a 与 b 满足 a ⊆ b，用三歧性比较二者。若 a 是 b 的元素，第一个辅助件调用 ∈sucV-inl：b 的元素自动是 sucV b 的元素，因为后继是 b 连同它的单点集。若 a 等于 b，第二个辅助件沿路径 a ≡ b 传递事实 self∈sucV b，即 b 属于自身的后继。三种情形中两种已经关闭。

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)

余下情形是 b ∈ a，而包含关系将它排除：由 b ∈ a 与 a ⊆ b 可得 b ∈ b，这与 ∈-irrefl 矛盾。由此矛盾可推出目标 a ∈ sucV b。因此，对序数 a 与 b，包含 a ⊆ b 强制 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 = ⊥₀-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 ⟩

这是第一次使用经典的序数比较。三歧结果返回之后的推理都是构造性的；下面关于后继的第二个比较会再使用同一原理。

⊆→∈suc a b orda ordb a⊆b = ⊎-rec
  (∈-case a b)
  (⊎-rec (≡-case a b) (wit-case a b a⊆b))
  (ord-tri a orda b ordb)

现在设 β ∈ α。用三歧性比较 sucV β 与 α，结果要么后继仍位于 α 内，要么它等于 α，要么 α 位于 sucV β 内。类型 Out β α 记录前两种可能；第三种将与 β ∈ α 矛盾。

不可能的情形在 overshoot 内部排除，它的前提恰是两个不能同时成立的事实：α 属于 sucV β，而 β 属于序数 α。用 ∈sucV-elim 展开 sucV β 中元素的事实，得到两个子情形：α ∈ β，或 α = β。该消去原则要求目标是命题，而空类型 ⊥* 正是命题，于是两个分支都可以终止于矛盾。

private
  Out : S → S → Type (ℓ-suc ℓ)
  Out β α = ⟨ sucV β ∈ˢ α ⟩ ⊎ (sucV β ≡ α)

  overshoot : (β α : S) → IsOrd α → ⟨ β ∈ˢ α ⟩ → ⟨ α ∈ˢ sucV β ⟩ → Out β α
  overshoot β α ordα β∈α α∈sβ = ⊥*-rec

第一个子情形给出成员关系链 α ∈ β ∈ α。α 的传递性，即其第一分量 ordα .fst，将这条链复合为 α ∈ α。第二个子情形中，α = β 沿反向路径传递 β ∈ α，同样得到 α ∈ α。两者都与 ∈-irrefl 矛盾，因此这个不可能的第三种情形推出所需结论 Out β α。

    (∈sucV-elim {A = β} {x = α} {P = ⊥* {ℓ-suc ℓ}} isProp⊥* α∈sβ
      (λ α∈β → lift (∈-irrefl α (ordα .fst α∈β β∈α)))
      (λ α≡β → lift (∈-irrefl α (subst (λ w → ⟨ w ∈ˢ α ⟩) (sym α≡β) β∈α))))

suc∈or≡ : (β α : S) → IsOrd β → IsOrd α → ⟨ β ∈ˢ α ⟩
        → ⟨ sucV β ∈ˢ α ⟩ ⊎ (sucV β ≡ α)

引理本身接着在 sucV β 与 α 之间运行三歧性，二者都被证明为序数，sucV β 经 suc-ord。前两种情形已经具有所需形状，成员关系或相等，直接返回即可。

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≡α

第三种情形 α ∈ sucV β 恰是 overshoot 的前提，代入已有假设 β ∈ α 即完成分析。结论 suc∈or≡ 是「不越头」的锐利形式：在 α 之下，α 各元素的后继层从不停留在严格超出 α 的位置。

  go (inr (inr α∈sβ)) = overshoot β α ordα β∈α α∈sβ

而它所服务的累积引理则是：在自身后继层现身过的序数，在此后每层都已现身，其中「此后」指索引在其之上。

这是「β 在 sucV β 现身」这一逐点陈述与「α 的每个元素都在 Lset α 中」这一层陈述之间的桥。给定 β ∈ α，后继 sucV β 或位于 α 内部、或与之重合，无论哪种情形，较小层中的成员关系都会转化为 Lset α 中的成员关系。

成员关系分支使用层的单调性：Lset-mono 说若 γ ∈ δ 则 Lset γ 包含于 Lset δ，于是较早层的元素是较晚层的元素。此处 γ = sucV β、δ = α，恰是 suc∈or≡ 的第一种情形。

private
  cumul-∈ : (β α : S) → ⟨ sucV β ∈ˢ α ⟩ → ⟨ β ∈ˢ Lset (sucV β) ⟩
          → ⟨ β ∈ˢ Lset α ⟩
  cumul-∈ β α s∈α = Lset-mono {α = α} {β = sucV β} s∈α {x = β}

  cumul-≡ : (β α : S) → sucV β ≡ α → ⟨ β ∈ˢ Lset (sucV β) ⟩ → ⟨ β ∈ˢ Lset α ⟩

相等分支是退化情形：当 sucV β 不严格在下而是等于 α 时，Lset (sucV β) 中的成员关系已经是 Lset α 中的成员关系，沿该路径的传递把这一点变成字面事实。Lset-cumul 的陈述取两个序数证书与现身假设，并按 suc∈or≡ 分派。

  cumul-≡ β α s≡α = subst (λ w → ⟨ β ∈ˢ Lset w ⟩) s≡α

Lset-cumul : (β α : S) → IsOrd β → IsOrd α → ⟨ β ∈ˢ α ⟩
           → ⟨ β ∈ˢ Lset (sucV β) ⟩ → ⟨ β ∈ˢ Lset α ⟩
Lset-cumul β α ordβ ordα β∈α β∈Lsβ =
  ⊎-rec (λ s∈α → cumul-∈ β α s∈α β∈Lsβ)

注意结果的形状：它并未直接断言对所有 β ∈ α 都有 β ∈ Lset α，因为在后继层的现身仍是假设。最后的定理将用归纳给出该假设，而这条引理恰是把假设转化为层内容的那一步。

          (λ s≡α → cumul-≡ β α s≡α β∈Lsβ)
          (suc∈or≡ β α ordβ ordα β∈α)

没有东西早于自身的秩现身

若一个集合属于 Lset α，其秩便以 α 为界。对于秩等于自身的序数，这说明它不能在更早层出现。

这是较难的一半。沿层索引归纳：Lset α 中的集合落在某个 β ∈ α 的 Lset β 的可定义子集里，故它是 Lset β 的子集；于是依归纳假设它的每个元素的秩都在 β 中；故它自身的秩，即那些秩的后继之并，包含于 β；三歧比较给出它属于 β 的后继，从而属于 α。

关于归纳的一点记法说明：截断存在式中的成员关系本身也是截断的，归纳按截断形式 β ∈ᵗ α 陈述，而非按显式元素。目标是一个成员关系陈述，因而是命题，所以用 rec₁ 消去该截断是合法的。

陈述同时对所有序数 α 量化，∈-induction 施加于作为 α 之函数的整个谓词，序数证书作为参数一路携带。归纳是沿 α 上的成员关系进行的，故在 α 处的归纳假设谈论的是 α 的元素 β，而不是按任何次序排列的「更早层」。

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)

关键一步揭示 x ∈ Lset α 的含义：由 Lset-out，x 仅仅 (merely) 属于某个 β ∈ α 之上的可定义子集层。层中的成员关系同样是截断的，但结论 rank x ∈ α 是命题，故 rec₁ 可以消去截断，并把纤维 β、β∈α、x∈𝒟ₒLβ 当作已经给出而加以使用。

       → (∀ β → β ∈ᵗ α → IsOrd β → (x : S) → ⟨ x ∈ˢ Lset β ⟩ → ⟨ rank x ∈ˢ β ⟩)
       → IsOrd α → (x : S) → ⟨ x ∈ˢ Lset α ⟩ → ⟨ rank x ∈ˢ α ⟩
  step α IH ordα x x∈Lα = rec₁ ((rank x ∈ˢ α) .snd) fromStage (Lset-out α x x∈Lα)
    where
    fromStage : Σ[ β ∶ S ] (⟨ β ∈ˢ α ⟩ × ⟨ x ∈ˢ 𝒟ₒ (Lset β) ⟩) → ⟨ rank x ∈ˢ α ⟩

在纤维内部，运行归纳假设所需的一切都被恢复。序数 α 的元素 β 经 mem-ord 本身就是序数，正是这一点让归纳假设得以在 β 处启用。

    fromStage (β , β∈α , x∈𝒟ₒLβ) = rankx∈α
      where
      ordβ : IsOrd β
      ordβ = mem-ord {A = α} ordα β β∈α
      x⊆Lβ : (y : S) → ⟨ y ∈ˢ x ⟩ → ⟨ y ∈ˢ Lset β ⟩

x 在 Lset β 上的可定义性意味着 x 是它的子集：𝒟ₒ-inv 拆开证书，DefOf.Def∋⊆A 把它变成包含关系 x ⊆ Lset β。与归纳假设结合，x 的每个元素 y 的秩都在 β 中。随后 rank-upper 在恰有这些元素秩上界的前提下，把 rank x 本身包含进 β。

      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∈β

剩下的是把 rank x ∈ sucV β 提升为 rank x ∈ α。rank x 与 β 都是序数，前者由 rank-ord 保证，于是第一节建立的 ⊆→∈suc 施于二者的包含关系，把 rank x 放进 β 的后继。随后 ∈sucV-elim 与已知的 β ∈ α 比较：若 rank x 是 β 的元素，α 的传递性把成员关系再推一步；若 rank x 等于 β，路径直接传递 β ∈ α。无论哪种情形，秩都落入 α，归纳完成。

      rankx∈α : ⟨ rank x ∈ˢ α ⟩
      rankx∈α = ∈sucV-elim {A = β} {x = rank x} ((rank x ∈ˢ α) .snd)
        (⊆→∈suc (rank x) β (rank-ord x) ordβ rankx⊆β)
        (λ rx∈β → ordα .fst rx∈β β∈α)
        (λ rx≡β → subst (λ w → ⟨ w ∈ˢ α ⟩) (sym rx≡β) β∈α)

对序数，结论更简单，因为秩完全确定它：Lset α 中的序数是 α 的元素。这就是本章刻画中以下界形式呈现的可用版本。

这一步是一次传递：rank-fix x ordx 给出路径 rank x ≡ x，沿它替换即把秩上界 rank x ∈ α 转化为成员关系 x ∈ α。注意方向，这正是上述归纳所保证的：在层中的现身强制对索引的成员关系，而非相反。

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α)

用有界量词表达序数性质

一个集合是传递的，且其每个元素也都是传递的，这一性质可以用有界量词表达。因此，该公式在传递层与外围宇宙之间绝对地识别序数。

这个谓词由两条子句构成，两条都已有界：集合传递，指其元素的元素也都是其元素；元素皆传递，指同一条性质在低一层成立。没有无界量词出现，故公式是 Δ₀；也没有常元出现，从而免去了一整套常元改名操作。

索引采用 de Bruijn：每个有界量词约束一个新的变元 0，并把先前已有的变元向外推移一位，故两层约束之后，候选序数位于索引 2。

第一条子句说的是传递性。其有界量词 ∀̇∈ 在外一层所约束值的元素上取遍；按 de Bruijn 索引来读，第一层约束后元素位于索引 0、候选序数位于索引 1，而第二层约束内的原子公式要求 y ∈ x，y 在 0，x 被推到 2。公式对常元字母表 K 多态但不使用任何常元，故同一语法可服务于任何解释。

φ-ord : ∀ {ℓk} {K : Type ℓk} → Formula K 
φ-ord =
  (∀̇∈ (var zero) (∀̇∈ (var zero) (var zero ∈̇ var (suc (suc zero)))))
  ∧̇
  (∀̇∈ (var zero)

第二条子句多叠一层量词：候选序数的元素 x、x 的元素 y、y 的元素 z 必须落回候选序数，这正说明候选序数的每个元素都是传递的。三层约束之后，最内层变元在索引 0，候选序数在索引 3。证书 φ-ord-Δ₀ 由同样的三种基本证书拼成，原子成员关系的 δ-∈、有界量词的 δ-∀∈ 与合取的 δ-∧，一步对一步地映照公式的构造。

    (∀̇∈ (var zero) (∀̇∈ (var zero) (var zero ∈̇ var (suc (suc zero))))))

φ-ord-Δ₀ : ∀ {ℓk} {K : Type ℓk} → Δ₀ (φ-ord {K = K})
φ-ord-Δ₀ = δ-∧ (δ-∀∈ (δ-∀∈ δ-∈)) (δ-∀∈ (δ-∀∈ (δ-∀∈ δ-∈)))

一层中的序数

用有界序数公式作分离，恰好收集属于某一层的全部序数。其成员关系规格在内部与外围宇宙中都可使用。

固定一层。利用传递层上的有界绝对性，公式在环境层级中的满足恰好展开成序数谓词的两条子句，故二者只需重排参数即可互换。于是它作分离所得的可定义子集就是 α 自身：其元素是该层的序数，故经秩那一半是 α 的元素；而 α 的元素是已经现身过的序数，经累积引理，它们满足该公式。

累积引理需要 α 的每个元素都在自身的后继层现身。这恰是本定理的结论本身，故在此把它作为假设引入，而下面的归纳正是给出这一假设的论证。

固定序数 α 及其证书。层 A = Lset α 是一层，layer-trans 把它升级为集合 A 的传递性，这是 Δ₀ 公式在 A 的内部满足与外围宇宙之间保持绝对的唯一前提。L.Definability 那章的可定义性机制相对于 A 打开，故下文的 defSet φ 总指 φ 从 A 中定出的子集。

module OrdAt (α : S) (ordα : IsOrd α) where

private
  A = Lset α
  Atrans = layer-trans (Lset-layer α)
  module DefA = DefOf A

  module RefA = DefA.Refine Atrans
  open RefA.Abs using ( _⊨ᵛ_ )

  φ : Formula ⟪ A ⟫ 
  φ = φ-ord {K = ⟪ A ⟫}

⊨ᵛ→ord : (m : ⟪ A ⟫) → ⟨ (⟪ A ⟫↪ m ∷ []) ⊨ᵛ (mapFo DefA.ι φ) ⟩

       → IsOrd (⟪ A ⟫↪ m)
⊨ᵛ→ord m sat = transB , memTransB
  where
  B = ⟪ A ⟫↪ m
  transB : isTransV 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.ι φ) ⟩

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

  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₂)

  where
  sub₁ : ⟨ DefA.defSet φ ⊆ α ⟩
  sub₁ y y∈ₛ = ∈∈ₛ {a = y} {b = α} .fst
    (y∈α (∈∈ₛ {a = y} {b = DefA.defSet φ} .snd y∈ₛ))
    where

    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

      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)

      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∈ₛ))

    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

      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

      sat : ⟨ (⟪ A ⟫↪ m ∷ []) ⊨ᵛ (mapFo DefA.ι φ) ⟩
      sat = ord→⊨ᵛ m (subst IsOrd (sym q) ordy)

序数现身于其后继

每个序数都是自身的可定义子集，由有界序数公式选出。因此 α 属于 Lset α 的可定义幂集，也就是后继层。

剩下的缺口正是上一节不得不假设的包含关系 α ⊆ Lset α。它由对成员关系的归纳填补：归纳假设陈述的是定理对 α 的每个元素 β 的情形，于是 β 出现在 Lset (sucV β) 中，再经第一节的累积引理被提升到 Lset α 中。一旦所有元素都累积进来，公式便从 Lset α 中分离出 α，而下一层定义中的并包含这一项。这里没有循环：归纳假设关心的是元素，而非 α 自身。

归纳之前先打包两个小事实。其一是从可定义幂集到层的单向桥：一个说明 α 属于 𝒟ₒ (Lset α) 的证书，即 α 是 Lset α 的可定义子集，与 self∈sucV α (它说 α 属于自身的后继) 合在一起，恰是 Lset-in 所需的全部数据。第二行开始定理本身，直接应用对成员关系的归纳原理：被归纳证明的陈述就是定理本身，相对化到每个序数上。

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

归纳步对 α 的每个元素 β 收到定理在 β 处的结论，并须给出在 α 处的结论。由于上一节已把目标化归为唯一的假设 α ⊆ Lset α，这一步要做的只是组装这个包含关系，并把结果交给桥引理。除了 α 是序数与归纳假设之外，别无所用。

  {P = λ α → IsOrd α → ⟨ α ∈ˢ Lset (sucV α) ⟩} step
  where
  step : (α : S) → (∀ β → β ∈ᵗ α → IsOrd β → ⟨ β ∈ˢ Lset (sucV β) ⟩)
       → IsOrd α → ⟨ α ∈ˢ Lset (sucV α) ⟩
  step α IH ordα = 𝒟ₒ→Lset-suc α α∈𝒟ₒ

包含关系逐个元素地组装。对 α 中的每个 β，作为序数 α 的元素使 β 自己也是序数，归纳假设把它放进 Lset (sucV β)；而第一节的累积引理，正是为其后继或落入 α、或与之相等这两种情形而设，随即把它提升到 Lset α。前面那两个比较引理在此兑现：一次分情形就同时覆盖了所有元素。

    where
    α⊆A : (β : S) → ⟨ β ∈ˢ α ⟩ → ⟨ β ∈ˢ Lset α ⟩
    α⊆A β β∈α = Lset-cumul β α ordβ ordα β∈α (IH β β∈α ordβ)
      where
      ordβ = mem-ord {A = α} ordα β β∈α

有了 α ⊆ Lset α，上一节的结论原样适用：由 φ-ord 从 Lset α 中选出的可定义子集正是 α 自身。证书以截断的方式仅仅给出，因为 𝒟ₒ 的元素只需要某个定义公式及一致性证明，而 φ-ord 与 OrdAt 中的外延性论证组成的对恰是这样的见证。桥引理随后把 α 移入 Lset (sucV α)，归纳与定理同时完成。

    α∈𝒟ₒ : ⟨ α ∈ˢ 𝒟ₒ (Lset α) ⟩
    α∈𝒟ₒ = 𝒟ₒ-intro (Lset α) α
      ∣ φ-ord {K = ⟪ Lset α ⟫} , OrdAt.defSet-φ-ord α ordα α⊆A ∣₁

小结

序数现在具有准确的层界：α 出现在 Lset (sucV α) 中，而若它出现在 Lset β 中，则必有 α ∈ β。有界序数公式使后续内部论证能够使用这些事实。

ord∈Lset-suc 说序数现身在自身之后的那一层中，ord∈Lset→∈ 说它不会更早现身。二者合起来，Lset α 中的序数恰是 α 的元素。经由第一节那两次比较，本章是经典的，而它用到的其余一切都是构造性的。模块 L.Stage 将这一结果应用于 ω，从而完成无穷公理的证明。