---
title: "von Neumann ランク"
module: L.Rank
lang: ja
site: "Bedrock"
description: "von Neumann ランク"
stage: "構成可能段階と公理"
reading_order: 27
canonical: https://bedrock.institute/ja/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/zh/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` が要求するものです。ステップの形に注意してください。`rank` を直接呼ぶのではなく、関数 `rec` を通して再帰的な値を受け取ります。これが `∈-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` が何らかの族の元、すなわち `y` の要素 `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)
```

## ランクの上界

`β` が順序数で、`A` の各要素のランクを含むなら、ランクの再帰方程式と `β` の推移性により `rank A ⊆ β` が従います。この補題は集合全体のランクを一つの順序数で抑えます。

主張は狭義の所属ではなく各点ごとの包含です。`IsOrd β` と、すべての要素のランク `rank y` が狭義に `β` に属するという仮定の下で、`rank A` のすべての要素が `β` に属すると結論します。証明は定義の和の形からの消去です。和への所属は `union-family-out` を通して、`x ∈ˢ s m` となる添字 `m` を単に (merely) 与えます。ゴール `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 ∈ˢ β` に着地します。消去子が和集合から受け取るのは単に (merely)`hm : ⟨ x ∈ˢ s m ⟩` なので、ファイバー `(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`)。この二つは、ランクが各順序数と一致する順序数値尺度であることを示します。どちらの証明も正則性公理の上の所属帰納であり、本章は追加の仮定を一切使いません。これにより、所属に沿って狭義に増加する順序数値尺度と、対象が順序数である場合の不動点法則が得られます。