Von Neumann 秩

可以直接阅读本章，也可以通过阅读指南和依赖地图选择其他路线。

阅读指南 · 依赖地图

集合的秩是其所有成员之秩的后继的并；用记号说，计算定理 rank-compute 把 rank x 等同于 rankStep x (λ y _ → rank y)。本章证明秩的四条性质：rank-mono 说秩沿隶属关系严格增长，rank-ord 说秩总是序数，rank-upper 给出秩包含于某序数的有条件结论，rank-fix 说秩固定每个序数。

此处不需要任何外部的序数类型：秩取值于层级自身，而递归依据正则性所保证的成员关系良基性进行。因此本章每条定理都不需要排中律参数。

秩直接定义在累积层级 V ℓ 的载体 S 中。成员关系 x ∈ˢ y 是命题值的，而正则性保证这条成员关系良基。因此，成员归纳原理 ∈-induction 可以利用每个成员处已经定义的值，在当前集合处定义一个 S 中的值。

{-# OPTIONS --cubical --safe --guardedness #-}

open import Base.Prelude

module L.Rank {ℓ : Level} where

open import FOL.ZFStructure using ( module hPropStructure )

对秩而言，集合处的值要汇集其所有成员之秩的后继。sucV 与小索引并正好表达这一构造。递归得到的成员秩一旦是序数，suc-ord 与 setUnion-ord 就证明汇集后的值仍是序数；在处理序数自身时，mem-ord 再给出其成员的序数性。

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 )

这里的索引确实是小的。每个集合 x 都有小成员类型 ⟪ x ⟫ 及其到 S 的嵌入 ⟪ x ⟫↪，而 ∈ₛ⟪ x ⟫↪ m 证明所表示的集合属于 x。反过来，给定成员关系证明，∈-asFiber 返回一个索引以及所表示集合与该成员相等的路径。这两个方向把沿成员关系的递归与取并所需的小族连接起来。

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; ⟪_⟫; ⟪_⟫↪; ∈ₛ⟪_⟫↪_ )

于是递归步可以直接读成数学构造：取成员组成的小族，把每个成员换成其递归所得秩的后继，再对这一族取并。下一节把这个构造写成 rankStep，并给出它的计算路径。

open import Cubical.HITs.CumulativeHierarchy.Constructions
  using ( ⋃_; module InfinitySet )
open InfinitySet using ( sucV )

open hPropStructure 𝒮ᵥ

递归

步进取 x 的各成员之秩的后继的并。递归调用跑在成员的小类型上，而计算法则作为路径命题性地成立、而非定义性地成立，这正是后文证明所用的形式。

递归方程说：要对集合 x 求秩，就对每个成员求秩，再取其后继的并。形式上，被取并的族以成员的小类型 ⟪ x ⟫ 为索引，故 ⋃ (sett ⟪ x ⟫ …) 是一次合法的小并；嵌入 ⟪ x ⟫↪ 把索引 m 变成实际的集合 ⟪ x ⟫↪ m，而辅助 mem 提供该嵌入集合确实是 x 的成员的证明，这正是递归调用 rec 所要求的。注意步进函数的形状：它经函数 rec 接收递归值，而不直接调用 rank，这使它能充当 ∈-induction 的步进。

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)

秩本身就是把成员归纳用在这个步进上：∈-induction rankStep 把步进函数变成整个 S 上的全定义族。定义标记为 opaque，以免检查器展开其中的良基消去子。取而代之可用的是计算法则 rank-compute，它把递归方程作为命题路径暴露出来：rank x 有一条到 rankStep x (λ y _ → rank y) 的路径，即同一条方程、但每次递归调用都由 rank 自身填充。后续证明按这条路径改写，而不直接化简 rank。

opaque
  rank : S → S
  rank = ∈-induction rankStep

  rank-compute : (x : S) → rank x ≡ rankStep x (λ y _ → rank y)
  rank-compute = ∈-induction-compute rankStep

秩沿成员关系严格增长

定理 rank-mono 说：若 x ∈ˢ y，则 rank x ∈ˢ rank y。它直接来自定义之并的形状：rank y 是以 y 的成员 w 为索引的后继 sucV (rank w) 之并，故只需把 rank x 表为其中某个后继的成员。命题中完全不出现 IsOrd 假设。

给定 x ∈ˢ y，目标是 rank x ∈ˢ rank y。先用 rank-compute 把 rank y 展开一次：目标变成属于并 ⋃ (sett ⟪ y ⟫ (λ m → sucV (rank (⟪ y ⟫↪ m))))。于是只需把 rank x 表为某个族元、即某成员 w 的 sucV (rank w) 的成员；self∈sucV 把 rank x 放进它自身的后继，union-family-in 再把它提升进并，包括沿计算路径的传输。

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

剩下的部分是并的族元所用的索引从何而来。函数 ∈-asFiber 把给定的证明 x∈y 转换为嵌入 ⟪ y ⟫↪ 的一个纤维：一个对，其第一分量 fib .fst 是 ⟪ y ⟫ 中的一个索引，第二分量 fib .snd 是说被索引的集合等于 x 的路径。代码正是沿这条路径传输，使得后继中的隶属谈的是 rank x 自身。

  fib = ∈-asFiber {a = x} {b = y} x∈y

秩是序数

一次成员归纳。先用 rank-compute 展开一次；归纳假设给出每个成员的秩是序数，封闭引理 suc-ord 给出每个后继是序数，封闭引理 setUnion-ord 给出这一族序数之并仍是序数。

命题对所有集合量化，故证明是以 λ A → IsOrd (rank A) 为谓词的成员归纳。归纳假设对 A 的每个成员 y 给出「rank y 是序数」的证书。由于 rank-compute A 在命题意义下把 rank A 等同于步进所得，目标可沿计算路径 rank-compute A 传输 IsOrd 而达成，剩下只需证步进所得的并是序数。

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

最后一步组合两个封闭事实。每个族元 sucV (rank (⟪ A ⟫↪ m)) 是某序数的后继，故由 suc-ord 是序数，其输入证书由归纳假设与辅助 mem 供给。随后 setUnion-ord 保证序数的小索引并仍是序数。从假设到结论的链条是：若成员的秩是序数，则集合的秩也是序数。

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

界住秩

若一个集合的每个成员的秩都属于某序数，则该集合的秩包含于该序数：定义之并的每个成员都落在某个成员之秩的后继中，传递性给出所需包含。序数的不动点性质与可构造层中的秩界都用这条论证。

所述是逐点包含而非严格隶属：在 IsOrd β 与「每个成员秩 rank y 严格属于 β」的假设下，结论是 rank A 的每个成员都属于 β。证明从定义之并的形状出发消去。属于该并经 union-family-out 给出仅仅一个索引 m 使 x ∈ˢ s m；由于目标 x ∈ˢ β 是命题，对这个截断做消去是合法的，随后 ∈sucV-elim 把在后继 s m = sucV (rank (⟪ A ⟫↪ m)) 中的隶属分成两种情形。

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

后继的两种情形正是序数性发挥作用之处。若 x 属于 rank (⟪ A ⟫↪ m)，则因 β 传递且该秩已在 β 中，x 也在 β 中：这是分支 oβ .fst h (below m)。若 x 直接等于 rank (⟪ A ⟫↪ m)，第二支沿该路径传输界 below m。两种情形的结论都落在 x ∈ˢ β。union-family-out 给出的索引与证明位于命题截断中；由于目标 x ∈ˢ β 是命题，PT.rec 可以逐个处理其中的 (m , hm)，而不选择一个全局索引。

    (λ 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

族 s 就是递归方程中的后继之秩的族，把索引 m 映到 sucV (rank (⟪ A ⟫↪ m))。事实 below m 是把假设 bound 作用于被嵌入成员 ⟪ A ⟫↪ m 及其成员证明，得到 rank (⟪ A ⟫↪ m) ∈ˢ β。整个引理因此不依赖任何归纳：按计算法则改写一次，拆开并，让序数的传递性吸收后继。

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

序数是自身的秩

仍是成员归纳，而这次的证明是 rank A 与 A 之间的一次外延。从左到右：rank A 的元素落在某个成员之秩的后继里面，而依归纳假设那个秩就是该成员，故该元素或就是该成员，或属于它，两种情形都经传递性属于 A。从右到左：A 的成员是自身的秩，故属于该秩的后继，而那是并的一支。

定理说秩固定每个序数，以路径而非等价的形式。归纳以把序数性假设与结论打包在一起的谓词 λ A → IsOrd A → rank A ≡ A 设立，因为步进确实需要它：要比较 rank A 与 A，必须知道序数 A 的成员本身也是序数。于是步进在收到递归等式 rank y ≡ y 之外，还收到证书 IsOrd A，并返回在 A 处的等式。

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

等式本身来自 extensionalV，它把逐点的隶属等价变成集合的路径，⇔toPath 打包两个方向。被比较的两个集合保持不展开。向前的方向 toA 不是别的，正是取 β = A 的 rank-upper：作用在成员秩上的序数界就是 A 自身，而界定假设由归纳假设当场构造。

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

两个方向都依赖同一事实 mem-ord：序数 A 的成员仍是序数，故归纳假设适用于它。对 toA，rank-upper 要求的假设是 rank y ∈ˢ A；由归纳假设 rank y ≡ y 且已给 y ∈ˢ A，传输即可落位。对 fromA，方向相反：rank-mono x A x∈A 给出 rank x ∈ˢ rank A，而归纳假设的路径 rank x ≡ x 把它传输成 x ∈ˢ rank A。至此所有材料齐备，路径 rank A ≡ A 随之成立。

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

小结

rank 以序数度量每个集合 (rank-ord)，并固定序数自身 (rank-fix)，二者表明它是与每个序数一致的序数值度量。两个证明都是正则性上的成员归纳，故本章不引入任何额外假设。它给出沿成员关系严格增长的序数值度量，以及被测集合本身为序数时所需的不动点律。