Bedrockvon Neumann ランク
この章を読むか、読書案内と依存マップで別のルートを選べます。
読書案内 · 依存マップ集合のランクは、その各要素のランクの後続を要素にわたって合わせた和集合です。記号で言えば、計算定理 rank-compute が rank x を rankStep x (λ y _ → rank y) と同一視します。本章で証明するのは四つの事実です。rank-mono はランクが所属に沿って狭義単調に増加すること、rank-ord はランクが常に順序数であること、rank-upper はランクがある順序数に含まれるという条件付きの結論を与えること、そして rank-fix はランクが順序数を固定することを言います。
ここでは外部の順序数の型は何も要りません。ランクは階層自身の中に値を取り、再帰は整礎な所属関係の上を走ります。これは正則性公理が直接保証するものです。したがって本章の各定理には排中律のパラメータがありません。
ランクは累積階層 V ℓ の台 S の中で直接定義されます。所属 x ∈ˢ y は命題値をとり、正則性によりこの所属関係は整礎です。したがって所属帰納 ∈-induction は、各要素ですでに定義された値から、現在の集合に対する S の値を定義できます。
{-# 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 がその要素の順序数性を与えます。
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 により、添字と、その表示が当の要素に等しいというパスを得られます。この二方向が、所属に沿う再帰と和集合を作る小さな族を結びます。
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 として述べ、計算パスを記録します。
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 のステップとして使える理由です。
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 = 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) は命題消去の内部で消費され、添字がデータとして取り出されることはありません。
(λ 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)。この二つは、ランクが各順序数と一致する順序数値尺度であることを示します。どちらの証明も正則性公理の上の所属帰納であり、本章は追加の仮定を一切使いません。これにより、所属に沿って狭義に増加する順序数値尺度と、対象が順序数である場合の不動点法則が得られます。