Bedrock古典論理との境界
この章を読むか、読書案内と依存マップで別のルートを選べます。
読書案内 · 依存マップ宇宙レベルをもつ型理論では、命題について二つの異なる小ささの問題が生じます。第一に、命題 P : hProp (ℓ-suc ℓ) を固定したとき、一つ下のレベルに同値な命題を見つけられるか。これが命題リサイズで、命題ごとに語る主張です。第二に、レベル ℓ の命題全体の型 hProp ℓ 自身が Type (ℓ-suc ℓ) に住んでいます。この全体を一つの小さな型で提示できるか。これが小分類子です。二つの主張は形が異なりますが、本章は一つの明示的な仮定から両方を証明します。
その仮定が排中律です。所定のレベルのすべての命題は、真か偽かのどちらかだという原理です。Cubical 型理論は排中律を仮定しないため、ここでの古典的な証明はそれぞれそれを明示的な引数として受け取り、各結果はどのレベルの実例を使ったかを正確に記録します。構成的な定義と古典的な段階は終始分かれています。構成そのものは何も判定せず、仮定が現れるのは判定を消費する場所だけです。
{-# OPTIONS --cubical --safe --guardedness #-} module Base.Classical where
二つの小ささの問題は「非可述性」の章で正確な形を与えられており、本章はその語彙をそのまま使います。単一の命題に対して isSmall P は、低いレベルの命題 Q : hProp ℓ と基礎型の間の同値 ⟨ P ⟩ ≃ ⟨ Q ⟩ からなります。一様な主張は何を量化するかで異なります。Resizing ℓ はすべての P : hProp (ℓ-suc ℓ) がそのようなデータを持つことを要求し、HPropSmallness ℓ は全体の hProp ℓ と一度に同値な型 Ω' : Type ℓ を一つ要求します。前者は命題ごとの証拠の族、後者は全体を提示する単一の台です。本章は排中律から両者をそれぞれ導き、両者の間の含意については何も主張しません。
open import Base.Prelude open import Base.Impredicativity using ( isSmall; Resizing; HPropSmallness; Impredicativity )
命題を判定するとは何かを、証明に先立って固定しておきます。P を判定するとは、⟨ P ⟩ の証明を与えるか、⟨ P ⟩ から空型への写像を与えるかのどちらかです。後者は任意の証明を不条理に変えることで P を反証します。直和 _⊎_ とその二つの構成子が担うのはまさにこの二者択一であり、この選言は本物のデータです。元は自分がどちらの直和項から来たかを知っているので、判定は場合分けで使えます。ブール値 Bool と true、false は二つの結果にラベルを付け、tt* は「真」の命題の底にある単元型の唯一の元です。
open import Cubical.Data.Sum using ( _⊎_; inl; inr ) import Cubical.Data.Empty as Empty open import Cubical.Data.Bool using ( Bool; true; false ) open import Cubical.Data.Unit using ( tt* )
小ささは「同じである」を通して命題を比較します。以下には、その二つの形が現れます。二つの命題の間では、両方向の写像の組は、命題外延性 ⇔toPath によって hProp 値の間のパスを与え、propBiimpl→Equiv によって基礎型の間の同値を与えます。同型 iso は二つの写像と二つの逆法則をまとめて記録し、isoToEquiv がそれを同値として読みます。分類子は命題を同一視するので hProp のパスを作り、命題リサイズは基礎型の同値を届けなければなりません。
open import Cubical.Foundations.Equiv using ( propBiimpl→Equiv ) open import Cubical.Foundations.Isomorphism using ( iso; isoToEquiv ) open import Cubical.Functions.Logic using ( ⇔toPath )
排中律の主張
何かを証明する前に、仮定を宇宙レベルとともに正確に述べておく必要があります。レベルの添字は飾りではありません。どの宇宙で一様な判定を要求するかを告げており、後の定理はどの古典的実例を求めているのかを読み取ることができます。
各宇宙レベル ℓ に対して LEM ℓ は、命題 P : hProp ℓ を受け取り、⟨ P ⟩ の証明か、あるいは ⟨ P ⟩ を空型へ写す反証のどちらかを返す関数です。hProp ℓ のすべての命題を量化するため、その型は一つ上の宇宙 Type (ℓ-suc ℓ) に住みます。主張そのものは大きくても、生み出される個々の判定は小さなデータのひと塊にすぎず、さらに LEM ℓ は全レベル一度にではなく一レベルずつ主張されます。この形がもたらす強さに注意してください。判定は命題ではなくデータなので、排中律の仮定から、証明の場合と反証の場合に分けて推論できます。どちらかが存在すると主張するだけではありません。
LEM : ∀ ℓ → Type (ℓ-suc ℓ) LEM ℓ = (P : hProp ℓ) → ⟨ P ⟩ ⊎ (⟨ P ⟩ → Empty.⊥)
応用では排中律が複数のレベルで要りますが、証明に渡されるのはしばしば高い方の実例 LEM (ℓ-suc ℓ) だけです。一段の下降補題がその差を埋めます。結果は正確に一段分、すなわち LEM (ℓ-suc ℓ) → LEM ℓ です。P : hProp ℓ を判定するには、一つ上の宇宙で P の持ち上げられたコピーを判定し、その結果を持ち帰ります。判定が一度に任意の段数を降りるとは主張しません。
lem : LEM (ℓ-suc ℓ) と命題 P : hProp ℓ が与えられたときの計画は、lem を P 自身ではなく、レベル ℓ-suc ℓ に住み仮定が適用できる P の持ち上げられたコピーに適用し、そのコピーについての判定を P についての判定へ翻訳し戻す、というものです。
lowerLEM : ∀ {ℓ} → LEM (ℓ-suc ℓ) → LEM ℓ lowerLEM {ℓ} lem P = fromLifted (lem lifted)
持ち上げられた命題の基礎型は Lift ⟨ P ⟩ で、その元は一つ上の宇宙における ⟨ P ⟩ の元です。そしてこれは命題です。元 x と y に対し、lower で両者を ⟨ P ⟩ へ降ろし、P の命題性 P .snd で降ろしたもの同士のパスを得て、cong lift でそのパスを上の宇宙へ持ち上げます。こうして lifted は lem の正当な入力になります。
where lifted : hProp (ℓ-suc ℓ) lifted = Lift ⟨ P ⟩ , λ x y → cong lift (P .snd (lower x) (lower y))
判定の翻訳に必要なのは lift と lower だけで、両者はちょうど正しい方向へ進みます。Lift ⟨ P ⟩ の証明は lower で ⟨ P ⟩ の証明へ降り、Lift ⟨ P ⟩ の反証は lift との合成で ⟨ P ⟩ の反証になります。持ち上げた後に ⟨ P ⟩ の任意の証明へ適用できるからです。どちらの場合も判定を運ぶだけの純粋な変換であり、ここに古典的推論はありません。古典的な一歩は、持ち上げられた命題を判定したところで起こっています。
fromLifted : ⟨ lifted ⟩ ⊎ (⟨ lifted ⟩ → Empty.⊥) → ⟨ P ⟩ ⊎ (⟨ P ⟩ → Empty.⊥) fromLifted (inl p) = inl (lower p) fromLifted (inr np) = inr (λ p → np (lift p))
排中律から得られる小分類子
古典的な見方では、固定したレベルの命題は真か偽かの二つのどちらかです。そこで自然に浮かぶのが二点からなる分類子です。小さな代表の候補は Lift Bool で、true が真という命題を、false が偽という命題を代表します。ここで二つの注意が必要です。ブール値はラベルにすぎず、それが代表する命題は別の hProp 値であり、分類子が両者を同一視するのは hProp 値の間のパスに関してであって、構文的な同一によってではありません。また両端の大きさは異なります。Lift Bool は Type ℓ に、hProp ℓ は Type (ℓ-suc ℓ) に住み、同値は異なるレベルの型を結んでもよく、この大きさの差こそが確立される小ささです。
構成はきれいに二段に分かれます。復号は各ブール値をその代表である命題へ送ります。符号化には、与えられた P がどちらの場合かを知る必要があるので、P の判定を明示的な引数として受け取ります。二つの逆法則はそのデータに対して証明されます。排中律が現れるのは最後だけで、判定を一様に供給するためです。
二つの代表命題は、「基礎語彙」の論理演算における正準な頂命題 ⊤ と底命題 ⊥ です。後者は定義上、対 (⊥* , isProp⊥*) そのものであり、その基礎型は空型 ⊥* です。両者は任意のレベル ℓ で使えるので、hProp ℓ の中で代表を務められます。後のブールのラベルが指すのはまさにこの二つの命題です。
private decodeB : ∀ {ℓ} → Lift {ℓ-zero} {ℓ} Bool → hProp ℓ
復号はブールのラベルを読んで、それが代表する命題を返します。lift true は ⊤ を、lift false は ⊥ を返します。定義域は Bool 自身ではなく持ち上げの Lift {ℓ-zero} {ℓ} Bool です。Bool は Type ℓ-zero に住み、その持ち上げは Type ℓ の型であり、分類子の主張が要求するのはこちらです。復号だけなら代表を割り当てる関数にすぎず、その割り当てが両方向で忠実であることは、後に続く二つの逆法則の内容です。
decodeB (lift true) = ⊤ decodeB (lift false) = ⊥
符号化は逆向きの割り当てです。P と P の判定が与えられれば、勝った場合のラベルを返します。判定は明示的な引数であり、符号化器自身が作り出すものではないので、この段階で排中律は使いません。一般に P の代表を選ぶのは二段階の作業です。まず P を判定し、それからラベルを読み取ります。二つの逆法則は、この往復がそれぞれ恒等であること、一つは命題の上で、もう一つはラベルの上で、示すことになります。
マッチの対象は P ではなく判定です。左の直和項の元なら lift true を、右の元なら lift false を返します。証明や反証そのものは捨てられます。ラベルが記録するのはどちらの場合だったかだけで、証拠ではないからです。結果の型は Lift {ℓ-zero} {ℓ} Bool で、decodeB の定義域と正確に一致します。
encodeB : ∀ {ℓ} (P : hProp ℓ) → ⟨ P ⟩ ⊎ (⟨ P ⟩ → Empty.⊥) → Lift {ℓ-zero} {ℓ} Bool encodeB P (inl _) = lift true encodeB P (inr _) = lift false
最初の逆法則は、判定を通して選ばれた代表が P と同じ真理値を持つことを述べます。具体的には secB が decodeB (encodeB P d) ≡ P、つまり hProp 値の間のパスを証明します。どちらの場合も証明の戦略は同じで、両方向の写像を与え、命題外延性 ⇔toPath にパスを組み立てさせます。
判定が証明 p だった場合、ゴールは ⊤ ≡ P です。⊤ から ⟨ P ⟩ への写像は判定で得た証拠 p そのものであり、逆方向ではすべての入力が ⊤ の唯一の元 tt* に写ります。判定が反証 np だった場合、ゴールは ⊥ ≡ P です。⊥* には照合すべき構成子がないことを荒謬パターン λ () が表し、⟨ P ⟩ の各証明 p は np に渡され Empty.rec で消去されます。どちらの分岐でも選ばれた代表は P とパスで等しく、符号化の往復が真理値を失わないことがわかります。
secB : ∀ {ℓ} (P : hProp ℓ) (d : ⟨ P ⟩ ⊎ (⟨ P ⟩ → Empty.⊥)) → decodeB (encodeB P d) ≡ P secB P (inl p) = ⇔toPath (λ _ → p) (λ _ → tt*) secB P (inr np) = ⇔toPath (λ ()) (λ p → Empty.rec (np p))
第二の逆法則は代表を読み戻します。encodeB (decodeB b) d ≡ b です。ここで本質的な注意が一つあります。組み上がった分類子では判定 d を排中律が供給しますが、その判定がどのように計算されるかを保証するものは何もありません。したがって retrB は、特定の証明が供給しうる判定だけでなく、すべての判定 d に対して成り立たねばなりません。証明は四つの場合に分かれます。両立する二つの分岐は refl に計算され、両立しない二つの分岐は不可能として消去されます。これはまた、⊤ に要素があり ⊥ が空であることから、二つの代表が混同されえないことも示しています。
b = lift true のとき、復号は ⊤ を返します。証明とともに符号化すれば lift true が返り、ゴールは定義上 refl です。反証の分岐は起こりえません。⊤ の元 tt* に適用すれば空型の元が得られ、Empty.rec がこの矛盾から場合を締めくくります。
retrB : ∀ {ℓ} (b : Lift {ℓ-zero} {ℓ} Bool) (d : ⟨ decodeB b ⟩ ⊎ (⟨ decodeB b ⟩ → Empty.⊥)) → encodeB (decodeB b) d ≡ b retrB (lift true) (inl _) = refl retrB (lift true) (inr n⊤) = Empty.rec (n⊤ tt*)
b = lift false のとき、復号は ⊥、すなわち基礎型 ⊥* を持つ命題を返します。そのいわゆる証明は空型の項になるはずなので、荒謬パターン () がこの分岐を直ちに終わらせ、反証とともに符号化すれば lift false が返り、これも refl で済みます。四つの場合を通して、どの判定が供給されようとも、返されるラベルは出発点のラベルと等しくなります。
retrB (lift false) (inl ()) retrB (lift false) (inr _) = refl
いま部品が HPropSmallness ℓ が約束する分類子へと組み上がります。すなわち Type ℓ の、hProp ℓ と同値な型です。小さな型は Lift Bool であり、同値は順方向の写像が decodeB、逆方向の写像が P を判定して符号化するもので構成されます。二つの逆法則はまさに secB と retrB で、それぞれ lem からの判定で具体化されます。この節で排中律が働くのはここです。構成的な部分が入力として取る判定を、一様に供給するのです。
対 (Lift Bool , ...) が HPropSmallness ℓ の証拠です。第一成分は Type ℓ の型で、第二成分は同値 Lift Bool ≃ hProp ℓ です。ポイントはレベルの配置にあります。Lift Bool : Type ℓ、hProp ℓ : Type (ℓ-suc ℓ) なので、一つ上の宇宙の型が小さな代表を得るのです。これはレベルについてのサイズの主張であって、両端が同じ宇宙に属するとの主張ではありません。さらに同値そのものは二つの逆法則に依存するため、ブールのラベルとその命題が同一視されるのは secB と retrB が認証するパスに関してだけです。
lem→hPropSmallness : ∀ {ℓ} → LEM ℓ → HPropSmallness ℓ lem→hPropSmallness lem = Lift Bool , isoToEquiv (iso decodeB (λ P → encodeB P (lem P)) (λ P → secB P (lem P)) (λ b → retrB b (lem (decodeB b))))
排中律から得られる命題リサイズ
第二の小ささの問題は命題ごとのものです。P : hProp (ℓ-suc ℓ) を固定すると、リサイズは命題 Q : hProp ℓ と基礎型の間の同値 ⟨ P ⟩ ≃ ⟨ Q ⟩ を産み出します。同じ二つの代表が再び使えます。P が真なら ⊤ を、偽なら ⊥ を取ります。どちらもレベル ℓ に住みます。結果の形に注意してください。基礎となる型の間の同値であって、まとめられた命題 P と Q の間のパスではありません。
二つの構成が違うのは、組み立てる「同じである」の種類です。分類子は命題を同一視するので、その「同じである」は命題外延性によって hProp 値の間のパスとして組み立てられました。命題リサイズが届けるべきは基礎型の間の同値であり、propBiimpl→Equiv はまさにそれを産み出します。両側の命題性の証明 P .snd と Q .snd と二つの写像を与えれば、⟨ P ⟩ ≃ ⟨ Q ⟩ が返ります。
P の判定が与えられると、resizeDec は isSmall P の証拠を返します。真の場合の証拠は (⊤ , 同値) です。⟨ P ⟩ から ⊤ への写像はすべての入力を tt* に写し、戻りの写像は判定で得た証明 p を使います。両側が命題なので、propBiimpl→Equiv は命題性の証明 P .snd と ⊤ .snd を与えられ、この写像の組を基礎型の間の同値に変えます。
private resizeDec : ∀ {ℓ} (P : hProp (ℓ-suc ℓ)) → ⟨ P ⟩ ⊎ (⟨ P ⟩ → Empty.⊥) → isSmall P resizeDec P (inl p) = ⊤ , propBiimpl→Equiv (P .snd) (⊤ .snd) (λ _ → tt*) (λ _ → p) resizeDec P (inr np) = ⊥ , propBiimpl→Equiv (P .snd) (⊥ .snd)
偽の場合の証拠は (⊥ , 同値) で、写像は secB と同じものです。⟨ P ⟩ からの写像は各証明 p を反証 np と Empty.rec で処理し、逆方向の写像は ⊥* に構成子がないためその場で荒謬です。代表 ⊤ と ⊥ はどちらも P より一段下のレベル ℓ に住み、これがまさに認証される小ささです。Q は hProp ℓ の中から選ばれ、同値が ⟨ P ⟩ と ⟨ Q ⟩ を結びます。
(λ p → Empty.rec (np p)) (λ ())
命題リサイズはこれで、レベル ℓ-suc ℓ の排中律の一つの実例から従います。レベルがこう定まるのは主張そのものによるものです。Resizing ℓ は hProp (ℓ-suc ℓ) 上で量化するので、消費する判定はちょうど一つ上の宇宙の命題の判定です。
lem→resizing は LEM (ℓ-suc ℓ) を一行で Resizing ℓ に変えます。各 P : hProp (ℓ-suc ℓ) に対し、lem で判定し、その結果を resizeDec に渡すだけです。要点はすべてレベルの向きにあります。レベル ℓ の命題リサイズが消費するのは ℓ-suc ℓ の古典的判定です。下の宇宙に同値な代表を得る命題が、ちょうど一つ上の宇宙のものだからです。
lem→resizing : ∀ {ℓ} → LEM (ℓ-suc ℓ) → Resizing ℓ lem→resizing lem P = resizeDec P (lem P)
二つの帰結をまとめる
二つのサイズの制御が今や一つの仮定から得られます。LEM (ℓ-suc ℓ) の一つの実例が命題リサイズを直接与え、さらに lowerLEM で一段降りることで小分類子も与えます。二つの原理は異なる主張のままです。本章は同じ仮定から両方を証明しますが、一方が他方を含意するかどうかについては何も主張しません。
「非可述性」の章のレコード Impredicativity ℓ は原理ごとに一つずつ、二つのフィールドを持ち、lem→impredicativity は単一の lem から両方を満たします。リサイズのフィールドは lem→resizing lem で、与えられた実例をそのレベルでそのまま使います。分類子のフィールドは lem→hPropSmallness (lowerLEM lem) で、まず LEM ℓ まで降りてから Lift Bool ≃ hProp ℓ を構成します。この共有はこの導出についての事実、つまり二つの帰結が同じ上位実例から証明できたことであり、原理同士が相互に含意するという主張ではありません。
lem→impredicativity : ∀ {ℓ} → LEM (ℓ-suc ℓ) → Impredicativity ℓ lem→impredicativity lem = record { resizing = lem→resizing lem ; hPropSmallness = lem→hPropSmallness (lowerLEM lem) }
まとめ
本章における排中律はただ一つのものです。明示したレベルのすべての命題を判定する能力であり、つねに明示的な仮定として渡されます。ℓ-suc ℓ の一つの実例が、章全体に必要な判定を供給しました。lowerLEM のために持ち上げられた各命題を判定し、命題リサイズのために各 P : hProp (ℓ-suc ℓ) を判定し、さらに一段の下降を経て、小分類子のために各 P : hProp ℓ を判定します。二つの帰結は依然として異なる原理であり、本章は両者を比べることをしません。lem→impredicativity が両者を同時に持つのは、同じ仮定がたまたま両方を与えたからです。累積階層の諸章はこのインターフェースを受け取り、全分離と V の冪集合の背後で小ささが求められる場所で用います。