---
title: "序数由隶属关系线性排序"
module: L.Ordinal.Linear
lang: zh
site: "Bedrock"
description: "序数由隶属关系线性排序"
stage: "可构造层与公理"
reading_order: 28
canonical: https://bedrock.institute/zh/L.Ordinal.Linear.html
html: L.Ordinal.Linear.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/Ordinal/Linear.lagda.md
prerequisites: [Base.Prelude, Base.Classical, FOL.ZFStructure, V.Hierarchy, L.Constructible, L.Ordinal]
routes: [constructible-axioms]
translations: [https://bedrock.institute/en/L.Ordinal.Linear.md, https://bedrock.institute/ja/L.Ordinal.Linear.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
# 序数由隶属关系线性排序

任两个序数，或一者属于另一者，或二者相等。本章把这种比较所需的经典步骤单独列出，并说明为何需要显式假设。

迄今关于序数的一切都是闭包：零是序数，后继是，并也是，上界存在。闭包陈述关乎建造；它们从不需要**判定**任何东西。三歧要判定。给定两个彼此之间不假设任何关系的序数，它要回答三种互斥情形中的哪一种成立，本章从显式的排中律参数取得这一判定。所以本章把排中律取作模块参数，采用基础层定下的逐层级打包形式，使用 `ord-tri` 的模块都显式接收这个参数。

来自环境层级的两样材料使证明比教科书版本更短。正则性给出良基归纳，而且要用两次，两个自变量各一次。外延性意味着互相包含**就是**相等，故相等那一情形无须另行处理。排中律既判定两个方向的包含，也判定把包含失败转成截断反例时所需的成员关系命题。

全章只在模块参数的形式下使用一条经典假设：`LEM (ℓ-suc ℓ)` 的一个实例。回顾基础层的形状：对每个命题 `P : hProp (ℓ-suc ℓ)`，它返回 `⟨ P ⟩` 的证明，或一个反驳，即从 `⟨ P ⟩` 映入空类型的映射。这个层级恰好匹配 `⊆ᵇ-prop A B : hProp (ℓ-suc ℓ)` 以及反例论证中被判定的成员关系命题。把假设保留为显式模块参数，会在每次使用本模块时记录经典输入。

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

open import Base.Prelude
open import Base.Classical using ( LEM )

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

证明直接在环境层级 V 中进行，而不经由对象语言。载体与结构隶属 `∈ˢ` 来自打包在 `𝒮ᵥ` 上的 ZF 结构，因此 `⟨ x ∈ˢ A ⟩` 是一个 `hProp` 真值的底层命题。V 的两条原理承担数学重任：`extensionalV` 把一族成员关系的双向蕴含转换为相等的路径；`regularityV` 使隶属关系良基，从而支持其上的归纳。L 侧其余的导入 `mem-ord` 在每次递归调用处起作用：它表明序数的任何成员自身也是序数，这正是归纳假设能在下层使用的原因。

```agda
open import FOL.ZFStructure using ( module hPropStructure )
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ; extensionalV; regularityV )
open import L.Constructible {ℓ} using ( IsOrd )
open import L.Ordinal {ℓ} using ( mem-ord )

open import Cubical.Data.Sum using ( _⊎_; inl; inr )
```

判定程序要回答三种情形中哪一种成立，因此返回类型由三向和构造：左边是隶属关系，中间是相等，右边是隶属关系。还需要从双向蕴含到路径的转换，外延性论证将对载体的每一点使用它。空类型全程扮演反驳的角色：反驳一个命题，就是把它映入一个没有元素的类型。

```agda
open import Cubical.Functions.Logic using ( ⇔toPath )
import Cubical.Data.Empty as Empty
import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∣_∣₁; ∥_∥₁ )
import Cubical.Induction.WellFounded as WF
```

最后为整个文件打开两项约定。`hProp` 上的直接运算提供成员关系陈述所用的命题联结词，结构词汇把 `S` 固定为载体、`∈ˢ` 固定为其隶属关系，于是代码读起来是集合论而非逻辑管道。这些约定让后面的论证能直接追踪序数元素的隶属、相等与良基递归。

```agda
open hPropStructure 𝒮ᵥ
```

## 包含，及其失败的见证

证明围绕一个关系展开：逐点包含。若它双向成立，外延性使两个序数相等；若它在某一方向失败，排中律给出一个截断的反例成员；良基归纳与传递性再把这个反例转成严格比较。本小节固定这个关系及其打包方式。注意层级运算已经说明的事：包含住在 `Type (ℓ-suc ℓ)`，这正是所给排中律实例能判定它的那一层。

`A` 包含于 `B` 在这里不是初始概念而是定义出来的：`A` 的每个成员 `x`，在结构意义下，必须是 `B` 的成员。每个成员关系 `x ∈ˢ A` 是 `hProp` 中的命题，因此定义量化了载体 `S` 与 `ℓ` 层的命题，把整个关系放进 `Type (ℓ-suc ℓ)`。配套的 hProp 打包附上命题性的证明：到命题的依赖函数仍是命题，把这一点对两层嵌套的函数类型各用一次。这很重要，因为排中律是逐 hProp 判定的，而证明交给 `lem` 的正是这个打包后的陈述。

```agda
_⊆ᵇ_ : S → S → Type (ℓ-suc ℓ)
A ⊆ᵇ B = (x : S) → ⟨ x ∈ˢ A ⟩ → ⟨ x ∈ˢ B ⟩

⊆ᵇ-prop : (A B : S) → hProp (ℓ-suc ℓ)
⊆ᵇ-prop A B = (A ⊆ᵇ B) , isPropΠ (λ x → isPropΠ (λ _ → snd (x ∈ˢ B)))

ext-⊆ᵇ : {A B : S} → A ⊆ᵇ B → B ⊆ᵇ A → A ≡ B
```

三歧中的相等情形由层级的外延性免费给出。给定双向包含，载体的每一点 `x` 都给出 `⟨ x ∈ˢ A ⟩` 与 `⟨ x ∈ˢ B ⟩` 之间的双向蕴含；`⇔toPath` 把它变成路径，`extensionalV` 再把路径族组装成相等 `A ≡ B`。这里完全没有用到经典输入：外延性本身就是 V 的定理。

```agda
ext-⊆ᵇ {A} {B} s₁ s₂ = extensionalV (λ x → ⇔toPath (s₁ x) (s₂ x))
```

这里是真正经典的那一步。从包含**失败**出发，证明需要一个见证它的成员，而从「`B` 的成员并非都含于 `A`」过渡到「某个成员不含于 `A`」不是构造性的。排中律直接判定那个存在陈述：若没有这样的见证，则可以逐个判定成员关系，证明 `B` 的每个成员终究含于 `A`，与假设的失败矛盾。得出的见证仍是命题截断的，而这已经足够，因为三歧证明对它唯一要做的事就是把它消去成一个成员关系命题。

陈述是条件式的：若包含 `A ⊆ᵇ B` 可被反驳，则存在一个截断的见证，即 `A` 的一个成员 `a` 使 `a ∉ B`。结论刻意写成 `∥ ∥₁` 下的存在陈述，而非选定的对。第一步经典动作是判定截断的存在陈述 `Witness` 本身。注意层级的记账：见证陈述是 `ℓ-suc ℓ` 处的 hProp，恰好是模块的 `lem` 适用的地方，因此无须抬升。正分支中见证已在手；有趣的是负分支。

```agda
¬⊆ᵇ→witness : (A B : S) → (A ⊆ᵇ B → Empty.⊥)
            → ∥ Σ[ a ∈ S ] (⟨ a ∈ˢ A ⟩ × (⟨ a ∈ˢ B ⟩ → Empty.⊥)) ∥₁
¬⊆ᵇ→witness A B ¬sub = decide (lem Witness)
  where
  Witness : hProp (ℓ-suc ℓ)
```

设 `Witness` 可被反驳。那么对包含的反驳本身也可被反驳：对任意的 `x`，单独判定成员关系 `x ∈ˢ B`；在负分支中，把成员 `x` 连同 `x ∈ˢ A` 与对 `x ∈ˢ B` 的反驳组装成 `Witness` 的一个元素，与所给反驳矛盾。于是包含终究成立，把它交给假设的对包含的反驳就得到空类型。这正是上面宣布的模式：对 `Witness` 的一次全局判定，加上对每个 `x ∈ˢ B` 的逐点判定，共同把「不存在见证」转化为「包含成立」。

```agda
  Witness = ∥ Σ[ a ∈ S ] (⟨ a ∈ˢ A ⟩ × (⟨ a ∈ˢ B ⟩ → Empty.⊥)) ∥₁
          , PT.isPropPropTrunc
  decide : ⟨ Witness ⟩ ⊎ (⟨ Witness ⟩ → Empty.⊥) → ⟨ Witness ⟩
  decide (inl wit)  = wit
  decide (inr ¬wit) = Empty.rec (¬sub sub)
```

逐点判定值得停一停，因为它显示了截断的结论如何容纳截断的输入。要从 `x ∈ˢ A` 证明 `x ∈ˢ B`，用 `lem` 判定这一个成员关系。若成立则完成。若失败，对 `x ∈ˢ B` 的反驳连同 `x ∈ˢ A` 与 `x` 恰好是见证的数据，其截断 `∣ x , (x∈A , ¬x∈B) ∣₁` 是 `Witness` 的一个元素，与负分支的假设矛盾。

```agda
    where
    sub : A ⊆ᵇ B
    sub x x∈A = at (lem (x ∈ˢ B))
      where
      at : ⟨ x ∈ˢ B ⟩ ⊎ (⟨ x ∈ˢ B ⟩ → Empty.⊥) → ⟨ x ∈ˢ B ⟩
```

把各部分组装起来：对 `Witness` 的外层判定在正情形直接返回截断见证；在负情形，从假设的包含失败导出矛盾。辅助引理 `¬⊆ᵇ→witness` 现在可供三歧论证的两个方向使用，而且它承诺的从来不超过一个截断见证。保持截断显式正是使后面的消去合法的原因：命题截断只能消去到命题，而下一小节消去进入的成员关系陈述恰好是命题。

```agda
      at (inl x∈B)  = x∈B
      at (inr ¬x∈B) = Empty.rec (¬wit ∣ x , (x∈A , ¬x∈B) ∣₁)
```

## 三歧

主要定理的准备工作已经齐备。比较写成三向和：或者 `A` 是 `B` 的成员，或者二者由一条路径相等，或者 `B` 是 `A` 的成员。证明对两个自变量各作一次良基归纳，使得在叶子处可以递归到任一序数的成员内部。两个包含 `A ⊆ᵇ B` 与 `B ⊆ᵇ A` 在每个叶子处由排中律判定；上一小节完成了其余工作。读者在情形分析中应当带上的方向记账是：`B ⊆ᵇ A` 失败产生一个属于 `B` 而不属于 `A` 的成员，结论是 `A ∈ˢ B`；`A ⊆ᵇ B` 失败产生一个属于 `A` 而不属于 `B` 的成员，结论是 `B ∈ˢ A`。

陈述 `Tri A B` 把三种可能的答案打包进一个类型，由嵌套的和构造。外侧两种情形是结构意义的成员关系；中间情形是相等的路径。类型位于 `Type (ℓ-suc ℓ)`，这是其内部的成员关系命题所要求的层级。

```agda
Tri : S → S → Type (ℓ-suc ℓ)
Tri A B = ⟨ A ∈ˢ B ⟩ ⊎ ((A ≡ B) ⊎ ⟨ B ∈ˢ A ⟩)

ord-tri : (A : S) → IsOrd A → (B : S) → IsOrd B → Tri A B
ord-tri = WF.WFI.induction regularityV {P = P} stepA
  where
```

定理的形状是正则性供给的良基归纳。被证的谓词 `P A` 说的是：`A` 与任何与之比较的序数 `B` 都表现正确，并把两个序数性证明当作假设。于是正则性给出对第一个自变量的归纳：要证 `P A`，只需对 `A` 的每个成员 `A'` 证 `P A'`。这是两层嵌套归纳中的第一层；第二层对 `B`，将出现在步内。

```agda
  P : S → Type (ℓ-suc ℓ)
  P A = IsOrd A → (B : S) → IsOrd B → Tri A B

  stepA : (A : S) → (∀ A' → ⟨ A' ∈ˢ A ⟩ → P A') → P A
  stepA A IHA ordA =
    WF.WFI.induction regularityV {P = λ B → IsOrd B → Tri A B} stepB
```

外层步拿到 `A` 每个成员的归纳假设，随即运行第二个良基归纳，这次对 `B`，谓词是 `λ B → IsOrd B → Tri A B`。在内层归纳步中，两个包含由 `lem` 应用于打包命题 `⊆ᵇ-prop A B` 与 `⊆ᵇ-prop B A` 来判定。这两个判定开启经典的分情形；前面的辅助引理也使用排中律，把每个包含失败转成截断的反例。

```agda
    where
    stepB : (B : S) → (∀ B' → ⟨ B' ∈ˢ B ⟩ → IsOrd B' → Tri A B')
          → IsOrd B → Tri A B
    stepB B IHB ordB = decide (lem (⊆ᵇ-prop A B)) (lem (⊆ᵇ-prop B A))
      where
```

第一个失败情形假设 `B ⊆ᵇ A` 失败，于是仅仅存在 `B` 的一个不属于 `A` 的成员 `b`。辅助引理 `fromB` 表明这样一个显式的对能给出什么：由于 `b` 是序数 `B` 的成员，`mem-ord` 证明 `b` 自身是序数，内层归纳假设 `IHB` 便可比较 `A` 与 `b`。其第一种结果是 `A ∈ˢ b`；序数的传递性，即 `IsOrd B` 的第一个分量，再把它经由 `b ∈ˢ B` 提升为 `A ∈ˢ B`。

```agda
      fromB : Σ[ b ∈ S ] (⟨ b ∈ˢ B ⟩ × (⟨ b ∈ˢ A ⟩ → Empty.⊥)) → ⟨ A ∈ˢ B ⟩
      fromB (b , (b∈B , ¬b∈A)) = at (IHB b b∈B (mem-ord {A = B} ordB b b∈B))
        where
        at : Tri A b → ⟨ A ∈ˢ B ⟩
        at (inl A∈b)       = ordB .fst A∈b b∈B
```

比较 `A` 与 `b` 的另外两种结果依次处理。若 `A ≡ b` 是一条路径，则沿该路径把 `b ∈ˢ B` 反向搬运，即用 `subst` 配 `sym` 所做的，得到 `A ∈ˢ B`。若 `b ∈ˢ A`，则与 `b` 被选为 `A` 之外直接矛盾。三个分支都落入同一命题 `⟨ A ∈ˢ B ⟩`，这正是仅仅存在的见证在此够用的原因：截断的对被消去进命题，从不消去进数据。

```agda
        at (inr (inl A≡b)) = subst (λ w → ⟨ w ∈ˢ B ⟩) (sym A≡b) b∈B
        at (inr (inr b∈A)) = Empty.rec (¬b∈A b∈A)

      fromA : Σ[ a ∈ S ] (⟨ a ∈ˢ A ⟩ × (⟨ a ∈ˢ B ⟩ → Empty.⊥)) → ⟨ B ∈ˢ A ⟩
      fromA (a , (a∈A , ¬a∈B)) =
        at (IHA a a∈A (mem-ord {A = A} ordA a a∈A) B ordB)
```

镜像的辅助引理 `fromA` 覆盖另一个失败：`A ⊆ᵇ B` 失败，于是 `A` 的某个成员 `a` 不在 `B` 内。此时由外层归纳假设承担工作，因为它比较 `A` 的成员，并在 `a` 处应用。若 `a` 结果属于 `B`，则与 `a` 的选取矛盾；若 `a ≡ B`，搬运给出 `B ∈ˢ A`；若 `B ∈ˢ a`，则 `A` 的传递性把它经由 `a ∈ˢ A` 提升。注意镜像引入的不对称：相等分支沿路径搬运 `a ∈ˢ A` 而非反向搬运，因为这次被比较的一对方向相反。

```agda
        where
        at : Tri a B → ⟨ B ∈ˢ A ⟩
        at (inl a∈B)       = Empty.rec (¬a∈B a∈B)
        at (inr (inl a≡B)) = subst (λ w → ⟨ w ∈ˢ A ⟩) a≡B a∈A
        at (inr (inr B∈a)) = ordA .fst B∈a a∈A
```

两个转换器在手后，四种裁决组合归入三种答案。若两个包含都成立，由上一小节可知互相包含就是相等，返回中间答案。若 `A ⊆ᵇ B` 成立而 `B ⊆ᵇ A` 失败，则用 `PT.rec` 消去该失败的截断见证，这之所以合法，恰恰因为目标 `⟨ A ∈ˢ B ⟩` 是命题，其命题性由成员 hProp 的第二个分量提供。结果是左侧答案 `A ∈ˢ B`：这正是 `B ⊆ᵇ A` 失败而结论为 `A` 属于 `B` 的分支。

```agda
      decide : (A ⊆ᵇ B) ⊎ ((A ⊆ᵇ B) → Empty.⊥)
             → (B ⊆ᵇ A) ⊎ ((B ⊆ᵇ A) → Empty.⊥) → Tri A B
      decide (inl A⊆B) (inl B⊆A) = inr (inl (ext-⊆ᵇ A⊆B B⊆A))
      decide (inl A⊆B) (inr ¬B⊆A) =
        inl (PT.rec (snd (A ∈ˢ B)) fromB (¬⊆ᵇ→witness B A ¬B⊆A))
```

最后一种组合覆盖 `A ⊆ᵇ B` 的失败，无论第二个裁决如何，镜像转换器交付 `B ∈ˢ A`。与上面两种情形合并，每个叶子现在都返回 `Tri A B` 的一个元素，于是双层归纳闭合，`ord-tri` 成为关于任意序数 `A` 与 `B` 的定理。后续关于层序与基数的章节，例如 `L.GCH.CardinalSquareLaw`，把它当作自己的比较原语。

```agda
      decide (inr ¬A⊆B) _ =
        inr (inr (PT.rec (snd (B ∈ˢ A)) fromA (¬⊆ᵇ→witness A B ¬A⊆B)))
```

## 小结

结合层级成员关系已有的非自反性和 `IsOrd` 所含的传递性，`ord-tri` 现在给出任意两个序数的比较。这些比较定律构成后续层单调性与基数论证的序论基础。

`ord-tri` 比较任意两个序数，而本书为它提供一份排中律实例，并把它取作模块参数。这正是奠基部分为使其可审计而搭建的那道边界：无一处 postulate，使用 `ord-tri` 时必须提供本模块的排中律参数。随后的章节把这个比较用在它被需要的那个问题上：哪些序数出现在可构造层级的哪个层。