--- title: "古典論理との境界" module: Base.Classical lang: ja site: "Bedrock" description: "古典論理との境界" stage: "基礎" reading_order: 4 canonical: https://bedrock.institute/ja/Base.Classical.html html: Base.Classical.html agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/Base/Classical.lagda.md prerequisites: [Base.Prelude, Base.Impredicativity] routes: [common-foundations] translations: [https://bedrock.institute/en/Base.Classical.md, https://bedrock.institute/zh/Base.Classical.md] agent_guide: https://bedrock.institute/llms.txt license: "CC-BY-NC-SA-4.0" --- ```agda {-# OPTIONS --cubical --safe --guardedness #-} module Base.Classical where ``` # 古典論理との境界 ```agda open import Base.Prelude open import Base.Impredicativity using ( Resizing; ΩResizing; ΩResizing→Resizing ) ``` 本書は、構成的な Cubical 型理論を基礎として、その中で古典集合論を展開する。基礎を構成的なまま保つことで、古典的推論との境界が明確になる。排中律を必要としない定義と証明は構成的なまま残り、排中律を本当に必要とする定理だけが、それを明示的な引数として受け取る。初めから基礎理論に古典論理を組み込めば、定理の主張そのものからこの違いを読み取れなくなる。 排中律は、本書が古典的推論へ移る箇所を示すだけでなく、前章に残された命題の小ささに関する二つの問題も解決する。 - 命題リサイズ：`P : hProp ℓ₁` が与えられたとき、指定したレベル `ℓ₂` に、基礎型が `P` の基礎型と同値な命題を見つけられるか。 - 命題宇宙リサイズ：型 `hProp ℓ₁` 全体を `Type ℓ₂` の一つの型で提示できるか。 ## 排中律 排中律は、各命題に真偽の判定を与える。命題は異なる宇宙に住むため、この原理はレベルごとに述べる必要がある。 **定義** (`LEM`) ここでは「レベル `ℓ` での排中律」を `LEM ℓ` と表し、次の依存関数として定義する。各 `P : hProp ℓ` に対して判定 `Dec ⟨ P ⟩` を返し、`yes` は `P` の証明を、`no` はその反証を運ぶ。この関数は命題宇宙 `hProp ℓ` 全体を量化するので、`LEM ℓ` は `Type (ℓ-suc ℓ)` に住む。したがって、そのレベル添字は、この古典的仮定がどの命題を判定できるかを正確に記録する。 ```agda LEM : ∀ ℓ → Type (ℓ-suc ℓ) LEM ℓ = (P : hProp ℓ) → Dec ⟨ P ⟩ ``` **事実** (`isPropLEM`) 各レベル `ℓ` で、排中律 `LEM ℓ` 自体も命題である。 ```agda isPropLEM : ∀ {ℓ} → isProp (LEM ℓ) ``` **証明** 各 `P : hProp ℓ` に対して、`isPropDec` は `Dec ⟨ P ⟩` が命題であることを示す。命題の依存関数に対する閉性 `isPropΠ` を用いれば、主張が各点で従う。 ```agda isPropLEM {ℓ} = isPropΠ λ P → isPropDec ⟨ P ⟩isProp ``` **補題** (`lowerLEM`) 後続レベルでの排中律から、直下のレベルでの排中律が従う。この補題を繰り返し適用すれば、さらに一段ずつ下降できる。 ```agda lowerLEM : ∀ {ℓ} → LEM (ℓ-suc ℓ) → LEM ℓ ``` **証明** `lem : LEM (ℓ-suc ℓ)` が与えられたとし、`P : hProp ℓ` を固定する。`lem` はレベル `ℓ-suc ℓ` の命題を要求するため、`P` を直接判定することはできない。そこで、基礎型を `Lift ⟨ P ⟩`、命題性の証明を `isOfHLevelLift 1 ⟨ P ⟩isProp` とする上位レベルの命題を作る。この対を `lem` に渡せば、`P` の持ち上げられたコピーを判定できる。 下図の二つの分岐は、この判定を `Dec ⟨ P ⟩` へ戻す方法を示す。肯定の分岐では `lower` を用い、否定の分岐では `P` の証明を仮定してその持ち上げた像を反駁する。関数 `mapDec` が二つの変換をまとめる。 ```agda lowerLEM {ℓ} lem P = mapDec lower (λ np p → np (lift p)) (lem (Lift ⟨ P ⟩ , isOfHLevelLift 1 ⟨ P ⟩isProp)) ```
$$\operatorname{yes}\,\hat x$$
$\operatorname{Lift}\langle P\rangle$ $\hat x$ $\operatorname{lower}$ $\langle P\rangle$ $\operatorname{lower}\,\hat x$
$$\operatorname{yes}\,(\operatorname{lower}\,\hat x)$$
$$\operatorname{no}\,\mathit{np}$$
$\operatorname{Lift}\langle P\rangle$ $\operatorname{lift}\,p$ $\operatorname{lift}$ $\langle P\rangle$ $p$
$$\mathit{np}\,(\operatorname{lift}\,p):\bot_0$$
肯定の判定では `lower` で証明を下へ移す。否定の判定では `p : ⟨ P ⟩` を一時的に仮定し、`lift` で上へ移して `np` を適用し、矛盾を得る
## 排中律から得られる命題宇宙リサイズ 始域レベルのすべての命題を判定できれば、それぞれを二つのブールラベルの一方で表せる。任意のレベル `ℓ₁` と `ℓ₂` に対して、`ΩResizing ℓ₁ ℓ₂` は型 `hProp ℓ₁` 全体と同値な一つの型を `Type ℓ₂` に要求する。本章は `ℓ₁` での排中律からそのような分類子を構成し、一般定理 `ΩResizing→Resizing` によって、この命題宇宙の小さな表示を `Resizing ℓ₁ ℓ₂` へ移す。すなわち、始域レベルの各命題が終域レベルに同値な代表をもつ。 分類子には先に導入した型 `Bool` を用い、その二つの構成子 `true` と `false` をラベルとする。 これらのラベルは符号であり、それ自体が `hProp ℓ₁` の命題なのではない。`Bool` は `Type ℓ-zero` に住むため、符号の型を終域宇宙 `Type ℓ₂` の `Lift {ℓ-zero} {ℓ₂} Bool` へ持ち上げる。その二つのラベルは、任意のレベルで使える `hProp ℓ₁` の `⊤` と `⊥` をそれぞれ表す。この終域レベルの符号の型と命題宇宙との同値を構成すれば、求める命題宇宙リサイズが得られる。 構成は二段階に分かれる。第一段階では、まず明示的な判定 `Dec ⟨ P ⟩` から符号化を定義し、次に復号を定義し、最後に二つの往復則を証明する。この四つの補助結果を非公開の部分モジュール `BooleanCodes` にまとめる。いずれも排中律を使わない。第二段階の公開定理で初めて排中律を呼び出し、各 `P` に判定を一様に与え、この四つの結果を求める同値へ組み立てる。
```agda private module BooleanCodes where ```
**補題** (`encodeB`) 命題 `P` とその判定を入力として受け取り、`Lift {ℓ-zero} {ℓ₂} Bool` の符号を返す符号化操作が存在する。 ```agda encodeB : ∀ {ℓ₁ ℓ₂} (P : hProp ℓ₁) → Dec ⟨ P ⟩ → Lift {ℓ-zero} {ℓ₂} Bool ``` **証明** 与えられた判定を調べる。`yes` の枝は `lift true` を返し、`no` の枝は `lift false` を返す。どちらの枝も具体的な証明や反証を捨て、どちらの結果が成り立つかだけを保持する。判定は明示的に与えられるため、符号化は排中律を使わない。 ```agda encodeB P (yes _) = lift true encodeB P (no _) = lift false ``` **補題** (`decodeB`) `Lift {ℓ-zero} {ℓ₂} Bool` の符号を入力として受け取り、`hProp ℓ₁` の命題を返す復号操作が存在する。 ```agda decodeB : ∀ {ℓ₁ ℓ₂} → Lift {ℓ-zero} {ℓ₂} Bool → hProp ℓ₁ ``` **証明** 与えられた符号を調べる。`lift true` の枝は `⊤` を返し、`lift false` の枝は `⊥` を返す。どちらの枝もラベルを捨て、それが表す命題だけを保持する。二つの場合を直接与えるため、復号も排中律を使わない。 ```agda decodeB (lift true) = ⊤ decodeB (lift false) = ⊥ ``` **補題** (`secB`) 任意の命題 `P` とその判定 `d` に対して、`encodeB` で符号化してから `decodeB` で復号すると、`hProp` で `P` が復元される。すなわち `decodeB (encodeB P d) ≡ P` である。 ```agda secB : ∀ {ℓ₁ ℓ₂} (P : hProp ℓ₁) (d : Dec ⟨ P ⟩) → decodeB {ℓ₁} {ℓ₂} (encodeB {ℓ₁} {ℓ₂} P d) ≡ P ``` **証明** `d` について場合分けする。`d = yes p` なら、符号化は `lift true` を選び、復号は `⊤` を返すため、ゴールは `⊤ ≡ P` となる。命題外延性 `⇔toPath` は、`p` を返す写像と `tt*` を返す写像からこのパスを構成する。`d = no np` なら、符号化は `lift false` を選び、復号は `⊥` を返すため、ゴールは `⊥ ≡ P` となる。両方向の写像は、荒謬関数 `λ ()` と、反証 `np` を適用してから `⊥₀` から消去する関数である。したがって、どちらの場合も符号化してから復号すると `P` と等しい命題が復元される。 ```agda secB {ℓ₁} {ℓ₂} P (yes p) = ⇔toPath (λ _ → p) (λ _ → tt*) secB {ℓ₁} {ℓ₂} P (no np) = ⇔toPath (λ ()) (λ p → ⊥₀-rec (np p)) ``` **補題** (`retrB`) 任意の符号 `b̂` と、その復号で得た命題の判定 `d` に対して、`decodeB` で復号してから `encodeB` で符号化すると `b̂` が復元される。すなわち `encodeB (decodeB b̂) d ≡ b̂` である。 ```agda retrB : ∀ {ℓ₁ ℓ₂} (b̂ : Lift {ℓ-zero} {ℓ₂} Bool) (d : Dec ⟨ decodeB {ℓ₁} {ℓ₂} b̂ ⟩) → encodeB {ℓ₁} {ℓ₂} (decodeB {ℓ₁} {ℓ₂} b̂) d ≡ b̂ ``` **証明** まず `b̂` について場合分けし、次に `d` について場合分けするので、組合せは四つである。`b̂ = lift true` なら、復号は `⊤` を返す。証明は再び `lift true` を選ぶため、等式は `refl` で成り立つ。反証は `tt*` に適用すると `⊥₀` の元を生じるため不可能である。`b̂ = lift false` なら、復号は `⊥` を返す。証明は空パターン `()` によって不可能であり、反証は再び `lift false` を選ぶため、等式は `refl` で成り立つ。したがって、可能なすべての場合に復号してから符号化すると元の符号が復元される。 ```agda retrB {ℓ₁} {ℓ₂} (lift true) (yes _) = refl retrB {ℓ₁} {ℓ₂} (lift true) (no n⊤) = ⊥₀-rec (n⊤ tt*) retrB {ℓ₁} {ℓ₂} (lift false) (yes ()) retrB {ℓ₁} {ℓ₂} (lift false) (no _) = refl ```
二つの往復則から、各命題に判定を一様に与えられれば、符号化と復号が互いに逆写像になることがわかる。したがって、得られる分類子は二つの真理値ラベルで命題を全射的に覆うだけではなく、真正な型同値を与える。 候補となる証拠は対 `(Lift Bool , ...)` である。第一成分は `Type ℓ₂` に住み、第二成分は型同値 `hProp ℓ₁ ≃ Lift Bool` となる。ここでは `ℓ₁` と `ℓ₂` の大小関係を要求しない。後で使う下向きの実例では `ℓ₁ = ℓ-suc ℓ`、`ℓ₂ = ℓ` とするが、終域レベルが始域レベルと同じ場合や高い場合も許される。排中律に残された役割は一つだけであり、符号化器が必要とする判定を一様に供給することである。以上の四つの非公開な結果はいずれも構成的である。 **定理** (`LEM→ΩResizing`) 任意のレベル `ℓ₁` と `ℓ₂` に対して、始域レベル `ℓ₁` での排中律は、`ℓ₁` から `ℓ₂` への命題宇宙リサイズを導く。 ```agda LEM→ΩResizing : ∀ {ℓ₁ ℓ₂} → LEM ℓ₁ → ΩResizing ℓ₁ ℓ₂ ``` **証明** 第一成分として `Lift Bool` を選ぶ。第二成分には `isoToEquiv` を用い、次の同型を型同値へ変換する。同型の順写像は `P` を `encodeB P (lem P)` へ送り、逆写像は `decodeB` である。二つの往復則には、`lem` が与える判定で具体化した `retrB` と `secB` を用いる。この二つの成分が `ΩResizing ℓ₁ ℓ₂` に必要な証拠を構成する。 ```agda LEM→ΩResizing lem = Lift Bool , isoToEquiv (iso (λ P → encodeB P (lem P)) decodeB (λ b → retrB {ℓ₁ = _} b (lem (decodeB b))) (λ P → secB {ℓ₂ = _} P (lem P))) where open BooleanCodes ``` 図中の二つの三角形は、それぞれ二つの往復則によって閉じる。`lem : LEM ℓ₁` を固定し、符号の型 `Lift {ℓ-zero} {ℓ₂} Bool` を $B$ と略記し、$E(P) := \operatorname{encodeB}\,P\,(\operatorname{lem}\,P)$、$D := \operatorname{decodeB}$ と書く。各往復で得られる点は、示したパスによって出発点と結ばれる。
$B$ $E(P)$ $\operatorname{hProp}\,\ell_1$ $P$ $D(E(P))$ $E$ $D$ $\operatorname{secB}$
$\operatorname{hProp}\,\ell_1$ $D(b)$ $B$ $b$ $E(D(b))$ $D$ $E$ $\operatorname{retrB}$
符号化と復号はパスの意味で互いに逆となる。排中律は $E$ に判定を供給する。明示的な判定が与えられれば、符号化・復号と二つの往復則はいずれも構成的である
**系** (`LEM→Resizing`) 任意のレベル `ℓ₁` と `ℓ₂` に対して、始域レベル `ℓ₁` での排中律は、`ℓ₁` から `ℓ₂` への命題リサイズを導く。 **証明** まず `LEM→ΩResizing` を適用して命題宇宙リサイズを得てから、一般定理 `ΩResizing→Resizing` によって命題リサイズへ変換する。 ```agda LEM→Resizing : ∀ {ℓ₁ ℓ₂} → LEM ℓ₁ → Resizing ℓ₁ ℓ₂ LEM→Resizing lem = ΩResizing→Resizing (LEM→ΩResizing lem) ``` ## まとめ 本章では排中律をレベルごとに `LEM ℓ` と定め、それ自身が命題であることを示し、`lowerLEM` によって後続レベルの排中律から直下の実例を得た。`LEM ℓ₁` が与えられると、`LEM→ΩResizing` は任意の目標レベル `ℓ₂` に対して `ΩResizing ℓ₁ ℓ₂` を構成する。さらに `ΩResizing→Resizing` と合成すれば、`Resizing ℓ₁ ℓ₂` が得られる。したがって、始域レベルでの一つの排中律の仮定が、本章の冒頭で挙げた二つの大きさの問題をともに解決する。