最小の構成可能段階の添字

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

各構成可能集合 x は、少なくとも一つの順序数 α に対する Lset α に属します。本章は、この単なる存在から標準的な上界、すなわち x を含む最小段階の順序数添字を得ます。まず、より一般的な問題を解きます。順序数上の任意の hProp 値の性質 P について、整礎的な降下が最小の証人を見つけ、順序数の三分法がその一意性を示します。

降下は P を満たす任意の順序数から始まります。α において、より小さい β ∈ α も P を満たすかを問います。肯定なら β における帰納法の結果を使い、否定なら α の最小性が得られます。所属に関する帰納法により、この定義は整礎的です。「より小さい証人が存在する」という主張と最初の証人はいずれも命題的に切り捨てられていますが、LeastOrd P 自身が命題なので、それぞれの切り捨てをこの完全なパッケージへ消去できます。

P σ を x ∈ Lset σ に特殊化すると stage x hx が得られます。付随する定理は、この添字が順序数で、その段階が x を含み、より小さい順序数の段階は x を含まないことを述べます。排中律を使うのは、より小さい証人の存在を判定するときと、二つの候補順序数を比較するときだけです。

宇宙レベル ℓ を固定し、レベル ℓ-suc ℓ における排中律を仮定します。この仮定には二つの異なる数学的用途があります。ord-tri は候補の順序数を比較し、降下は「より小さい候補が存在する」という hProp を判定します。

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

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

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

所属関係は、順序数上の狭義順序と、その整礎帰納の原理の両方を与えます。構成可能性からは、述語 IsOrd、段階族 Lset、そして x がある順序数添字の段階に現れるという主張 isL x を得ます。したがって同じ所属関係が候補添字の間の降下を制御し、特殊化後には x の段階への所属を表します。

open import FOL.ZFStructure using ( module hPropStructure )
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ; ∈-induction )
open import L.Constructible {ℓ} using ( IsOrd; isPropIsOrd; Lset; isL )
open import L.Ordinal.Linear {ℓ} lem using ( ord-tri )

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

「より小さい証人が存在する」という主張は、命題的に切り捨てられた存在で表します。これは存在だけを記録し、選ばれた β を取り出しません。消去子 PT.rec がこの証拠を使えるのは対象が命題の場合だけであり、下の一意性の証明が LeastOrd P についてまさにそれを示します。積と依存関数型は命題性を保つので、固定した順序数添字に付随する証拠も一意になります。

import Cubical.Data.Empty as Empty
import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∣_∣₁; ∥_∥₁ )
open import Cubical.Functions.Logic using ( ∃[∶]-syntax )
open import Cubical.Data.Sigma using ( Σ≡Prop )

性質 P は Ω、すなわち hProp の型への写像です。したがって ⟨ P α ⟩ は α における基礎の命題であり、snd (P α) はその任意の二つの証人が一致することを示します。順序数添字の等号を最小証人のパッケージ全体の等号へ持ち上げるとき、この命題性を使います。

open import Cubical.Foundations.HLevels using ( isProp×; isPropΠ )

open hPropStructure 𝒮ᵥ

性質を満たす最小の順序数

順序数の性質 P に対して、LeastOrd P は P を満たす順序数 α と、それより小さい順序数は P を満たさないという証明とを組にします。この定義が扱うのは順序数の添字そのものであり、後で P σ = (x ∈ Lset σ) と特殊化して初めて、その添字は構成可能段階の添字になります。

一意性は、性質が hProp の値を取るという事実を用います。二人の候補は三分性で比較され、どちらの厳密な向きも相手の最小性によって反駁され、残りの成分はすべて命題です。したがって順序数として等しければ、パッケージ全体としても等しいのです。

最小性は反駁として述べられます。isLeastOrd α とは、任意の集合 γ について、γ が P を満たす順序数でかつ γ ∈ α であるような状況は起こりえない、という主張です。ここで背理的な形の最小性が適切なのは、順序数の厳密な順序が所属を通して読み取られるからです。返すべき「より小さい順序数」の値はなく、導出すべきは不可能な状況だけです。パッケージ全体 LeastOrd は、順序数、その順序数性、そこでの P の証明、そしてこの最小性の条項をひとまとめにします。

module _ (P : S → hProp (ℓ-suc ℓ)) where

  isLeastOrd : S → Type (ℓ-suc ℓ)
  isLeastOrd α = (γ : S) → IsOrd γ → ⟨ P γ ⟩ → ⟨ γ ∈ˢ α ⟩ → Empty.⊥

  LeastOrd : Type (ℓ-suc ℓ)
  LeastOrd = Σ[ α ∈ S ] (IsOrd α × ⟨ P α ⟩ × isLeastOrd α)

このようなパッケージが等しいことを示すには、まず順序数の添字を比較します。三分性は α ∈ α′、α = α′、α′ ∈ α の三つの場合を届けます。方針は、厳密な二つの場合を背理的に消去し、等しい場合を残すことです。decide はこの三分法の結果をパス α ≡ α′ に変える関数です。重要なのは、この議論が示すのは添字の等しさだけだということです。パッケージは添字上の依存対なので、添字の等しさだけからパッケージの等しさは得られません。

  isPropLeastOrd : isProp LeastOrd
  isPropLeastOrd (α , ordα , pα , leastα) (α' , ordα' , pα' , leastα') =
    Σ≡Prop propRest α≡α'
    where
    decide : (⟨ α ∈ˢ α' ⟩ ⊎ ((α ≡ α') ⊎ ⟨ α' ∈ˢ α ⟩)) → α ≡ α'

それぞれの厳密な場合は最小性と矛盾しますが、それは相手側の候補の最小性との矛盾です。α ∈ α′ なら、α は α′ より厳密に下にあり P を満たす順序数であり、leastα' が反駁するのはまさにこれです。α′ ∈ α の場合は leastα を用いて対称です。真ん中の場合がパスそのものです。ord-tri の判定を decide に流し込めばパス α≡α' が得られます。ここまでに P について使った仮定は、その値が命題であること以外にありません。

    decide (inl α∈α')       = Empty.rec (leastα' α ordα pα α∈α')
    decide (inr (inl e))    = e
    decide (inr (inr α'∈α)) = Empty.rec (leastα α' ordα' pα' α'∈α)
    α≡α' : α ≡ α'
    α≡α' = decide (ord-tri α ordα α' ordα')

残るは、添字のパスをパッケージのパスへ引き上げることであり、ここでは依存する残りの命題性を使います。添字とともに変わる成分は IsOrd β × ⟨ P β ⟩ × isLeastOrd β です。IsOrd β は構成可能の章により命題であり、⟨ P β ⟩ は P が hProp 値であることから命題であり、isLeastOrd β は空型への関数型なので isPropΠ の繰り返しで命題です。よって propRest β が残りの全体の命題性を証明し、Σ≡Prop が基礎のパスを、求めるパッケージの相等へと変えます。添字が一致すれば、依存する残りは一致しないようがないのです。

    propRest : (β : S) → isProp (IsOrd β × ⟨ P β ⟩ × isLeastOrd β)
    propRest β = isProp× (isPropIsOrd β)
      (isProp× (snd (P β))
        (isPropΠ λ _ → isPropΠ λ _ → isPropΠ λ _ → isPropΠ λ _ → Empty.isProp⊥))

最小の順序数への降下

P を満たす任意の順序数から始め、leastOrdBelow は、それより小さく P を満たす順序数があれば再帰的にそこへ降ります。所属に関する帰納法は、真に小さい順序数での結果から現在の結果を定め、P を満たす最小の順序数を与えます。この時点ではまだ構成可能段階への特殊化は行いません。

結果が命題であるため、出発点の順序数は切り詰められた形で与えてよく、それこそが呼び出し側の実際の形です。呼び出し側は、適切な順序数が存在することを知っているだけで、ひとつを選んではいません。

降下は所属に関する整礎帰納として構成されます。これが階層の章の原理 ∈-induction です。そのステップは、順序数 α、その順序数性、α での P の証明、そしてすべての厳密に小さい要素 β に対して有効な帰納法の仮定を受け取ります。β が再び P を満たす順序数であれば、β から帰納を始めて得られる大域的に最小の P の証人がすでに手にある、というものです。ステップの仕事はただひとつ、α において降下を続けるか、到着したかを判定することです。

  leastOrdBelow : (α : S) → IsOrd α → ⟨ P α ⟩ → LeastOrd
  leastOrdBelow = ∈-induction step
    where
    step : (α : S) → (∀ β → ⟨ β ∈ˢ α ⟩ → IsOrd β → ⟨ P β ⟩ → LeastOrd)
         → IsOrd α → ⟨ P α ⟩ → LeastOrd

判定すべき問いは Smaller です。すなわち、β ∈ α であり、順序数であり、P を満たすような β が単に存在するかどうかで、各条件は論理積でひとつの hProp にまとめられます。ここで重要な点が二つあります。第一に、この存在文は切り詰められていることです。Smaller は選ばれた β を持たず、存在することの主張だけを運びます。第二に、レベル ℓ-suc ℓ における排中律が lem を通してこの問いを丸ごと判定し、切り詰めの要素か、反駁かのどちらかを届けることです。これこそ古典的な仮定が降下に入り込む場所です。

    step α IH ordα pα = decide (lem Smaller)
      where
      Smaller : hProp (ℓ-suc ℓ)
      Smaller = ∃[ β ∶ S ] ((β ∈ˢ α) ⊓ ((IsOrd β , isPropIsOrd β) ⊓ P β))
      decide : (⟨ Smaller ⟩ ⊎ (⟨ Smaller ⟩ → Empty.⊥)) → LeastOrd

判定の二つの分岐は、どちらも答えを直接組み立てます。肯定的な分岐では、切り詰められた証人をデータとして分解することはできませんが、PT.rec はそれを任意の命題へ消去でき、LeastOrd はまさに命題です。そこで証人は、選ばれることなく、β における帰納法の仮定が与える大域的に最小のパッケージへと変換されます。否定的な分岐では、より小さい証人はそもそも存在しないので、α 自身が最小です。再帰は ∈-induction の管理された帰納法の仮定を通してのみ起こります。。

      decide (inl ∃β) = PT.rec isPropLeastOrd
        (λ { (β , (β∈α , (ordβ , pβ))) → IH β β∈α ordβ pβ }) ∃β
      decide (inr ¬∃β) = α , ordα , pα , leastProof
        where
        leastProof : isLeastOrd α

否定的な分岐の最小性の条項で、反駁が働きます。α より下で P を満たす順序数 γ が与えられれば、証人 (γ , γ∈α , ordγ , pγ) は、まさに否定されたはずの切り詰め Smaller に梱包され、それに ¬∃β を適用して求める矛盾が得られます。最後に leastOrd が、呼び出し側が実際に持つ形を扱います。P を満たす順序数が単に存在する、という形です。ここでも LeastOrd への消去は、前節で証明された命題性によって許されます。こうして切り詰められた存在は、切り捨てを任意のデータ型へ消去することなく、正準な最小の添字へと洗練されるのです。

        leastProof γ ordγ pγ γ∈α = ¬∃β ∣ γ , (γ∈α , (ordγ , pγ)) ∣₁

  leastOrd : ∥ (Σ[ α ∈ S ] (IsOrd α × ⟨ P α ⟩)) ∥₁ → LeastOrd
  leastOrd = PT.rec isPropLeastOrd
    (λ { (α , (ordα , pα)) → leastOrdBelow α ordα pα })

段階の添字を返す関数

P σ = (x ∈ Lset σ) とすると、降下は x を含む段階 Lset α の最小の順序数添字 α を返します。関数 stage が α を選び、stage-ord はそれが順序数であることを、stage-mem と stage-earliest はその添字と対応する段階との関係を示します。

この添字は再帰的な構成そのものではなく、三つの安定した事実を通して与えられます。すなわち、順序数であり、その段階が x を含み、その性質をもつ順序数添字の中で最小です。stage を opaque とすることで、この抽象化の境界を保ちます。

構成可能性の証明書 ⟨ isL x ⟩ は、leastOrd が期待する入力の形そのものです。構成可能の章でのクラスの定義により、isL x の要素とは、順序数 σ とその順序数性と所属 x ∈ˢ Lset σ の対を単に切り詰めたものです。したがって性質 λ σ → x ∈ˢ Lset σ は降下の仮定を満たし、theEarliest はこの性質に leastOrd を適用します。したがって構成可能性は、最小段階の添字を得るために必要な切り捨てられた存在の前提をちょうど与えます。

theEarliest : (x : S) → ⟨ isL x ⟩ → LeastOrd (λ σ → x ∈ˢ Lset σ)
theEarliest x = leastOrd (λ σ → x ∈ˢ Lset σ)

opaque
  stage : (x : S) → ⟨ isL x ⟩ → S
  stage x p = theEarliest x p .fst

パッケージ theEarliest x p は、最小の添字と三つの証明を含みます。関数 stage は添字を射影し、その再帰的構成を不透明に保つので、後の議論は順序数性、段階への所属、最小性を使います。これは構成可能集合とその証人から順序数を返す関数であり、宇宙レベルでも階数関数でもありません。

opaque
  unfolding stage
  stage-ord : (x : S) (p : ⟨ isL x ⟩) → IsOrd (stage x p)
  stage-ord x p = theEarliest x p .snd .fst

  stage-mem : (x : S) (p : ⟨ isL x ⟩) → ⟨ x ∈ˢ Lset (stage x p) ⟩

三つの定理がインターフェースであり、どれもパッケージの射影です。stage-ord は選ばれた添字が順序数であることを述べ、したがって後に他の添字と比較できます。stage-mem は x を段階 Lset (stage x p) に属させます。これが降下によって示される所属の事実です。stage-earliest は最小性の条項そのものを取り戻します。より小さい順序数 σ で x ∈ˢ Lset σ となるものはありません。合わせて、これらは stage x p が章の冒頭で約束された最小の添字にちょうど等しいことを、再帰を開き直すのではなく射影を通して述べています。

  stage-mem x p = theEarliest x p .snd .snd .fst

  stage-earliest : (x : S) (p : ⟨ isL x ⟩)
                 → isLeastOrd (λ σ → x ∈ˢ Lset σ) (stage x p)
  stage-earliest x p = theEarliest x p .snd .snd .snd

まとめ

leastOrd は、ある性質を満たす順序数が存在するという切り詰められた証人から、その最小の順序数を取り出します。その特殊化 stage x hx は x を含む最小の Lset α の順序数添字 α を返し、stage-ord、stage-mem、stage-earliest がその事実を正確に述べます。後の議論では、これらの順序数添字を比較または上から抑えてから、対応する構成可能段階を使えます。