Ordinals

上一章的塔以序数为索引，而本书迄今只用到关于序数的一个事实：「是序数」是命题。接下来的构造要得更多。可构造宇宙的每一个闭包论证都是同一个形状：一个集合由散落在各个阶段的材料造出，而论证必须把结果安置在单一阶段上。所以诸公理向序数索取的不是一套序理论，而是一批上界。

本章恰好提供这批上界，别无他物。零是序数；序数的后继是序数；序数之并是序数；以及本章的交付物：任一小族序数都落在单一序数之下。最后这条把「每份材料各有其阶段」变成「它们共处同一阶段」，而这正是下一章每个闭包证明所做的动作。

显眼地缺席的是比较。人们期望序数是线序的，它们确实是，但那个事实不构造，而且此处用不上：公共上界比比较廉价，而公理要的只是公共上界。本书取那条廉价的路，于是可构造宇宙的基本公理不花费任何经典逻辑。

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

open import Base.Prelude
open import Base.Truth

module L.Ordinal {ℓ : Level} where

open import FOL.ZFStructure using ( module hPropStructure )
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ )
open import V.Model {ℓ} using ( ∈sucV-elim; ∈sucV-inl; self∈sucV )
open import V.Coding {ℓ} using ( #-inj′ )
open import L.Constructible {ℓ}
  using ( isTransV; isPropIsTransV; ∅-trans; setUnion-trans; IsOrd; isPropIsOrd )

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 )
open import Cubical.HITs.CumulativeHierarchy.Base using ( sett )
open import Cubical.HITs.CumulativeHierarchy.Properties using ( _∈ₛ_; ∈∈ₛ )
open import Cubical.HITs.CumulativeHierarchy.Constructions
  using ( ∅; ∅-empty; ⋃_; union-ax; module InfinitySet )
open InfinitySet using ( sucV; #_; ω; #-in-ω )

open TruthAlgebra (hPropAlgebra (ℓ-suc ℓ))
open hPropStructure 𝒮ᵥ

零与后继

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

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

后继 sucV A 把 A 自身添作成员，而层级那一章留下了推理它的工具：sucV A 的成员要么是 A 的成员，要么就是 A 自身，这个分情形是命题级的消去子。序数谓词的两半都照着它走。传递性一半：sucV A 的成员之成员，或经 A 的传递性、或在退化支上直接地，落回 A；第二半：sucV A 的成员或是 A 的成员 (依假设传递)、或就是 A (仍依假设传递)。

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 → ∈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)
    (λ x≡A → subst isTransV (sym x≡A) Atr)

并与上界

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

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
  memTr z z∈⋃ = PT.rec (isPropIsTransV z)
    (λ { (w , (w∈ₛsett , z∈ₛw)) → PT.rec (isPropIsTransV z)
        (λ { (x , fx≡w) → hf x .snd z
               (∈∈ₛ {a = z} {b = f x} .snd
                 (subst (λ W → ⟨ z ∈ₛ W ⟩) (sym fx≡w) z∈ₛw)) })
        (∈∈ₛ {a = w} {b = sett X f} .snd w∈ₛsett) })
    (union-ax (sett X f) z .fst (∈∈ₛ {a = z} {b = ⋃ (sett X f)} .fst z∈⋃))

然后是本章的交付物。给定一小族序数，有单一序数包含该族的每一个成员。朴素的尝试，取该族之并，只能给出包含关系：并吸收其成员的元素，而非成员本身，且没有集合以自身为成员。补救是一步后继：改取后继族之并。于是 f x 属于 sucV (f x)，后者属于被取并的那个族，故 f x 属于该并，这正是闭包论证所需。结果是货真价实的序对，而非截断的存在：消费方要点名那个上界，并造出它的阶段。

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
  g x = sucV (f x)
  β : S
  β = ⋃ (sett X g)
  ordβ : IsOrd β
  ordβ = setUnion-ord X g (λ x → suc-ord (hf x))
  memβ : (x : X) → ⟨ f x ∈ˢ β ⟩
  memβ x = ∈∈ₛ {a = f x} {b = β} .snd
    (union-ax (sett X g) (f x) .snd
      ∣ sucV (f x) , (s∈ₛsett , fx∈ₛs) ∣₁)
    where
    s∈ₛsett : ⟨ sucV (f x) ∈ₛ sett X g ⟩
    s∈ₛsett = ∈∈ₛ {a = sucV (f x)} {b = sett X g} .fst ∣ x , refl ∣₁
    fx∈ₛs : ⟨ f x ∈ₛ sucV (f x) ⟩
    fx∈ₛs = ∈∈ₛ {a = f x} {b = sucV (f x)} .fst (self∈sucV (f x))

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

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
  f : Lift {ℓ-zero} {ℓ} Bool → S
  f (lift true)  = σ₁
  f (lift false) = σ₂
  fo : (b : Lift {ℓ-zero} {ℓ} Bool) → IsOrd (f b)
  fo (lift true)  = o₁
  fo (lift false) = o₂
  r = boundingOrd (Lift {ℓ-zero} {ℓ} Bool) f fo

成员

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

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

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

数码，及其极限

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

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

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

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)
  (λ 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 ω
ω-ord = trans-ω , (λ x x∈ω → ω-mem-ord x x∈ω .fst)
  where
  trans-ω : isTransV ω
  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 的数码的成员，恰是更小自然数的数码。前一半即消去，是一次沿后继消去子的归纳；后一半，即数码属于数码意味着序号可比，则由单射性得出。编码诸章将用它们从一个集合里读出序号，而那正是变元的界最终的含义。

∈#-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
  (λ 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 })
  (∈#-elim b (# a) h)

小结

零、后继与序数的小并都是序数，而 boundingOrd 以单一序数界住任一小族。最后这条就是本章的全部目的：它把「有穷多份材料各有其阶段」变成「它们同处一个阶段」，而下一章会把它花掉三次，头几条闭包公理各一次。向下封闭、无自环，以及 ω 自身是序数，都是同一套理论的续篇；它们在此等候无穷公理的收集那一步，那是最先需要它们的地方。