順序数は所属によって線形に順序付けられる

この章を読むか、読書案内と依存マップで別のルートを選べます。

読書案内 · 依存マップ

任意の二つの順序数は、一方が他方に属するか、両者が等しいかのどちらかです。本章では、この比較に必要な古典的段階を切り分け、なぜ明示的な仮定が必要かを説明します。

これまでの順序数に関する命題はすべて閉包性でした。零は順序数であり、後続も和も順序数であり、上限も存在する。閉包の主張は構築に関わるもので、何かを判定する必要はありません。三分性は判定を要求します。互いに何の関係も仮定されていない二つの順序数を与えられ、三つの場合のどれが成り立つかを答えなければならず、本章では、この判定を明示的な排中律のパラメータから得ます。そこで本章は排中律をモジュールパラメータとして取り、基礎の段階で固定されたレベルごとのパッケージングを用います。ord-tri を使うモジュールは、このパラメータを明示的に受け取ります。

周囲の階層からの二つの材料が、証明を教科書の版より短くします。正則性公理は整礎帰納を与え、二つの引数に対して一度ずつ、計二回使われます。外延性により、相互包含は等号そのものなので、等しい場合を別途扱う必要はありません。排中律は二方向の包含を判定し、さらに包含の失敗を切り詰められた反例へ変える際に必要な所属命題も判定します。

本章はただ一つの古典的仮定の下で進みます。それはモジュールパラメータとして一度だけ宣言される LEM (ℓ-suc ℓ) の実例です。基礎の章で確めた形を思い出してください。各命題 P : hProp (ℓ-suc ℓ) に対し、⟨ P ⟩ の証明か、あるいは ⟨ P ⟩ を空型へ写す反証を返します。このレベルは ⊆ᵇ-prop A B : hProp (ℓ-suc ℓ) と、反例の議論で判定する所属命題に一致します。仮定を明示的なモジュールパラメータとして保つことで、このモジュールを使うたびに古典的入力が記録されます。

{-# OPTIONS --cubical --safe --guardedness #-}

open import Base.Prelude
open import Base.Classical using ( LEM )

module L.Ordinal.Linear {ℓ : Level} (lem : LEM (ℓ-suc ℓ)) where

証明は対象言語を経由せず、周囲の階層 V の中で直接行われます。台と構造の所属 ∈ˢ は 𝒮ᵥ の上にパッケージされた ZF 構造から来るので、⟨ x ∈ˢ A ⟩ は hProp 真理値の基礎命題です。V の二つの原理が数学的な重みを担います。extensionalV は所属関係の双条件の族を等号のパスへ変え、regularityV は所属関係を整礎にしてその上の帰納を可能にします。L 側のもう一つの輸入 mem-ord は再帰呼び出しのたびに効きます。順序数の任意の要素がそれ自身順序数であることを示すもので、これが帰納仮説を下の層で使えるようにする理由です。

open import FOL.ZFStructure using ( module hPropStructure )
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ; extensionalV; regularityV )
open import L.Constructible {ℓ} using ( IsOrd )
open import L.Ordinal {ℓ} using ( mem-ord )

open import Cubical.Data.Sum using ( _⊎_; inl; inr )

判定手続きは三つの場合のどれが成り立つかを返すので、返り値の型は三分岐の直和で組み立てます。左に所属、中央に等号、右に所属です。さらに必要なのは双条件からパスへの変換で、外延性の議論が台の各点に適用します。空型は全体を通して反証の役割を果たします。命題を反証するとは、それを元を持たない型へ写すことです。

open import Cubical.Functions.Logic using ( ⇔toPath )
import Cubical.Data.Empty as Empty
import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∣_∣₁; ∥_∥₁ )
import Cubical.Induction.WellFounded as WF

最後に、ファイル全体に対して二つの約束を開きます。hProp 上の直接の演算が所属の記述で使う命題結合子を供給し、構造の語彙は S を台、∈ˢ をその所属として固定します。これでコードは論理の配管ではなく集合論として読めます。この設定に新しい数学はありません。前の章々の順序数が階層 V と出会うインターフェースです。

open hPropStructure 𝒮ᵥ

包含と、その失敗を示す証人

証明は一つの関係を軸に回ります。点ごとの包含です。これが両方向に成り立てば外延性により二つの順序数は等しく、一方向で失敗すれば排中律が切り詰められた反例の要素を与え、整礎帰納と推移性がその反例を狭義の比較へ変えます。この節ではその関係とそのパッケージングを固定します。レベルの計算がすでに語っていることに注意してください。包含は Type (ℓ-suc ℓ) に住み、これは与えられた排中律の実例がまさに判定できる場所です。

A が B に含まれることはここでは原始概念ではなく定義された概念です。A の各要素 x は、構造の意味で、B の要素でなければならない。各所属 x ∈ˢ A は hProp の命題なので、この定義は台 S とレベル ℓ の命題を量化し、関係全体を Type (ℓ-suc ℓ) に置きます。対応する hProp のパッケージングは命題性の証明を添えます。命題への依存関数は再び命題であり、これを入れ子になった二つの関数型にそれぞれ適用します。これが重要なのは、排中律が hProp ごとに判定されるからであり、証明が lem に渡すのはまさにこのパッケージされた命題です。

_⊆ᵇ_ : S → S → Type (ℓ-suc ℓ)
A ⊆ᵇ B = (x : S) → ⟨ x ∈ˢ A ⟩ → ⟨ x ∈ˢ B ⟩

⊆ᵇ-prop : (A B : S) → hProp (ℓ-suc ℓ)
⊆ᵇ-prop A B = (A ⊆ᵇ B) , isPropΠ (λ x → isPropΠ (λ _ → snd (x ∈ˢ B)))

ext-⊆ᵇ : {A B : S} → A ⊆ᵇ B → B ⊆ᵇ A → A ≡ B

三分性の等号の場合は、階層の外延性からただで手に入ります。両方向の包含が与えられれば、台の各点 x は ⟨ x ∈ˢ A ⟩ と ⟨ x ∈ˢ B ⟩ の間の双条件を与え、⇔toPath がそれをパスに変え、extensionalV がパスの族を等式 A ≡ B に組み立てます。ここには古典的な入力はまったく使われません。外延性は V 自身の定理だからです。

ext-⊆ᵇ {A} {B} s₁ s₂ = extensionalV (λ x → ⇔toPath (s₁ x) (s₂ x))

ここが本当に古典的な一段です。包含の失敗から出発して、証明はそれを証人する要素を必要としますが、「B の要素がすべて A に含まれるわけではない」から「ある要素は含まれない」への移行は構成的ではありません。排中律がこの存在文を直接判定します。そのような証人が存在しないなら、所属を一つずつ判定しながら B の各要素がやはり A に含まれることを示せ、これは仮定された失敗に矛盾します。得られる証人は命題切り詰めされたままですが、それで十分です。三分性の証明がこれにすることは、メンバーシップ命題への消去だけだからです。

この主張は条件文です。包含 A ⊆ᵇ B が反証可能なら、切り詰められた証人、すなわち a ∉ B を満たす A の要素 a が存在する。結論は選ばれた対ではなく、意図的に ∥ ∥₁ の下の存在主張になっています。最初の古典的な動作は、切り詰められた存在文 Witness 自体を判定することです。レベルの計算に注意してください。証人の文は ℓ-suc ℓ の hProp であり、モジュールの lem が適用できるちょうどその場所にあるので、持ち上げは不要です。肯定的な分岐では証人はすでに手にあり、興味があるのは否定的な分岐です。

¬⊆ᵇ→witness : (A B : S) → (A ⊆ᵇ B → Empty.⊥)
            → ∥ Σ[ a ∈ S ] (⟨ a ∈ˢ A ⟩ × (⟨ a ∈ˢ B ⟩ → Empty.⊥)) ∥₁
¬⊆ᵇ→witness A B ¬sub = decide (lem Witness)
  where
  Witness : hProp (ℓ-suc ℓ)

Witness が反証可能だとします。すると包含の反証自身も反証できます。任意の x に対して所属 x ∈ˢ B を独立に判定し、否定的な分岐では要素 x を x ∈ˢ A と x ∈ˢ B の反証とともに Witness の元へ組み立てます。これは与えられた反証に矛盾します。したがって包含は結局成り立ち、それを仮定された包含の反証に渡せば空型が得られます。これはまさに上で述べたパターンです。Witness への一度の大域判定と、各 x ∈ˢ B への点ごとの判定が、「証人は存在しない」を「包含は成り立つ」へ変えます。

  Witness = ∥ Σ[ a ∈ S ] (⟨ a ∈ˢ A ⟩ × (⟨ a ∈ˢ B ⟩ → Empty.⊥)) ∥₁
          , PT.isPropPropTrunc
  decide : ⟨ Witness ⟩ ⊎ (⟨ Witness ⟩ → Empty.⊥) → ⟨ Witness ⟩
  decide (inl wit)  = wit
  decide (inr ¬wit) = Empty.rec (¬sub sub)

点ごとの判定に少し立ち止まる価値があります。切り詰められた結論が切り詰められた入力をどう受け入れるかを示しているからです。x ∈ˢ A から x ∈ˢ B を証明するには、その一つの所属を lem で判定します。成り立てば終わりです。失敗するなら、x ∈ˢ B の反証は x ∈ˢ A と x とともにまさに証人のデータであり、その切り詰め ∣ x , (x∈A , ¬x∈B) ∣₁ は Witness の元となり、否定分岐の仮定に矛盾します。

    where
    sub : A ⊆ᵇ B
    sub x x∈A = at (lem (x ∈ˢ B))
      where
      at : ⟨ x ∈ˢ B ⟩ ⊎ (⟨ x ∈ˢ B ⟩ → Empty.⊥) → ⟨ x ∈ˢ B ⟩

部品を組み立てます。Witness に対する外側の判定は、肯定的な場合は切り詰められた証人を直接返し、否定的な場合は仮定された包含の失敗から矛盾を導きます。補題 ¬⊆ᵇ→witness はこれで三分性の議論の両方向で使えますが、切り詰められた証人以上のことは決して約束しません。切り詰めを明示的に保つことが後の消去を正当化する理由です。命題切り詰めは命題へしか消去できず、次の節で消去される所属の文はまさに命題だからです。

      at (inl x∈B)  = x∈B
      at (inr ¬x∈B) = Empty.rec (¬wit ∣ x , (x∈A , ¬x∈B) ∣₁)

順序数の三分性

主定理のための準備はすべて整いました。比較は三分岐の直和として述べられます。A が B の要素であるか、両者がパスによって等しいか、B が A の要素であるか。証明は整礎帰納を引数ごとに一度ずつ、計二回実行し、葉のところでどちらの順序数の要素にも再帰できるようにします。二つの包含 A ⊆ᵇ B と B ⊆ᵇ A は各葉で排中律によって判定され、残りは前節が担いました。場合分けを通して読者が手にしておくべき向きの対応は次のとおりです。B ⊆ᵇ A の失敗は B に属し A に属さない要素を生み、結論は A ∈ˢ B です。A ⊆ᵇ B の失敗は A に属し B に属さない要素を生み、結論は B ∈ˢ A です。

主張 Tri A B は三つの答えを一つの型にまとめ、入れ子になった直和で組み立てます。外側の二つの場合は構造の意味での所属であり、中央の場合は等号のパスです。この型は Type (ℓ-suc ℓ) に住み、これは内部の所属命題が要求するレベルです。

Tri : S → S → Type (ℓ-suc ℓ)
Tri A B = ⟨ A ∈ˢ B ⟩ ⊎ ((A ≡ B) ⊎ ⟨ B ∈ˢ A ⟩)

ord-tri : (A : S) → IsOrd A → (B : S) → IsOrd B → Tri A B
ord-tri = WF.WFI.induction regularityV {P = P} stepA
  where

定理の形は、正則性公理が供給する整礎帰納です。証明される述語 P A は、比較される任意の順序数 B に対して A が正しく振る舞うこと、二つの順序数性の証明を仮定として取ることを述べます。これにより正則性は第一引数上の帰納を与えます。P A を証明するには、A の各要素 A' について P A' を証明すれば十分です。これは入れ子になった二つの帰納の第一で、第二の B 上の帰納はステップの中に現れます。

  P : S → Type (ℓ-suc ℓ)
  P A = IsOrd A → (B : S) → IsOrd B → Tri A B

  stepA : (A : S) → (∀ A' → ⟨ A' ∈ˢ A ⟩ → P A') → P A
  stepA A IHA ordA =
    WF.WFI.induction regularityV {P = λ B → IsOrd B → Tri A B} stepB

外側のステップは A の各要素に対する帰納仮説を受け取り、すぐに第二の整礎帰納を実行します。今度は B 上で、述語は λ B → IsOrd B → Tri A B です。内側の帰納ステップでは、二つの包含がパッケージされた命題 ⊆ᵇ-prop A B と ⊆ᵇ-prop B A に lem を適用して判定されます。この二つの判定が古典的な場合分けを開始します。前の補題も排中律を使い、それぞれの包含の失敗から切り詰められた反例を得ます。

    where
    stepB : (B : S) → (∀ B' → ⟨ B' ∈ˢ B ⟩ → IsOrd B' → Tri A B')
          → IsOrd B → Tri A B
    stepB B IHB ordB = decide (lem (⊆ᵇ-prop A B)) (lem (⊆ᵇ-prop B A))
      where

最初の失敗の場合は B ⊆ᵇ A が失敗すると仮定し、B のうち A に属さない要素 b が単に存在するとしか分かりません。補題 fromB は、そのような明示的な対が一つあれば何が得られるかを示します。b は順序数 B の要素なので、mem-ord が b 自身も順序数であることを証明し、内側の帰納仮説 IHB が A と b を比較できます。その第一の結果は A ∈ˢ b です。順序数の推移性、すなわち IsOrd B の第一成分が、これを b ∈ˢ B を経て A ∈ˢ B まで持ち上げます。

      fromB : Σ[ b ∈ S ] (⟨ b ∈ˢ B ⟩ × (⟨ b ∈ˢ A ⟩ → Empty.⊥)) → ⟨ A ∈ˢ B ⟩
      fromB (b , (b∈B , ¬b∈A)) = at (IHB b b∈B (mem-ord {A = B} ordB b b∈B))
        where
        at : Tri A b → ⟨ A ∈ˢ B ⟩
        at (inl A∈b)       = ordB .fst A∈b b∈B

A と b の比較の残り二つの結果を順に処理します。A ≡ b がパスで与えられれば、そのパスに沿って b ∈ˢ B を逆方向へ輸送する、すなわち subst に sym を組み合わせる操作により A ∈ˢ B が得られます。また b ∈ˢ A なら、b を A の外として選んだことに直接矛盾します。三つの分岐はすべて同じ命題 ⟨ A ∈ˢ B ⟩ に着地します。これこそ、切り詰められた存在証人でここでは十分な理由です。切り詰められた対は命題へ消去されるのであって、データへ消去されることはありません。

        at (inr (inl A≡b)) = subst (λ w → ⟨ w ∈ˢ B ⟩) (sym A≡b) b∈B
        at (inr (inr b∈A)) = Empty.rec (¬b∈A b∈A)

      fromA : Σ[ a ∈ S ] (⟨ a ∈ˢ A ⟩ × (⟨ a ∈ˢ B ⟩ → Empty.⊥)) → ⟨ B ∈ˢ A ⟩
      fromA (a , (a∈A , ¬a∈B)) =
        at (IHA a a∈A (mem-ord {A = A} ordA a a∈A) B ordB)

鏡像の補題 fromA はもう一つの失敗を扱います。A ⊆ᵇ B が失敗すれば、A のある要素 a が B の外にあります。今度は外側の帰納仮説が仕事をします。A の要素を比較するもので、a で適用されます。a が結局 B に属するなら a の選択に矛盾し、a ≡ B なら輸送により B ∈ˢ A が得られ、B ∈ˢ a なら A の推移性がこれを a ∈ˢ A を経て持ち上げます。鏡像が持ち込む非対称に注意してください。等号の分岐はパスに沿って a ∈ˢ A を輸送するのであって逆向きにはしない、今回は比較される組の向きが逆だからです。

        where
        at : Tri a B → ⟨ B ∈ˢ A ⟩
        at (inl a∈B)       = Empty.rec (¬a∈B a∈B)
        at (inr (inl a≡B)) = subst (λ w → ⟨ w ∈ˢ A ⟩) a≡B a∈A
        at (inr (inr B∈a)) = ordA .fst B∈a a∈A

二つの変換器が手にあれば、四つの判定の組み合わせは三つの答えに整理されます。両方の包含が成り立てば、相互包含は等号であり、中央の答えが返ります。A ⊆ᵇ B が成り立ち B ⊆ᵇ A が失敗する場合は、その失敗の切り詰められた証人を PT.rec で消去します。これが正当なのは、目標 ⟨ A ∈ˢ B ⟩ が命題であり、その命題性が所属 hProp の第二成分から供給されるからです。結果は左の答え A ∈ˢ B です。B ⊆ᵇ A の失敗から A が B に属すると結論するのがこの分岐です。

      decide : (A ⊆ᵇ B) ⊎ ((A ⊆ᵇ B) → Empty.⊥)
             → (B ⊆ᵇ A) ⊎ ((B ⊆ᵇ A) → Empty.⊥) → Tri A B
      decide (inl A⊆B) (inl B⊆A) = inr (inl (ext-⊆ᵇ A⊆B B⊆A))
      decide (inl A⊆B) (inr ¬B⊆A) =
        inl (PT.rec (snd (A ∈ˢ B)) fromB (¬⊆ᵇ→witness B A ¬B⊆A))

最後の組み合わせは、二番目の判定がどうであれ A ⊆ᵇ B の失敗を扱い、鏡像の変換器が B ∈ˢ A を届けます。上の二つの場合と合わせて、各葉は今や Tri A B の元を返し、二重の帰納は閉じて、ord-tri は任意の順序数 A と B についての定理として立ちます。段階順序や基数に関する後の章、たとえば L.GCH.CardinalSquareLaw は、これを比較の原始部品として使います。

      decide (inr ¬A⊆B) _ =
        inr (inr (PT.rec (snd (B ∈ˢ A)) fromA (¬⊆ᵇ→witness A B ¬A⊆B)))

まとめ

階層の所属について既に得られた非反射性と IsOrd に含まれる推移性に加えて、ord-tri が任意の二つの順序数の比較を与えます。これらの比較法則は、後の段階の単調性と基数の議論に必要な順序論的基礎となります。

ord-tri は任意の二つの順序数を比較し、本書はそのために排中律の実例を一つ供給します。これはモジュールパラメータとして与えられます。これこそ基盤の部分が監査可能にするために築いた境界です。何一つ postulate されず、ord-tri を使うには、このモジュールの排中律パラメータを与える必要があります。続く章々は、この比較をそれが必要とされた問い、すなわちどの順序数が構成可能階層のどの段階に現れるか、に用います。