選択原理

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

読書案内 · 依存マップ

古典数学で用いられる原理は、排中律だけではありません。空でない集合の族が与えられれば、各集合から同時に一つずつ要素を選べます。有限の族や明示的に記述された族なら日常的な手続きですが、任意の集合で添字付けられた族に対しては、これは選択公理という固有の原理です。型理論は、ここでいう「空でない」をいっそう正確にします。基礎理論では、ファイバー B x の元は命題的切り詰め ∥ B x ∥₁ の後ろに隠れています。切り詰めはファイバーに元があることを記録しますが、どの元かは忘れます。切り詰めは命題へしか消去できないので、この形の仮定から実際の元を取り出すことはできません。「基礎語彙」は、切り詰められた存在から本物の関数を取り出すには選択原理が要ると述べました。したがってこの原理の仮定は、各ファイバーが単に要素を持つ、という形をしか取れません。結論にも切り詰めが残ります。主張されるのは、すべてのファイバーで同時に値を選ぶ一つの関数の単なる存在であり、関数そのものではありません。この主張には最初から一つの制限が含まれます。添字の型は h-集合でなければならず、ディアコネスクの定理の証明はまさにこれを用います。

集合レベルの選択と LEM は、どちらもレベルごとに述べられるので、その族の外側の型は同じ ∀ ℓ → Type (ℓ-suc ℓ) です。ただし、内側で量化する対象は異なります。排中律は命題全体にわたり、選択は h-集合 X、その上の族 B、そして各ファイバーが単に要素を持つことの証明にわたります。どちらの原理も大域的には仮定されず、必要とする章は所定のレベルの実例を明示的なパラメータとして受け取ります。

本章は三つの問いを中心に進みます。選択原理はここで何を主張し、どのレベルで主張するのか。一つ上の宇宙の仮定一つで、それより下のレベルを覆えるのか。そしてこの原理はどれほど強いのか。最後の問いにディアコネスクの定理が答えます。SetChoice ℓ は LEM ℓ を含意します (choice→lem)。したがって各レベルで選択のインターフェースはすでに排中律を与え、二つのインターフェースは対等ではありません。モデルの章はこのことを二度頼ります。choice→lem が一つの SetChoice (ℓ-suc ℓ) の実例から ZF の公理を支える排中律を得て、lowerSetChoice が同じ実例を下げて選択集合の公理に用います。

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

module Base.Choice where

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

open import Cubical.Foundations.Prelude using ( Path )

ディアコネスクの定理の証明は有限の議論であり、三つの具体的な材料を用います。ブール型 Bool と true、false は二点の型をなし、その等しさは _≟_ が判定します。単元型 Unit* は唯一の元 tt* を持ち、isPropUnit* がこれを命題として記録するので、議論には自明に成り立つ主張がいつでも用意できます。二つのブール値の比較は Dec の元を返します。yes に等式が伴うか、no に反証が伴うかです。

open import Cubical.Foundations.HLevels using ( isOfHLevelLift )
open import Cubical.Data.Bool using ( Bool; true; false; _≟_ )
open import Cubical.Data.Unit using ( Unit*; tt*; isPropUnit* )
open import Cubical.Relation.Nullary using ( Dec; yes; no )
import Cubical.Data.Sum as Sum

このほか、証明には二つの構成が要ります。第一は命題的切り詰め ∥_∥₁ で、「基礎語彙」で紹介しました。型の有元性だけを保ち、それがどの元であったかを忘れるので、∥ A ∥₁ から A 自身の元を取り出すことはできません。第二は集合商で、本書で初めて登場します。型と関係から類からなる型を作るもので、ディアコネスクの構成はその内部で行われます。

import Cubical.Data.Empty as Empty
import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∥_∥₁ )
open import Cubical.HITs.SetQuotients
  using ( _/_; [_]; eq/; squash/; []surjective; effective )

集合商そのものは任意の関係から作れます。ここで用いるより強い effectivity 定理は、商類の等しさを元の関係へ逆向きに読むものであり、関係が命題値で同値律を満たすことを要求します。ライブラリはこの二つの条件をレコードで表し、貼り合わせの関係が両方を満たすことをそれぞれ証明します。

open import Cubical.Relation.Binary.Base using ( module BinaryRelation )

原理

原理は、固定したレベル ℓ の上で、各ファイバーについての仮定と、すべてのファイバーを一度に扱う結論とを比べます。データは、Type ℓ の添字型 X、X が h-集合であることの証明、X の上のファイバーの族 B、そして各 x に対する仮定 ∥ B x ∥₁ です。結論 ∥ ((x : X) → B x) ∥₁ が言うのは、すべてのファイバーで同時に要素を選ぶ一つの関数が単に存在することです。切り詰めが両側に現れるのが、この原理の正確な強さです。仮定が与えるのは単なる要素の存在までであり、結論もそれ以上を主張しません。実際の選択関数こそ欠けているものであり、それを供給することがこの仮定の内容のすべてです。主張が Type ℓ 全体を量化するため、LEM と同じ理由で、それは一つ上の Type (ℓ-suc ℓ) に住みます。

SetChoice : ∀ ℓ → Type (ℓ-suc ℓ)
SetChoice ℓ = (X : Type ℓ) → isSet X → (B : X → Type ℓ)
            → ((x : X) → ∥ B x ∥₁) → ∥ ((x : X) → B x) ∥₁

排中律と同様、応用で使う選択にはしばしば一つの高いレベルの実例だけが渡され、下降の補題がそれを必要なレベルへ移します。lowerSetChoice の型は SetChoice (ℓ-suc ℓ) → SetChoice ℓ です。一つ上の宇宙の選択を仮定して、レベル ℓ の選択を取り戻します。lowerLEM と同じく、ここで用いる道具は Lift です。「基礎語彙」にある、Type ℓ の型を Type (ℓ-suc ℓ) の中で提示し、また取り戻す演算です。

レベル ℓ のデータが与えられると、証明はまずそれを一つ上のレベルへ移し、仮定 sc を適用できるようにします。添字型 X は Lift X となり、その h-集合性は setX から isOfHLevelLift によって従います。これは、持ち上げがホモトピーレベルを乱さないことを記録するライブラリの定理です。ファイバーの族は λ x → Lift (B (lower x)) となります。持ち上げられた添字の上のファイバーは、その下の元の添字の上のファイバーを持ち上げたものであり、移した族は元の族とまったく同じ情報を含みます。

lowerSetChoice : ∀ {ℓ} → SetChoice (ℓ-suc ℓ) → SetChoice ℓ
lowerSetChoice sc X setX B inh =
  PT.map (λ f x → lower (f (lift x)))
         (sc (Lift X) (isOfHLevelLift 2 setX)
             (λ x → Lift (B (lower x)))

残りの入力も同じ方法で移します。持ち上げられた各ファイバーが単に要素を持つのは、添字を降ろし、得られた切り詰めに lift を写像すれば必要な元が示されるからです。PT.map は切り詰めの内部で働くので、仮定は原理が求める通りの形で満たされます。sc が持ち上げられた選択関数 f の単なる存在を返したら、もう一度の PT.map が降ろした関数の単なる存在を与え、その x での値は lower (f (lift x)) です。最後の一段が正当なのは、目標が切り詰めの内部の主張だからです。この具体的な f について、切り詰めの外で主張されることは何もありません。

             (λ x → PT.map lift (inh (lower x))))

ディアコネスクの定理

定理はこう述べます。集合レベルの選択が与えられれば、任意の命題 P は判定できる、すなわち証明か反証のいずれかが得られます。構成的な立場から見れば、この結論は決して明らかではありません。任意の P は場合分けの入口を与えず、判定手続きが直接調べられるものもないからです。そこで証明は幾何的に進みます。形が P に応じて変わる小さな空間を作ります。その空間で true の類と false の類は、P が成り立つとき、そしてそのときに限って一致します。この空間についてのただ一つの質問を選択原理に投げれば、形は白日の下にさらされ、その形こそが P です。

具体的には、命題 P : hProp ℓ を固定し、この定理専用のモジュールの中で作業します。二つのブール値を、P が成り立つときちょうど貼り合わせます。貼り合わせとは集合商のことです。点は true と false のまま保たれ、貼り合わせの関係がそう述べるときには道が加えられ、結果は h-集合にされます。関係は四項の表です。対角では自明に成り立ち、混色の二項は文字どおり P そのものです。この最後の条項により、二点をまたぐ関係が成り立つことは P と同じ主張であり、議論はこれを二度使います。

貼り合わせの関係 _~_ は二つのブール値へのパターンマッチで定義され、表の四項が一目で分かります。入力が一致するとき、関係は単元型 Unit* の唯一の元 tt* とともに成り立ちます。異なるときは、⟨ P ⟩、すなわち P の基礎となる主張の証明とともに成り立ちます。ほかに使うものは何もありません。表の混色の項を読み取ることが、二点をまたぐ関係がまさに P を述べていることの証明になっています。

module Diaconescu {ℓ} (P : hProp ℓ) where

  _~_ : Bool → Bool → Type ℓ
  true  ~ true  = Unit*
  false ~ false = Unit*
  _     ~ _     = ⟨ P ⟩

空間そのものである Glued は集合商 Bool / _~_ です。型を関係で割ると、点は保たれ、関係が二者を結ぶ証明が与えられるたびに、構成子 eq/ が道 [ b ] ≡ [ b' ] を加えます。構成子 squash/ はさらに結果を h-集合にします。注目する二点は類 [ true ] と [ false ] です。P が成り立てば商が両者の間の道を供給し、成り立たなければ、後の逆読みが二つの類を引き離します。

  Glued : Type ℓ
  Glued = Bool / _~_

この先のすべては、集合商についての一条の定理、ライブラリの有効性にかかっています。命題値で同値律を満たす関係に対して、類の間の道が存在するのは、関係が実際に代表元を結んだとき、そのときに限ります。したがって商の中の道は、関係が成り立ったことの証明として逆読みできます。表はこの定理の要求する条件を項ごとに供給し、続く段落が一つずつ検証します。

第一の条件は命題値性です。入力の各組に対して、a ~ b の証明の型が命題でなければなりません。対角ではこの型は Unit* であり、isPropUnit* が命題であることを示します。混色の項では ⟨ P ⟩ そのものであり、その命題性は P の第二成分 P .snd にほかなりません。証明が異なり得るなら、商の道は逆読みのための well-defined な主張を定められません。

  ~-prop : BinaryRelation.isPropValued _~_
  ~-prop true  true  = isPropUnit*
  ~-prop false false = isPropUnit*
  ~-prop true  false = P .snd
  ~-prop false true  = P .snd

反射性は直ちに得られます。対角の二項は条件なしで成り立つので、すべてのブール値は自分自身と関係を持ち、その場合の証明はいずれも tt* です。

  ~-refl : (a : Bool) → a ~ a
  ~-refl true  = tt*
  ~-refl false = tt*

  ~-sym : (a b : Bool) → a ~ b → b ~ a
  ~-sym true  true  _ = tt*

対称性は、表そのものが対称なことから成り立ちます。入力を入れ替えても各項は自分自身に写るので、a ~ b の証明は b ~ a の証明として働きます。対角ではどちら向きでも証明は tt* であり、混色の項では P の証明であり、両方向で同じものです。

  ~-sym false false _ = tt*
  ~-sym true  false p = p
  ~-sym false true  p = p

  ~-trans : (a b c : Bool) → a ~ b → b ~ c → a ~ c
  ~-trans true  _     true  _ _ = tt*

推移性にはもう少しの注意が要ります。二つの証明の組が、表に存在しない項を要求する可能性が原理的にはあるからです。場合を調べれば、それは起こりえないと分かります。両端が一致していれば、どこかの対角の項が結論を自明にします。異なっていれば、与えられた二つの証明のどちらかは混色の項から来ており、もう一方はこのとき等しいブール値しか含まないので、同じ P の証明がそのまま結論になります。六つの場合がすべての可能性を覆い、それぞれが入力の一つを再利用します。

  ~-trans false _     false _ _ = tt*
  ~-trans true  false false p _ = p
  ~-trans false true  true  p _ = p
  ~-trans true  true  false _ p = p
  ~-trans false false true  _ p = p

三つの法則は、構成子 BinaryRelation.equivRel によってレコード isEquivRel _~_ に組み立てられます。命題値性と同値律が揃うと、Glued は有効性の仮定をちょうど満たし、道の逆読みが以下の補題で使えるようになります。

  ~-equivRel : BinaryRelation.isEquivRel _~_
  ~-equivRel = BinaryRelation.equivRel ~-refl ~-sym ~-trans

構成の核心は二行の主張です。二つの注目すべき類が一致するのは、P が成り立つとき、そのときに限ります。P が成り立てば、表は true と false を結び、商は両者の類を同一視します。二つの類が一致すれば、有効性は関係が true と false を結んだと報告し、表によればその関係こそ P です。混色の項は両方向で働きます。P の証明はそのまま道の構成子に渡り、有効性の出力はすでに ⟨ P ⟩ の証明であり、復号も不可能な場合の除去も要りません。

二つの向きは名前付きの関数になります。順方向の glue は P の証明を道の構成子に渡します。混色の項は証明 p とともに成り立つので、商の定義により二つの類は等しくなります。逆方向の unglue は true と false で具体化した有効性です。二つの類の間の任意の道が true ~ false の証明を返し、表によればそれは ⟨ P ⟩ の証明です。道に対する場合分けは不要です。両者合わせて、P と二つの類の一致とを結ぶ辞書になります。

  glue : ⟨ P ⟩ → Path Glued [ true ] [ false ]
  glue p = eq/ true false p

  unglue : Path Glued [ true ] [ false ] → ⟨ P ⟩
  unglue = effective ~-prop ~-equivRel true false

いま選択原理を用います。問いはただ一つ、Glued の各点にブール値の代表元を一つずつ渡せ、というものです。ある点での選択 (pick) とは、一つのブール値と、その類がその点に等しいという保証の組です。点ごとには必ず選択がありますが、それは単に存在するだけです。商は自分の点が代表元から来たことを覚えていても、どの代表元かは覚えていません。この点ごとの単なる非空性を、あらゆる点で一度に選ぶ一つの関数の単なる存在へ変えるのが、まさに集合レベルの選択の述べるところであり、Glued が構成上 h-集合であるためここに適用できます。選択関数は空間全体で一様に働き、最後の比較は二つの注目すべき類でのみ読み取ります。

選択の対象となる族は Pick x という依存対です。ブール値 b と、類 [ b ] が点 x に等しいことを見届ける道の組です。各点が単に選択を持つことは追加の仮定ではなく、商についての定理です。[]surjective は商の任意の元が、単に、何らかの代表元の類として現れると述べ、pickable はそれを x が Glued を走る形で読んだものです。第二成分の役割に注目してください。これはどの代表元が選ばれたかを記録する証明書であり、後に類と類の間の道を組み立てるのは、ブール値そのものではなくこの証明書です。

  Pick : Glued → Type ℓ
  Pick x = Σ[ b ∈ Bool ] ([ b ] ≡ x)

  pickable : (x : Glued) → ∥ Pick x ∥₁
  pickable = []surjective

この問いは独立した補題にする価値があります。型そのものが、選択原理が与えるもの、すなわち Glued 全体で定義された選択関数の単なる存在を示すからです。sc : SetChoice ℓ が与えられると、補題はこれまでに揃えたデータでこれを具体化します。添字 Glued、その h-集合の証明 squash/、族 Pick、点ごとの非空性 pickable です。仮定 sc はそれ自体が関数であり、切り詰められるのはその出力だけです。したがって選択が与えるのは関数ではなく、それがあるという主張であり、この制限が定理の最終段階の形を決めます。

  merePicker : SetChoice ℓ → ∥ ((x : Glued) → Pick x) ∥₁
  merePicker sc = sc Glued squash/ Pick pickable

いま picking 関数 g : (x : Glued) → Pick x が手もとにあるとします。二つの注目点で評価すれば二つの選択が得られ、その第一成分がブール値 b₀ と b₁、true の類と false の類でそれぞれ選ばれたものです。以降の推論はこの二つの生のブール値だけに関するものであり、P が機械的に判定できるのはこのためです。二つの補題が、向きごとに一つずつ、この値を P と結びます。代表元が一致すれば、両者の保証が true の類から false の類への道を与え、有効性がそれを P と読みます。P が成り立てば二つの注目点は等しく、g はその等しさを尊重するので、b₀ と b₁ は一致します。

  module _ (g : (x : Glued) → Pick x) where

    b₀ : Bool
    b₀ = g [ true ] .fst

    b₁ : Bool
    b₁ = g [ false ] .fst

最初の補題は、等式 q : b₀ ≡ b₁ を逆方向に読んで P と結びます。三つの道が Glued の中で合成されます。true の類から b₀ の類へ (g [ true ] の保証)、そこから b₁ の類へ (q が cong [_] を通して誘導する類の一致)、さらに false の類へ (g [ false ] の保証)。合成した道は一つの注目すべき類からもう一つへと走り、unglue がそれを ⟨ P ⟩ の証明に変えます。二番目の補題は順方向です。P の証明 p が与えられれば、道 glue p が二点を同一視し、それに沿って g を適用すれば b₀ ≡ b₁ が得られます。両端は生のブール値なので、これは g の直接の射影であり、族の輸送は一切要りません。

    agree→P : b₀ ≡ b₁ → ⟨ P ⟩
    agree→P q = unglue (sym (g [ true ] .snd) ∙ cong [_] q ∙ g [ false ] .snd)

    P→agree : ⟨ P ⟩ → b₀ ≡ b₁
    P→agree p i = g (glue p i) .fst

いまや二つのブール値で P を判定します。P とは違って、ブール値は検査できます。二つのブール値は等しいか等しくないか、機械的に決まります。一致すれば最初の補題が P を証明します。異なれば P は成り立たないはずです。成り立てば二番目の補題が両者の一致を強めるからです。どちらにしても P は判定されます。場合分けは選ばれた二つのブール値の上で行われ、P 自身には触れていません。

判定可能な等式 _≟_ が b₀ と b₁ を比較し、Dec (b₀ ≡ b₁) の元を返します。等式の証明を伴う yes か、反証を伴う no かです。補助関数 fromDec が辞書を通してそれぞれの結果を変換します。yes の場合、等式 q が agree→P に渡り、左の和成分、すなわち ⟨ P ⟩ の証明が得られます。

    decide : ⟨ P ⟩ Sum.⊎ (⟨ P ⟩ → Empty.⊥)
    decide = fromDec (b₀ ≟ b₁)
      where
      fromDec : Dec (b₀ ≡ b₁) → ⟨ P ⟩ Sum.⊎ (⟨ P ⟩ → Empty.⊥)
      fromDec (yes q) = Sum.inl (agree→P q)

no の場合、ne は二つのブール値が等しくありえないことの証明です。P が成り立てば P→agree が両者の等しさを示し、ne と衝突します。そこで右の和成分は、⟨ P ⟩ の任意の証明を受け取り、順方向の補題で b₀ ≡ b₁ を得て、それを ne に渡す関数です。二つの場合合わせて P は判定され、場合分けはブール値のデータの上だけで行われています。

      fromDec (no ne) = Sum.inr (λ p → ne (P→agree p))

定理を組み上げるまでに、まだ一段残っています。選択が渡すのは選択関数ではなく、その単なる存在です。しかし目標「P または P でない」はそれ自身が命題です。両側は互いに排反し、二つの判定の間に区別できるものが何もないからです。そのような目標への消去では、単なる存在は実際の存在であるかのように扱えて、証明が閉じます。

目標が命題であることは明示的に証明されます。Sum.isProp⊎ は両側それぞれの命題性と、両方の元が同時に存在しないことの証明を要求します。第一側は ⟨ P ⟩ で、P .snd により命題です。第二側は関数型 ⟨ P ⟩ → Empty.⊥ であり、isPropΠ が Empty.isProp⊥ を各点で用いて、その命題性を証明します。最後に λ p np → np p が、両側に同時に要素が存在しないことを証明します。定理 choice→lem の型はしたがって SetChoice ℓ → LEM ℓ です。sc と命題 P が与えられると、P について Diaconescu モジュールの中で働き、merePicker sc で単なる選択関数の存在を得て、PT.rec によって証明済みの命題である目標へ切り詰めを消去し、decide を返します。考えの順序が重要です。decide の中の場合分けは本物のデータであり、切り詰めが消去できるのは、目標がその答えたちを区別できないからです。

  decideIsProp : isProp (⟨ P ⟩ Sum.⊎ (⟨ P ⟩ → Empty.⊥))
  decideIsProp = Sum.isProp⊎ (P .snd) (isPropΠ (λ _ → Empty.isProp⊥)) (λ p np → np p)

choice→lem : ∀ {ℓ} → SetChoice ℓ → LEM ℓ
choice→lem sc P = PT.rec decideIsProp decide (merePicker sc)
  where open Diaconescu P

まとめ

一つの固定したレベルの上で、SetChoice が述べるのは次のことです。h-集合の添字の上では、各ファイバーの単なる非空性から、あらゆる点で一度に選ぶ一つの関数の単なる存在が従う。したがって一つ上のレベルの実例がその下のレベルを覆い、ディアコネスクの定理により、そのレベルのすべての命題を判定できます。本章が証明した方向では、選択はより強い古典的インターフェースです。すなわち SetChoice ℓ → LEM ℓ であり、逆はここでは確立されません。モデルの章は、一つの SetChoice (ℓ-suc ℓ) の実例を二通りに使います。choice→lem は ZF の公理に排中律を与え、lowerSetChoice は低いレベルで選択集合の公理を与えます。