von Neumann ランク

ランクは累積階層 V ℓ の台 S の中で直接定義される。所属 x ∈ˢ y は命題値をとり、正則性によりこの所属関係は整礎である。したがって所属帰納 ∈-induction は、各要素ですでに定義された値から、現在の集合に対する S の値を定義できる。

module L.Rank {ℓ : Level} where

集合のランクは、その各要素のランクの後続を要素にわたって合わせた和集合である。記号で言えば、計算定理 rank-compute が rank x を rankStep x (λ y _ → rank y) と同一視する。本章で証明するのは四つの事実である。rank-mono はランクが所属に沿って狭義単調に増加すること、rank-ord はランクが常に順序数であること、rank-upper はランクがある順序数に含まれるという条件付きの結論を与えること、そして rank-fix はランクが順序数を固定することを言う。

ここでは外部の順序数の型は何も要らない。ランクは階層自身の中に値を取り、再帰は整礎な所属関係の上を走る。これは正則性公理が直接保証するものである。したがって本章の各定理には排中律のパラメータがない。

ランクでは、集合の各要素のランクの後続を集める必要がある。この構成を表すのが sucV と小さな添字付き和である。再帰的に得た各要素のランクが順序数なら、suc-ord と setUnion-ord により集めた値も順序数になる。順序数自身を扱う際には、mem-ord がその要素の順序数性を与える。

ここで使う添字は実際に小さいものである。各集合 x には小さな要素型 ⟪ x ⟫ と S への埋め込み ⟪ x ⟫↪ があり、∈ₛ⟪ x ⟫↪ m は表された集合が x に属することを示す。逆に、所属の証明から ∈-asFiber により、添字と、その表示が当の要素に等しいというパスを得られる。この二方向が、所属に沿う再帰と和集合を作る小さな族を結ぶ。

open import Cubical.HITs.CumulativeHierarchy.Base using ( sett )
open import Cubical.HITs.CumulativeHierarchy.Properties
  using ( ∈∈ₛ; ∈-asFiber; ⟪_⟫; ⟪_⟫↪; ∈ₛ⟪_⟫↪_ )

これで再帰ステップをそのまま数学的に読める。要素からなる小さな族を取り、各要素を再帰的に得たランクの後続に置き換え、その和集合を作る。次節ではこの構成を rankStep として述べ、計算パスを記録する。

open import Cubical.HITs.CumulativeHierarchy.Constructions
  using ( ⋃_; module InfinitySet )
open InfinitySet using ( sucV )

open hPropView 𝒮ᵥ

再帰

ステップは、x の各要素のランクの後続の和集合を取る。再帰呼び出しは要素の小さな型の上を走り、計算法則は定義的等式ではなくパスとして命題的に成り立つ。後の証明が使うのはこの形である。

再帰方程式は次を言う。集合 x のランクを求めるには、各要素のランクを求め、その後続の和集合を取る。形式的には、和を取る族は要素の小さな型 ⟪ x ⟫ で添字づけられるので、⋃ (sett ⟪ x ⟫ …) は正当な小さな和である。埋め込み ⟪ x ⟫↪ が添字 m を実際の集合 ⟪ x ⟫↪ m に変え、補助 mem がこの埋め込まれた集合が実際に x の要素であることの証明を供給する。これは再帰呼び出し rec が要求するものである。ステップの形に注意してほしい。rank を直接呼ぶのではなく、関数 rec を通して再帰的な値を受け取る。これが ∈-induction のステップとして使える理由である。

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 を直接簡約せず、このパスで書き換える。

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 が計算パスに沿う輸送込みでそれを和集合の中へ引き上げる。

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 自身について語るようにする。

  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 を輸送することで到達し、残るのはステップの和が順序数であることの証明だけである。

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 が順序数の小さな添字付き和の閉性を与える。仮定から結論への連鎖はこうである。要素のランクが順序数なら、集合のランクも順序数である。

    (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)) への所属を二つの場合に分ける。

rank-upper : (A β : S) → IsOrd β
           → ((y : S) → ⟨ y ∈ˢ A ⟩ → ⟨ rank y ∈ˢ β ⟩)
           → (x : S) → ⟨ x ∈ˢ rank A ⟩ → ⟨ x ∈ˢ β ⟩
rank-upper A β oβ bound x hx = rec₁ ((x ∈ˢ β) .snd)
  (λ { (m , hm) → ∈sucV-elim ((x ∈ˢ β) .snd) 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) は命題消去の内部で消費され、添字がデータとして取り出されることはない。

    (λ 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) ∈ˢ β を与える。したがってこの補題全体は帰納を一切使わない。計算法則で一度書き換え、和を分解し、順序数の推移性に後続を吸収させるだけである。

  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 での等式を返す。

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 そのものであり、上界の仮定は帰納仮定からその場で作られる。

  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 が従う。

        (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)。この二つは、ランクが各順序数と一致する順序数値尺度であることを示す。どちらの証明も正則性公理の上の所属帰納であり、本章は追加の仮定を一切使わない。これにより、所属に沿って狭義に増加する順序数値尺度と、対象が順序数である場合の不動点法則が得られる。