---
title: "序数的封闭性与有限序数"
module: L.Ordinal
lang: zh
site: "Bedrock"
description: "序数的封闭性与有限序数"
stage: "可构造层与公理"
reading_order: 26
canonical: https://bedrock.institute/zh/L.Ordinal.html
html: L.Ordinal.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/Ordinal.lagda.md
prerequisites: [Base.Prelude, FOL.ZFStructure, V.Hierarchy, V.Model, V.Coding, L.Constructible]
routes: [constructible-axioms]
translations: [https://bedrock.institute/en/L.Ordinal.md, https://bedrock.institute/ja/L.Ordinal.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
# 序数的封闭性与有限序数

序数是其成员也都传递的传递集。本章证明序数对零、后继与并封闭，为小族构造序数上界，并刻画有限数码之间及其与 `ω` 的隶属关系。

本章先建立这些封闭与取界工具，再转向有限序数。零是序数；序数的后继是序数；序数之并是序数；以及本章的主要结果：任一小族序数都落在单一序数之下。最后这条把「小族的每个成员**各有**序数上界」变成「整个小族共用**同一**序数上界」；后面的分离、幂集、递归、反射与 GCH 构造都会使用这种形式。

本章没有给出序数的比较。序数确实构成线序，但该事实不是构造性的，而且此处也不需要它：这些公理只要求公共上界，因此本书在这里直接构造公共上界。本章的封闭与取界证明都不假设经典逻辑。

序数谓词在可构造宇宙一章中定义为 `IsOrd A = isTransV A × ((x : S) → ⟨ x ∈ˢ A ⟩ → isTransV x)`：它是传递性证明与「`A` 的每个成员自身传递」之证明的序对。两个分量都是命题，`isPropIsOrd` 证明了这一点，因此 `IsOrd` 是真正的真值，而不是携带结构的数据。本模块固定周遭宇宙层级 `ℓ`，并在其上的累积层级载体 `S` 中工作。

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

open import Base.Prelude

module L.Ordinal {ℓ : Level} where

open import FOL.ZFStructure using ( module hPropStructure )
```

这里会合了两套工具。来自周遭层级 `V` 一侧的有后继 `sucV`、其隶属消去子，以及小族之并；来自可构造宇宙 `L` 一侧的有空集与小并的传递性引理，以及谓词 `IsOrd` 本身。本章的全部结论都只涉及底层的集合，尚未触及可构造性，因此下面的任何陈述都不出现排中律假设。

```agda
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ )
open import V.Model {ℓ} using ( union-family-in; union-family-out; ∈sucV-elim; ∈sucV-inl; self∈sucV )
open import V.Coding {ℓ} using ( #-inj′ )
open import L.Constructible {ℓ}
  using ( isTransV; isPropIsTransV; ∅-trans; setUnion-trans; IsOrd; isPropIsOrd )
```

这些证明中反复出现的模式是截断见证的消去。属于一个并的成员只是**仅仅**由某个指标与某个成员见证，因此关于并之全体成员的事实要用 `PT.rec` 提取到一个命题值的目标中。正因如此，每条闭包引理在消耗截断之前先指明目标命题，例如 `isPropIsTransV z`：`∥ A ∥₁` 的消去恰好允许进入这类命题。

```agda
open import Cubical.Data.Nat.Order using ( _<_; ≤-suc; isProp≤ )
import Cubical.Data.Empty as Empty
import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∣_∣₁; ∥_∥₁; squash₁ )
open import Cubical.Data.Bool using ( Bool; true; false )
```

数码 `# n` 是层级的冯·诺依曼自然数：`# 0` 是空集，`# (suc n)` 是 `# n` 的后继。它们的极限 `ω`，以及每个数码都属于 `ω`，来自无穷构造。本章最后一节将从隶属关系 `z ∈ˢ (# n)` 中读回一个自然数序号，所用的是数码编码的单射性。

```agda
open import Cubical.HITs.CumulativeHierarchy.Base using ( sett )
open import Cubical.HITs.CumulativeHierarchy.Properties using ( ∈∈ₛ )
open import Cubical.HITs.CumulativeHierarchy.Constructions
  using ( ∅; ∅-empty; ⋃_; module InfinitySet )
open InfinitySet using ( sucV; #_; ω; #-in-ω )
```

最后一个约定：`hProp` 上的直接运算在全章可用，于是「命题 `P` 的底类型」的记号 `⟨ P ⟩`，而索引联结词直接作用于命题。这里的命题，如 `isTransV A` 与 `IsOrd A`，位于 `ℓ` 之上一层，而这正是稍后公理进行量化的层级。

```agda
open hPropStructure 𝒮ᵥ
```

## 零与后继

回忆那个谓词：序数是成员皆传递的传递集。两半对空集都真空成立，于是零是序数，无须证明什么。

证书 `∅-ord` 把两个真空的半边打包起来。`∅` 的传递性用已证的引理 `∅-trans`；对第二半，函数必须接受任何声称有 `x ∈ˢ ∅` 的 `x`，但空集引理把这一隶属转化为空宿主类型中的一个元素，`Empty.rec` 由此证明任何命题。不可能存在的成员不施加任何义务。

```agda
∅-ord : IsOrd ∅
∅-ord = ∅-trans
      , (λ x x∈∅ → Empty.rec (∅-empty x (∈∈ₛ {a = x} {b = ∅} .fst x∈∅)))
```

后继 `sucV A` 把 `A` 自身添作成员。`sucV A` 的成员要么是 `A` 的成员，要么就是 `A` 自身；这个分情形是命题级的消去子 `∈sucV-elim`，它要求目标是命题并接受两个分支。序数谓词的两半都照着这个消去子走。

`sucV A` 的传递性要从「`y ∈ˢ x` (就 `A` 内部的项而言) 与 `x ∈ˢ sucV A`」推出 `y ∈ˢ sucV A`。消去子消耗 `x∈suc`，它交给每个分支的证明义务又是一个对 `sucV A` 的隶属，因此以命题性论证 `snd (y ∈ˢ sucV A)` 作为目标。

```agda
suc-ord : ∀ {A} → IsOrd A → IsOrd (sucV A)
suc-ord {A} (Atr , Amem) = trans-sucV , mem-sucV
  where
  trans-sucV : isTransV (sucV A)
  trans-sucV {x} {y} y∈x x∈suc = ∈sucV-elim (snd (y ∈ˢ sucV A)) x∈suc
```

第一分支中 `x` 是 `A` 的成员，于是把 `A` 的传递性用于 `y ∈ˢ x` 与 `x ∈ˢ A` 得到 `y ∈ˢ A`，进而 `y ∈ˢ sucV A`。第二分支中 `x` 被等同于 `A` 自身，于是 `y ∈ˢ x` 沿这条路径直接传递为 `y ∈ˢ A`；这里无需关于 `A` 的任何额外事实。

```agda
    (λ x∈A → ∈sucV-inl (Atr y∈x x∈A))
    (λ x≡A → ∈sucV-inl (subst (λ w → ⟨ y ∈ˢ w ⟩) x≡A y∈x))
  mem-sucV : (x : S) → ⟨ x ∈ˢ sucV A ⟩ → isTransV x
  mem-sucV x x∈suc = ∈sucV-elim (isPropIsTransV x) x∈suc
    (λ x∈A → Amem x x∈A)
```

第二半，即 `sucV A` 的每个成员都传递，是同一分情形配以不同目标。`A` 的成员由假设 `Amem` 得到传递性；在 `x` 等于 `A` 的分支中，把传递性 `Atr` 沿反向路径传递回去。`isTransV x` 的命题性正是消去子在此适用的原因。

```agda
    (λ x≡A → subst isTransV (sym x≡A) Atr)
```

## 并与上界

序数对小索引并封闭。传递性就是传递集那边已证的闭包引理；第二半：并的成员落在某个 `f x` 里面，而依假设该族元是序数，故其成员传递。

族由小的索引类型 `X` 与映射 `f : X → S` 给出，因此并 `⋃ (sett X f)` 是由真实的函数构造的集合，而非截断的枚举。其传递性直接取自 `setUnion-trans`，并喂入各假设 `hf x` 的第一个分量。

```agda
setUnion-ord : (X : Type ℓ) (f : X → S) → ((x : X) → IsOrd (f x))
             → IsOrd (⋃ (sett X f))
setUnion-ord X f hf = setUnion-trans X f (λ x → hf x .fst) , memTr
  where
  memTr : (z : S) → ⟨ z ∈ˢ (⋃ (sett X f)) ⟩ → isTransV z
```

剩下的义务是：`union-family-out` 表明 `z ∈ˢ ⋃ (sett X f)` 仅仅意味着 `z` 落在某个 `f x` 中。由于目标 `isTransV z` 是命题，`PT.rec` 可以消去该截断，而在每个分支中 `hf x .snd z hz` 恰好给出所需证书：序数族元的成员是传递的。

```agda
  memTr z z∈⋃ = PT.rec (isPropIsTransV z)
    (λ { (x , hz) → hf x .snd z hz }) (union-family-out X f z z∈⋃)
```

然后是本章的主要结果。给定一小族序数，有单一序数包含该族的每一个成员。若直接取该族之并，只能得到包含关系：并包含其成员的**元素**，而非这些成员本身，并且没有集合以自身为成员。因此改为对后继族取并。结果明确给出相应的序对，而不只是截断的存在；使用方可以指称这个上界，并构造它所在的层。

结果把上界 `β` 作为显式数据返回，并附带其序数证书及每个指标处的严格隶属 `f x ∈ˢ β`。后续证明可以直接投影出这个上界和各项隶属，而无需消去一个截断存在。

```agda
boundingOrd : (X : Type ℓ) (f : X → S) → ((x : X) → IsOrd (f x))
            → Σ[ β ∈ S ] (IsOrd β × ((x : X) → ⟨ f x ∈ˢ β ⟩))
boundingOrd X f hf = β , (ordβ , memβ)
  where
  g : X → S
```

构造就是三行数学。把 `f` 换成其后继 `g x = sucV (f x)`；取该族的并 `β`；再应用刚证得的并封闭，其假设成立是因为依后继引理每个 `sucV (f x)` 都是序数。

```agda
  g x = sucV (f x)
  β : S
  β = ⋃ (sett X g)
  ordβ : IsOrd β
  ordβ = setUnion-ord X g (λ x → suc-ord (hf x))
```

隶属关系正是必须绕经后继的原因。每个 `f x` 严格属于其自身的后继，`union-family-in` 把它提升进并，而并自身的传递性随后把这些严格隶属升级为下游闭包论证所用到的包含关系。

```agda
  memβ : (x : X) → ⟨ f x ∈ˢ β ⟩
  memβ x = union-family-in X g x (f x) (self∈sucV (f x))
```

二元情形值得单独命名，因为用得最多的正是它：把两个序数合并为一个严格包含二者的序数。族由布尔值索引，抬升到周遭宇宙以便通用引理得以适用，而两条隶属关系在两个索引处读出。

结果打包了三份数据：上界 β、β 是序数的证明，以及两条严格隶属 ⟨ σ₁ ∈ˢ β ⟩ 与 ⟨ σ₂ ∈ˢ β ⟩，用嵌套的积类型组合。主体只是从 `r` 中取出这些成分，在两个布尔索引 `lift true` 与 `lift false` 处读出两条隶属；`r` 由下方的 `where` 块构造。

```agda
bound2 : (σ₁ σ₂ : S) → IsOrd σ₁ → IsOrd σ₂
       → Σ[ β ∈ S ] (IsOrd β × ⟨ σ₁ ∈ˢ β ⟩ × ⟨ σ₂ ∈ˢ β ⟩)
bound2 σ₁ σ₂ o₁ o₂ =
  fst r , (r .snd .fst , r .snd .snd (lift true) , r .snd .snd (lift false))
  where
```

索引类型需要一句说明。`Bool` 住在 `Type ℓ-zero`，而 `S` 住在 `Type ℓ`，但 `boundingOrd` 要求索引类型落在 `Type ℓ` 中。`Lift` 只抬升层级而不改变元素：元素变成 `lift true` 与 `lift false`。函数 `f` 把它们送到 σ₁ 与 σ₂，`fo` 则在每个索引处附上相应的序数性假设。

```agda
  f : Lift {ℓ-zero} {ℓ} Bool → S
  f (lift true)  = σ₁
  f (lift false) = σ₂
  fo : (b : Lift {ℓ-zero} {ℓ} Bool) → IsOrd (f b)
  fo (lift true)  = o₁
```

再没有新东西要证。`r` 就是对这个二点族应用一般引理的结果；它已经给出了序数上界以及对每个索引的隶属，结果的两条隶属不过是同一证明在两个布尔值处的实例。

```agda
  fo (lift false) = o₂
  r = boundingOrd (Lift {ℓ-zero} {ℓ} Bool) f fo
```

## 成员

序数向下封闭：序数的成员是序数。它自身的传递性就是假设的第二半；而成员的传递性，则经传递性把它们拉回外层序数即得。

层级那一章的无自环性，即没有集合属于自身，是这些论证需要的另一个事实；此处提起它，是因为序数的证明正是从这里开始取用。

拆开来看，假设 `IsOrd A` 是一个序对：`Atr` 即 `A` 的传递性，`Amem` 即「`A` 的每个成员都传递」。于是结论的前半就是 `Amem x x∈A`。后半：设 `y` 满足 `y ∈ x ∈ A`，由 `A` 的传递性得 `y ∈ A`，再由 `Amem y` 知 `y` 传递，这正是要对 `x` 的每个成员所说的话。

```agda
mem-ord : ∀ {A} → IsOrd A → (x : S) → ⟨ x ∈ˢ A ⟩ → IsOrd x
mem-ord {A} (Atr , Amem) x x∈A =
  Amem x x∈A , (λ y y∈x → Amem y (Atr y∈x x∈A))
```

## 数码，及其极限

层级的数码是零的迭代后继，故由上面两个事实即为序数，只需一层归纳。它们的极限 `ω` 也是序数，而那正是收集步骤将要用到的事实。其第二半由数码直接给出；第一半即传递性，说的是数码的成员仍是数码，那是另一次归纳，后继情形按消去子分情形。

对这种推理方式要提一句：属于 `ω` 只是**仅仅**给出一个索引。因此下面的证明从不取出一个选定的自然数，而是把截断消去到命题值的目标上，例如 `IsOrd y` 或某条隶属陈述。

由定义 `# zero = ∅` 与 `# suc n = sucV (# n)`，归纳在每种情形各占一行：空集由第一节可知是序数，序数的后继由第二节可知是序数。

```agda
numeral-ord : (n : ℕ) → IsOrd (# n)
numeral-ord zero    = ∅-ord
numeral-ord (suc n) = suc-ord (numeral-ord n)
```

在累积层级库中，`ω` 被表现为成员由自然数索引的集合，所以属于 `ω` 就相当于携带一个数值索引。引理 `#-in-ω` 为每个数码给出该索引，`∈∈ₛ` 再把所得的索引转成隶属命题 ⟨ `# k` ∈ˢ `ω` ⟩。

```agda
#∈ω : (k : ℕ) → ⟨ (# k) ∈ˢ ω ⟩
#∈ω k = ∈∈ₛ {a = # k} {b = ω} .snd (#-in-ω k)
```

下一条是数码的向下封闭，直接表述为「属于 `ω`」：`# k` 的每个成员都是 `ω` 的成员。对 `k` 的归纳底情形真空成立，因为没有东西属于空集。后继情形由 `sucV` 的消去子分成两支：要么 `y` 已经在 `# k` 中，此时用归纳假设；要么 `y` 等于 `# k` 自身，此时由上一条引理得到属于 `ω`。

```agda
numeral-mem : (k : ℕ) (y : S) → ⟨ y ∈ˢ (# k) ⟩ → ⟨ y ∈ˢ ω ⟩
numeral-mem zero y y∈ =
  Empty.rec (∅-empty y (∈∈ₛ {a = y} {b = ∅} .fst y∈))
numeral-mem (suc k) y y∈ = ∈sucV-elim (snd (y ∈ˢ ω)) y∈
  (λ y∈#k → numeral-mem k y y∈#k)
```

反过来，`ω` 的每个成员都是序数。属于 `ω` 仅仅给出一个自然数 `k` 使 `# k ≡ y`；目标 `IsOrd y` 由 `isPropIsOrd` 是命题，因此截断可以消去到它上面。沿路径 `# k ≡ y`，`# k` 的序数性被搬运到 `y`。这里没有选定任何具体索引；无论截断背后藏着哪一个，论证都一致适用。

```agda
  (λ y≡#k → subst (λ w → ⟨ w ∈ˢ ω ⟩) (sym y≡#k) (#∈ω k))

ω-mem-ord : (y : S) → ⟨ y ∈ˢ ω ⟩ → IsOrd y
ω-mem-ord y y∈ω = PT.rec (isPropIsOrd y)
  (λ { (k , #k≡y) → subst IsOrd #k≡y (numeral-ord (lower k)) })
  y∈ω
```

两半合起来得到 `ω-ord : IsOrd ω`。其第一个分量 `trans-ω` 建立 `isTransV ω`：从 `y ∈ x ∈ ω` 出发，关于 `x` 的假设仅仅给出索引 `k` 使 `# k ≡ x`，沿该路径搬运后，`numeral-mem` 把 `y` 放进 `ω`。这一消去进入命题值的目标，这正是允许去掉截断的理由。

```agda
ω-ord : IsOrd ω
ω-ord = trans-ω , (λ x x∈ω → ω-mem-ord x x∈ω .fst)
  where
  trans-ω : isTransV ω
```

对 `ω` 的每个成员 `x`，`ω-mem-ord x x∈ω` 证明 `IsOrd x`；它的第一个分量正是 `IsOrd ω` 的第二个分量所需的 `x` 的传递性。两部分合起来得到 `IsOrd ω`。

```agda
  trans-ω {x} {y} y∈x x∈ω = PT.rec (snd (y ∈ˢ ω))
    (λ { (k , #k≡x) →
      numeral-mem (lower k) y (subst (λ w → ⟨ y ∈ˢ w ⟩) (sym #k≡x) y∈x) })
    x∈ω
```

## 数码之下有什么

数码不只是序数，它们还被序数**计数**：`n` 的数码的成员，恰是更小自然数的数码。前一半说的是消去，它由一次沿后继消去子的归纳得到；后一半，即数码属于数码意味着序号可比，则由单射性得出。编码诸章将用这两件事实从一个集合里读出序号，而这正是变元的界最终的含义。

消去引理说：`# n` 的成员 `z` 仅仅来自某个更小的索引，即仅仅存在 `m < n` 使 `z ≡ # m`。陈述有意落在命题截断之中：证明不从截断中选取见证，只使用某个这样的分解存在这一命题。底情形真空成立，因为属于空集导致矛盾。

```agda
∈#-elim : (n : ℕ) (z : S) → ⟨ z ∈ˢ (# n) ⟩
        → ∥ Σ[ m ∈ ℕ ] ((m < n) × (z ≡ # m)) ∥₁
∈#-elim zero    z h = Empty.rec (∅-empty z (∈∈ₛ {a = z} {b = ∅} .fst h))
∈#-elim (suc n) z h = ∈sucV-elim {A = # n} {x = z}
  {P = ∥ Σ[ m ∈ ℕ ] ((m < suc n) × (z ≡ # m)) ∥₁} squash₁ h
```

后继情形中，`sucV` 的消去子把「属于 `# (suc n)`」分成两支。若 `z` 在 `# n` 中，归纳假设给出 `m < n` 与 `z ≡ # m`，再用 `≤-suc` 提升为 `m < suc n`。若 `z` 就是 `# n` 自身，见证即 `n` 本身，其严格不等式由 `0` 与 `refl` 给出。对于配套的 `#∈#-elim`，把它应用于 `# b` 中的 `z = # a`：得到一个截断的三元组，其中方程 `# a ≡ # m` 经单射性引理 `#-inj′` 化为 `a ≡ m`，再沿该等同把 `m < b` 转成所要的 `a < b`。

```agda
  (λ z∈#n → PT.map (λ { (m , p , e) → m , ≤-suc p , e }) (∈#-elim n z z∈#n))
  (λ e → ∣ n , (0 , refl) , e ∣₁)

#∈#-elim : (a b : ℕ) → ⟨ (# a) ∈ˢ (# b) ⟩ → a < b
#∈#-elim a b h = PT.rec isProp≤
  (λ { (m , p , e) → subst (_< b) (sym (#-inj′ e)) p })
```

最后一步是消去截断本身。ℕ 上的严格序由 `isProp≤` 是命题值的，因此消去到 `a < b` 是合法的；结论只需要**某个**见证索引成立，并不需要典范的那个。

```agda
  (∈#-elim b (# a) h)
```

## 小结

零、后继与序数的小并都是序数，而 `boundingOrd` 以单一序数界住任一小族。这一上界把任意小族的逐点序数界合并为一个严格公共界。后续各章分别使用这些结果：ZF 公理证明用序数界收集层，有限序数引理与 `ω-ord` 则用于无穷公理及后面的编码论证。