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

対話型目次 · 依存グラフ

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

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

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

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

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

open import Cubical.HITs.PropositionalTruncation using ( isPropPropTrunc )

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

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

import Cubical.Induction.WellFounded as WF

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

open hPropView 𝒮ᵥ

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

証明は一つの関係を軸に回る。点ごとの包含である。これが両方向に成り立てば外延性により二つの順序数は等しく、一方向で失敗すれば排中律が切り詰められた反例の要素を与え、整礎帰納と推移性がその反例を狭義の比較へ変える。この節ではその関係とそのパッケージングを固定する。レベルの計算がすでに語っていることに注意してほしい。包含は 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Π (λ _ → (x ∈ˢ B) .snd))

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 → ⊥₀)
            → ∥ Σ[ a ∶ S ] (⟨ a ∈ˢ A ⟩ × (⟨ a ∈ˢ B ⟩ → ⊥₀)) ∥₁
¬⊆ᵇ→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 ⟩ → ⊥₀)) ∥₁
          , isPropPropTrunc
  decide : Dec ⟨ Witness ⟩ → ⟨ Witness ⟩
  decide (yes wit) = wit
  decide (no ¬wit) = ⊥₀-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 (FOL.Semantics.decideMembership 𝒮ᵥ lem x B)
      where
      at : Dec ⟨ x ∈ˢ B ⟩ → ⟨ x ∈ˢ B ⟩

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

      at (yes x∈B) = x∈B
      at (no ¬x∈B) = ⊥₀-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 ⟩ → ⊥₀)) → ⟨ 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)) = ⊥₀-rec (¬b∈A b∈A)

      fromA : Σ[ a ∶ S ] (⟨ a ∈ˢ A ⟩ × (⟨ a ∈ˢ B ⟩ → ⊥₀)) → ⟨ 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)       = ⊥₀-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 が失敗する場合は、その失敗の切り詰められた証人を rec₁ で消去する。これが正当なのは、目標 ⟨ A ∈ˢ B ⟩ が命題であり、その命題性が所属 hProp の第二成分から供給されるからである。結果は左の答え A ∈ˢ B である。B ⊆ᵇ A の失敗から A が B に属すると結論するのがこの分岐である。

      decide : Dec (A ⊆ᵇ B) → Dec (B ⊆ᵇ A) → Tri A B
      decide (yes A⊆B) (yes B⊆A) = inr (inl (ext-⊆ᵇ A⊆B B⊆A))
      decide (yes A⊆B) (no ¬B⊆A) =
        inl (rec₁ ((A ∈ˢ B) .snd) fromB (¬⊆ᵇ→witness B A ¬B⊆A))

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

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

まとめ

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

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