---
title: "順序数の閉性と有限順序数"
module: L.Ordinal
lang: ja
site: "Bedrock"
description: "順序数の閉性と有限順序数"
stage: "構成可能段階と公理"
reading_order: 26
canonical: https://bedrock.institute/ja/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/zh/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 )
```

これらの証明で繰り返される型は、截断された証人の消去です。和集合への所属は、ある添字とある要素によって**単に (merely)** 証明されるだけなので、和のすべての要素に関する事実は `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 𝒮ᵥ
```

## 零と後続

述語を思い出しましょう。順序数とは、推移的集合であって、その要素がすべて推移的であるものです。空集合に対しては両方の条件が空虚に成立するので、零は順序数であり、証明すべきことは何もありません。次に、順序数 `A` から後続 `sucV A` が再び順序数であることを示します。

証明書 `∅-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` と `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` に属することを**単に (merely)** 意味することを述べます。目標 `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 ∈ x ∈ A` なる `y` を取ると、`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))
```

## 数項とその極限

階層の数項は零の後続の繰り返しなので、前節の二つの事実から帰納法によってただちに順序数です。その極限 `ω` も順序数であり、これが後に収集の場面で必要になる事実です。後半は数項に関する補題から直接従います。前半の推移性は「数項の要素は再び数項である」という主張で、これも別の帰納法であり、後続の場合は消去子で場合分けします。

推論の仕方について一言注意しておきます。`ω` への所属は索引を**単に (merely)** 与えるだけです。したがって以下の証明は特定の自然数を選び出すことはせず、`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 ≡ y` なる自然数 `k` を単に (merely) 与えるだけです。目標の `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 ≡ x` なる索引 `k` を単に与えるだけで、そのパスに沿って輸送した後、`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` が単に (merely) より小さい索引から来ることを述べます。すなわち、`z ≡ # m` なる `m < n` が単に存在するということです。この主張が意図的に命題的切断の中に置かれている点に注意してください。この証明は切断から証人を選ばず、そのような分解が存在するという命題だけを使います。底の場合は空虚に成り立ちます。空集合への所属は矛盾をもたらすからです。

```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` に属するなら、帰納法の仮定から `z ≡ # m` なる `m < n` が得られ、`≤-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` は無限公理や後の符号化で使われます。