---
title: "Von Neumann 秩"
module: L.Rank
lang: zh
site: "Bedrock"
description: "Von Neumann 秩"
stage: "可构造层与公理"
reading_order: 27
canonical: https://bedrock.institute/zh/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/en/L.Rank.md, https://bedrock.institute/ja/L.Rank.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
# 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` 中的值。

```agda
{-# 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` 再给出其成员的序数性。

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

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

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

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

```agda
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` 的步进。

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

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

```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-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` 再把它提升进并，包括沿计算路径的传输。

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

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

```agda
  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` 而达成，剩下只需证步进所得的并是序数。

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

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

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

## 界住秩

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

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

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

后继的两种情形正是序数性发挥作用之处。若 `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)`，而不选择一个全局索引。

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

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

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

## 序数是自身的秩

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

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

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

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

两个方向都依赖同一事实 `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` 随之成立。

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

## 小结

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