この章を読むか、対話型目次と依存グラフで別のルートを選べます。

対話型目次 · 依存グラフ

順序数述語は構成可能宇宙の章で IsOrd A = isTransV A × ((x : S) → ⟨ x ∈ˢ A ⟩ → isTransV x) と定義される。これは推移性の証明と「A の各要素がそれ自身推移的である」ことの証明との対である。両成分はともに命題であり、isPropIsOrd がそれを保証するので、IsOrd は構造を追加するデータではなく、命題値である。このモジュールは周囲の宇宙レベル ℓ を固定し、その上の累積階層の台 S の中で働く。

module L.Ordinal {ℓ : Level} where

順序数は、その要素も推移的である推移的集合である。本章では零、後続、和集合に関する閉性を示し、小さな族の順序数上界を構成し、有限数項の間および ω との所属関係を特徴付ける。

本章では、これらの閉性と上界構成を整えた後、有限順序数を扱う。零は順序数であり、順序数の後続は順序数であり、順序数の和集合は順序数であり、そして本章の主結果として、小さな順序数の族は必ず単一の順序数の下に収まる。最後の命題は、「小さな族の各要素がそれぞれ順序数上界を持つ」ことを「族全体が同一の順序数上界を共有する」ことへ変える。この形は後の分離、冪集合、再帰、反映、GCH の構成で使われる。

本章は順序数の比較を与えない。順序数が実際に線形に整列していることは事実であるが、その事実は構成的ではなく、ここでは必要でもない。公理が求めるのは共通の上界だけなので、本書は共通の上界を直接構成する。本章の閉性と上界の証明には古典論理の仮定は現れない。

ここで二組の道具が出会う。周囲の階層 V の側からは、後続 sucV、その所属の消去子、そして小さな族の和集合が来る。構成可能宇宙 L の側からは、空集合と小さな和集合に対する推移性の補題、および述語 IsOrd そのものが来る。本章の結果はすべて基礎となる集合についてであり、まだ構成可能性には触れないため、以下のどの主張にも排中律の仮定は現れない。

これらの証明で繰り返される型は、截断された証人の消去である。和集合への所属は、ある添字とある要素によって単に (merely) 証明されるだけなので、和のすべての要素に関する事実は rec₁ を用いて命題値の対象へと取り出す。そのため、各閉性補題は截断を消費する前に、isPropIsTransV z のような目標の命題を名指す。∥ A ∥₁ の消去が許されるのは、まさにこのような命題へのときだけだからである。

open import Cubical.Data.Nat.Order using ( _<_; ≤-suc; isProp≤ )

数項 # n は階層のフォン・ノイマン自然数である。# 0 は空集合、# (suc n) は # n の後続である。その極限 ω および各数項が ω に属することは、無限公理の構成から来る。本章の最終節では、数項の符号化の単射性を用いて、所属 z ∈ˢ (# n) から自然数の添字を読み戻す。

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 のようなここでの命題は ℓ の一つ上の階層に住み、それはのちの公理が量化を行う階層とちょうど一致する。

open hPropView 𝒮ᵥ

零と後続

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

証明書 ∅-ord は空虚に成立する二つの半分をまとめたものである。∅ の推移性には既証の補題 ∅-trans を使い、第二の半分については、x ∈ˢ ∅ を主張する任意の x を受け取る関数を与えるが、空集合の補題がその所属を空のホスト型の要素へと変換し、⊥*-rec がそこから任意の命題を証明する。存在し得ない要素は何の義務も課さない。

∅-ord : IsOrd ∅
∅-ord = ∅-trans
      , (λ x x∈∅ → ⊥₀-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 への所属であるため、命題性の証明 (y ∈ˢ sucV A) .snd を目標として渡す。

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 ((y ∈ˢ sucV A) .snd) x∈suc

第一分岐では x は A の要素なので、A の推移性を y ∈ˢ x と x ∈ˢ A に適用して y ∈ˢ A、したがって y ∈ˢ sucV A が得られる。第二分岐では x は A 自身と同一視されるので、y ∈ˢ x はそのパスに沿って直接 y ∈ˢ A へと輸送され、A に関する追加の事実は不要である。

    (λ 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 の命題性によるものである。

    (λ x≡A → subst isTransV (sym x≡A) Atr)

和集合と上界

順序数は、小さな添字付けられた族の和集合について閉じている。推移性は、推移的集合に対してすでに証明した閉性補題そのものである。第二の半分については、和集合の要素はある f x の内側にあり、仮定によりその族の元は順序数なので、その要素もまた推移的である。

族は小さな型 X の添字と写像 f : X → S で与えられるので、和集合 ⋃ (sett X f) は截断された列挙ではなく実際の関数から構成される集合である。その推移性は setUnion-trans から直接借り、仮定 hf 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

残りの義務については、union-family-out は z ∈ˢ ⋃ (sett X f) が、z がある f x に属することを単に (merely) 意味することを述べる。目標 isTransV z は命題なので rec₁ がこの截断を消去でき、各分岐では hf x .snd z hz がちょうど必要な証明書を与える。すなわち、順序数である族の元の要素は推移的である。

  memTr z z∈⋃ = rec₁ (isPropIsTransV z)
    (λ { (x , hz) → hf x .snd z hz }) (union-family-out X f z z∈⋃)

そして本章の成果物である。小さな順序数の族が与えられると、族のすべての元を含む単一の順序数が得られる。素朴に族の和を取るだけでは包含関係しか得られない。和集合はその要素の要素を吸収するのであって、要素そのものを吸収するわけではなく、しかもどの集合も自分自身を含まない。そこで一段の後続を挟み、後続の族の和を取る。結果は截断された存在ではなく実際の対として与えられ、利用者はこの上界を名指し、その段階を構成できる。

この結果は、上界 β を、その順序数証明と各添字に対する真の所属 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

構成は三行の数学である。f をその後続 g x = sucV (f x) に置き換え、その族の和 β を取り、いま証明した和の閉性を適用する。仮定は、後続の補題により各 sucV (f x) が順序数であることから満たされる。

  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 がそれを和集合の中へ引き上げ、さらに和集合自身の推移性が、この真の所属を、下流の閉性証明が使う包含関係へと格上げする。

  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 ブロックで構成される。

bound2 : (σ₁ σ₂ : S) → IsOrd σ₁ → IsOrd σ₂
       → Σ[ β ∶ S ] (IsOrd β × ⟨ σ₁ ∈ˢ β ⟩ × ⟨ σ₂ ∈ˢ β ⟩)
bound2 σ₁ σ₂ o₁ o₂ =
  r .fst , (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 は各索引に対応する順序数性の仮定を付ける。

  f : Lift {ℓ-zero} {ℓ} Bool → S
  f (lift true)  = σ₁
  f (lift false) = σ₂
  fo : (b : Lift {ℓ-zero} {ℓ} Bool) → IsOrd (f b)
  fo (lift true)  = o₁

これ以上新たに証明すべきものはない。r はこの二点族に対して一般の補題を適用したものであり、順序数の上界と各索引への所属をすでに備えている。結果に現れる二つの所属は、同じ証明を二つのブール値で具体化したものにすぎない。

  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 の各要素について主張していたことそのものである。

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) により、帰納法は各場合が一行で済む。空集合は最初の節により順序数であり、順序数の後続は二番目の節により順序数である。

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

累積階層のライブラリでは、ω はその要素が自然数で索引される集合として提示される。したがって ω への所属とは数値の索引を持つことにほかならない。補題 #-in-ω は各数項に対しその索引を与え、∈∈ₛ は得られた索引を所属の命題 ⟨ # k ∈ˢ ω ⟩ へと変換する。

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

次は数項の下向き閉性を、ω への所属という形で直接述べたものである。つまり # k のすべての要素は ω の要素である。k についての帰納法の底は空虚に成り立つ。空集合には何も属さないからである。後続の場合は sucV の消去子によって二つに分かれる。y がすでに # k に属する場合は帰納法の仮定を使い、y が # k 自身と等しい場合は前の補題から ω への所属が従う。

numeral-mem : (k : ℕ) (y : S) → ⟨ y ∈ˢ (# k) ⟩ → ⟨ y ∈ˢ ω ⟩
numeral-mem 0 y y∈ =
  ⊥₀-rec (∅-empty y (∈∈ₛ {a = y} {b = ∅} .fst y∈))
numeral-mem (suc k) y y∈ = ∈sucV-elim ((y ∈ˢ ω) .snd) y∈
  (λ y∈#k → numeral-mem k y y∈#k)

逆に、ω のすべての要素は順序数である。ω への所属は # k ≡ y なる自然数 k を単に (merely) 与えるだけである。目標の IsOrd y は isPropIsOrd により命題なので、截断をそれへ消去できる。パス # k ≡ y に沿って # k の順序数性が y へ輸送される。特定の索引が選ばれることはなく、截断の裏にどの索引が隠れていても議論は一様に通用する。

  (λ y≡#k → subst (λ w → ⟨ w ∈ˢ ω ⟩) (sym y≡#k) (#∈ω k))

ω-mem-ord : (y : S) → ⟨ y ∈ˢ ω ⟩ → IsOrd y
ω-mem-ord y y∈ω = 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 を ω の中に置く。この消去は命題値の目標への消去であり、それが截断を取り除いてよい根拠である。

ω-ord : IsOrd ω
ω-ord = trans-ω , (λ x x∈ω → ω-mem-ord x x∈ω .fst)
  where
  trans-ω : isTransV ω

ω の各要素 x に対して、ω-mem-ord x x∈ω は IsOrd x を証明する。その第一成分が、IsOrd ω の第二成分に必要な x の推移性である。二つの成分を合わせて IsOrd ω が得られる。

  trans-ω {x} {y} y∈x x∈ω = rec₁ ((y ∈ˢ ω) .snd)
    (λ { (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 が単に存在するということである。この主張が意図的に命題的切断の中に置かれている点に注意してほしい。この証明は切断から証人を選ばず、そのような分解が存在するという命題だけを使う。底の場合は空虚に成り立つ。空集合への所属は矛盾をもたらすからである。

∈#-elim : (n : ℕ) (z : S) → ⟨ z ∈ˢ (# n) ⟩
        → ∥ Σ[ m ∶ ℕ ] ((m < n) × (z ≡ # m)) ∥₁
∈#-elim 0    z h = ⊥₀-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 に変わる。

  (λ z∈#n → 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 = rec₁ isProp≤
  (λ { (m , p , e) → subst (_< b) (sym (#-inj′ e)) p })

最後の段階は截断そのものの消去である。ℕ 上の狭義の順序は isProp≤ により命題値を持つので、a < b へ消去するのは正当である。結論が必要とするのは、どこかの証明索引が機能することだけで、標準的なものである必要はない。

  (∈#-elim b (# a) h)

まとめ

零、後続、順序数からなる小さな族の和集合はいずれも順序数であり、boundingOrd は任意の小さな族を単一の順序数で抑える。この上界は、任意の小さな族に対する要素ごとの順序数上界を、一つの厳密な共通上界へまとめる。後の章ではこれらの結果を別々に使う。ZF 公理の証明は順序数上界で段階を集め、有限順序数の補題と ω-ord は無限公理や後の符号化で使われる。