累積階層における小さな真理値

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

読書案内 · 依存マップ

累積階層 V ℓ の上で作業をすると、x ∈ˢ a や a ≈ˢ b のような主張が次々に現れます。これらは hProp (ℓ-suc ℓ) の要素としてまとめられた命題であり、集合そのものの添字レベル ℓ より一つ上の宇宙に住みます。上の宇宙の命題はそのままでは不便です。レベル ℓ のデータを要求する構成、たとえばライブラリの分出集合は、それを受け付けられません。そこで、命題 P : hProp (ℓ-suc ℓ) の証明の型がある低い宇宙の命題 Q : hProp ℓ と同値であるとき、P は小さいと呼びます。小ささは P を単純化するのではなく、別の低い命題がまったく同じことを述べているという証明書です。

本章は、大きな真理値を段階的に小さな真理値へ下げます。V の原子的な所属と等号はそのまま小さく、これは各集合が要素を提示する小さな添字の型をもつからです。小ささはすべての結合子を通して保存され、有界量化子も同様です。その量化の範囲はまさにその添字の型だからです。非有界量化子については、範囲そのものが本質的に小さい、つまりレベル ℓ の型と同値である場合に小ささが保たれることを本章で示します。成果は二つあります。命題リサイズなしの Δ₀ 分出と、台が本質的に小さい制限構造の上でのすべての論理式の評価の小ささです。

本章のすべては、モジュール引数によって一度だけ固定される宇宙レベル ℓ のもとで行われます。対象となるのは V.Hierarchy 章の累積階層 V ℓ で、その集合は Type ℓ で添字付けられた族の像です。全体を貫く定義は isSmall です。P : hProp (ℓ-suc ℓ) に対し、isSmall P の要素は、低い宇宙の命題 Q : hProp ℓ と基礎型の間の同値 ⟨ P ⟩ ≃ ⟨ Q ⟩ からなる対です。本章の課題はこのような対を作ることです。舞台となるのは ZFStructure レコード、すなわち台と、真理値を返す等号と所属の関係をひとまとめにしたものです。このレコードをクラスに制限する演算 _↾_ は最終節で使います。

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

open import Base.Prelude

module V.Smallness {ℓ : Level} where

open import Base.Impredicativity using ( isSmall )

下げるべき主張は、一階の形式言語の中にあります。関係記号は所属と等号の _∈̇_ と _≐_、結合子は論理式を組み合わせ、さらに有界量化子 ∀̇∈ と ∃̇∈、非有界量化子 ∀̇ と ∃̇_ があります。Δ₀ のフラグメントは Lévy 階層による論理式の分類です。Δ₀ は論理式上の述語ではなく、その論理式が原子から結合子と有界量化子だけで作られていることの帰納的な証人です。決定的なのは、非有界量化に対応する構成子が存在しないことです。∀̇ や ∃̇_ を含む論理式はそもそも Δ₀ の証人をもてず、本章の Δ₀ 定理はまさにこの不在に依拠します。

open import FOL.ZFStructure using ( ZFStructure; _↾_ )
open import FOL.Syntax
  using ( Formula; _∈̇_; _≐_; _∧̇_; _∨̇_; _⇒̇_; ⊥̇; ∃̇_; ∀̇_; ∀̇∈; ∃̇∈ )
open import FOL.LevyHierarchy
  using ( Δ₀; δ-∈; δ-≐; δ-∧; δ-∨; δ-⇒; δ-⊥; δ-∀∈; δ-∃∈ )

論理式の意味は意味論のモジュールが与え、ここでは V.Hierarchy の構造 𝒮ᵥ で具体化します。つまり、構造としての装備を施した累積階層で、その関係は hProp (ℓ-suc ℓ) に値をとります。したがって本章が扱う真理値は一段上の宇宙の命題であり、まさに isSmall が語る種類のものです。証明はすべて同値の小さな道具立てに依拠します。同値の型 _≃_ とその適用 equivFun、原像 invEq、関数型を通して同値を運ぶ equivΠ、そして二つの命題性の証明と双条件から同値を作る propBiimpl→Equiv。以下の同値はどちらの側も命題なので、この構成子がほとんどの仕事を担います。

import FOL.Semantics
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ )

open import Cubical.Foundations.Equiv
  using ( _≃_; equivFun; invEq; invEquiv; equivΠ; propBiimpl→Equiv )
import Cubical.Functions.Logic as Logic

結合子による保存を示すには、低いレベル ℓ、すなわち圧縮の到達点となる宇宙の命題演算が必要です。これらは限定名 Logic のもとに置かれるので、Logic.⊓ などは明らかに hProp ℓ 上で働き、以下の無修飾の演算は hProp (ℓ-suc ℓ) 上で働きます。残りの部品は個々の同値の構成に役立ちます。Σ-cong-equiv は成分ごとの同値から対の型の間の同値を作り、Sum.⊎-equiv は直和を扱い、tt* は単一元であり、命題的切り詰めのモジュール PT は、証人を選ばずに関数に沿って「存在するだけ」の主張を運ぶ map を与えます。

open import Cubical.Functions.Logic using ( ⇔toPath )
open import Cubical.Data.Sigma using ( Σ-cong-equiv )
import Cubical.Data.Sum as Sum
open import Cubical.Data.Unit using ( tt* )
import Cubical.HITs.PropositionalTruncation as PT

階層そのものが原子的なデータを供給します。各集合 a は単射表示をもち、小さな添字の型 ⟪ a ⟫ と V ℓ への埋め込み ⟪ a ⟫↪ です。すると所属には小さい双子 _∈ₛ_ が伴います。これは対 (m : ⟪ b ⟫, ⟪ b ⟫↪ m ∼ a) 全体の型として定義され、hProp ℓ に住みます。変換 ∈∈ₛ が二つの所属を双方向に結び、identityPrinciple は双相似 ∼ を実際のパスと同一視します。演算 ∈-asFiber は (切り詰められていない) 所属を埋め込みの実際のファイバーに変えます。SeparationSet はライブラリの分出構成であり、すでに低い宇宙に値をもつ述語だけを受け付けます。無修飾の結合子 ⊓ ⊔ ⇒ ¬ ⊤ ⊥ と量化子 ∀[ x ] P x と ∃[ x ] P x は hProp (ℓ-suc ℓ) 上で直接働きます。

open import Cubical.HITs.CumulativeHierarchy.Properties
  using ( _∼_; identityPrinciple; _∈ₛ_; ∈∈ₛ; ⟪_⟫; ⟪_⟫↪; ∈ₛ⟪_⟫↪_; ∈-asFiber )
open import Cubical.HITs.CumulativeHierarchy.Constructions
  using ( module SeparationSet )

構造レコードは 𝒮ᵥ で具体化され、以後 S、_≈ˢ_、_∈ˢ_ という名前はその台と関係を指します。具体的には S は V ℓ です。したがって構造の要素についての主張は一段上の宇宙の命題であり、それが小さいと言えるかどうかこそ、本章が力を注ぐ点なのです。

open ZFStructure 𝒮ᵥ

小さい命題

命題 P : hProp (ℓ-suc ℓ) が小さい、つまり isSmall P が成り立つとは、低い宇宙の命題 Q : hProp ℓ と同値 ⟨ P ⟩ ≃ ⟨ Q ⟩ を備えることです。この定義は Base.Impredicativity で導入され、そこではリサイズのインターフェースがすべての命題について小ささを一括して断言します。本章はそのような仮定を置きません。個々の命題について小ささを獲得し、まず構造の二つの原子関係から始めて、その証人を結合子と量化子を通して運んでいきます。

原子がなぜ小さいのでしょうか。V ℓ の集合は、ある ⟪ a ⟫ : Type ℓ で添字付けられた族の像として作られているからです。「x は a の要素である」とは、ある添字が提示する要素が x と等しいことであり、その主張は小さな型の上で量化します。したがって所属には小さな双子 a ∈ₛ b が伴い、∈∈ₛ が双方向に変換します。等号も同様に、同一性原理を経て双相似 a ∼ b へ圧縮されます。

最初の補題は、小さな所属関係を小ささの証人としてまとめます。isSmall (a ∈ˢ b) を示すには、低い宇宙の命題と ⟨ a ∈ˢ b ⟩ との同値を示す必要があります。証人としては a ∈ₛ b をとります。両方の基礎型が命題なので、propBiimpl→Equiv によって ∈∈ₛ の二つの方向だけで同値が得られます。a や b についての情報は一切使っていません。集合が何であれ、それらの間の所属は小さいのです。この補題が主張しないことも重要です。二つの関係をパスで同一視するのでも、∈ˢ 自身を低い宇宙に落とすのでもなく、圧縮された同値物を供給するだけです。

small-∈ : (a b : S) → isSmall (a ∈ˢ b)
small-∈ a b = (a ∈ₛ b) ,
  propBiimpl→Equiv (snd (a ∈ˢ b)) (snd (a ∈ₛ b))
    (∈∈ₛ {a = a} {b = b} .fst) (∈∈ₛ {a = a} {b = b} .snd)

small-≡ : (a b : S) → isSmall (a ≈ˢ b)

等号の原子は同じ形をしつつ、別の小さな双子を用います。構造の等号 a ≈ˢ b は双相似 a ∼ b、すなわち二つの集合が同じ要素をもつという主張へ圧縮されます。ライブラリの同一性原理は ⟨ a ∼ b ⟩ とパスの型 a ≡ b との間の同値であり、invEquiv がそれを isSmall に必要な方向、すなわち大きな宇宙の等号型 ⟨ a ≈ˢ b ⟩ から低い宇宙の双相似の命題へ向け直します。small-∈ と合わせて、言語の原子の場合はこれで尽くされます。

small-≡ a b = (a ∼ b) , invEquiv identityPrinciple

結合子による保存

原子が揃ったところで、次の問いは、小ささが論理的な組み合わせの下で保たれるかどうかです。答えは肯定です。四つの結合子と二つの定数のそれぞれが小ささの証人を通し、この節が終わった時点で、小さな原子から結合子で作られる真理値はすべて再び小さくなります。これが後で、Δ₀ の証人に関する帰納法が結合子の場合を一括して片付ける理由です。

各証明は二つの小ささの証人 (P' , eP) と (Q' , eQ)、ここでは eP : ⟨ P ⟩ ≃ ⟨ P' ⟩、eQ : ⟨ Q ⟩ ≃ ⟨ Q' ⟩、を受け取り、合成された命題に対する小ささの証人を返します。低い宇宙側の成分は P' と Q' をレベル ℓ の対応する Logic の演算で組み上げ、同値の成分は eP と eQ に沿って合成の証明を輸送します。

連言が最も単純です。P ⊓ Q の基礎の型は対 ⟨ P ⟩ × ⟨ Q ⟩ だからです。二つの圧縮された命題を、基礎の型がやはり積である Logic.⊓ で組み合わせれば、同値は eP と eQ に Σ-cong-equiv を適用して得られます。証明の対を、圧縮された証明の対へ写すだけです。各因子が圧縮できること以外に、命題についての情報は要りません。

small⊓ : {P Q : hProp (ℓ-suc ℓ)} → isSmall P → isSmall Q → isSmall (P ⊓ Q)
small⊓ {P} {Q} (P' , eP) (Q' , eQ) =
  (P' Logic.⊓ Q') , Σ-cong-equiv eP (λ _ → eQ)

small⊔ : {P Q : hProp (ℓ-suc ℓ)} → isSmall P → isSmall Q → isSmall (P ⊔ Q)
small⊔ {P} {Q} (P' , eP) (Q' , eQ) =

選言と含意には、それぞれ一つの考え方が要ります。選言では ⟨ P ⊔ Q ⟩ は直和の命題的切り詰めなので、圧縮された命題 P' Logic.⊔ Q' も切り詰めであり、PT.propTrunc≃ が直和の同値 Sum.⊎-equiv eP eQ を切り詰めへ引き上げます。ここで切り詰めの規律が現れます。この写像はどちら側が成り立つかのラベルを付け替えるだけで、選ばれた側を検査しません。切り詰めは選ばれた側をそもそも提供しないからです。含意では ⟨ P ⇒ Q ⟩ は関数型 ⟨ P ⟩ → ⟨ Q ⟩ であり、圧縮された命題 P' Logic.⇒ Q' はレベル ℓ で同じ形をもち、equivΠ が関数空間を通して同値を各点で運びます。

  (P' Logic.⊔ Q') , PT.propTrunc≃ (Sum.⊎-equiv eP eQ)

small⇒ : {P Q : hProp (ℓ-suc ℓ)} → isSmall P → isSmall Q → isSmall (P ⇒ Q)
small⇒ {P} {Q} (P' , eP) (Q' , eQ) =
  (P' Logic.⇒ Q') , equivΠ eP (λ _ → eQ)

small¬ : {P : hProp (ℓ-suc ℓ)} → isSmall P → isSmall (¬ P)

否定だけは、圧縮された命題だけでは同値が定まりません。否定は反変だからです。¬ P の証明は P の証明を消費します。圧縮された命題は Logic.¬ P' であり、その基礎の型は ⟨ P' ⟩ を空な型へ送ります。両側とも命題なので propBiimpl→Equiv が使え、二つの方向は eP を逆向きに使います。圧縮された反証 p' から np : ¬ P の矛盾を作るには、原像 invEq eP p' を np に適用し、逆に p : ⟨ P ⟩ の像 equivFun eP p を np' に渡します。同値の適用と逆が、否定の論理の要求どおり、正反対の変動で現れます。

small¬ {P} (P' , eP) = (Logic.¬ P') ,
  propBiimpl→Equiv (snd (¬ P)) (snd (Logic.¬ P'))
    (λ np p' → np (invEq eP p'))
    (λ np' p → np' (equivFun eP p))

small⊤ : isSmall ⊤

最後の二つの定数でこの節を閉じます。真が小さいのは、両側とも要素をもつ命題だからです。圧縮された命題は Logic.⊤ であり、どちらの方向の関数も引数を捨てて単一元 tt* を返します。偽は少し違う始まり方をします。真理値 ⊥ はもともと hProp の対 (⊥* , isProp⊥*) として定義されているので、その基礎の型は空な型 ⊥* そのものであり、圧縮された命題も同じ空な型を hProp にまとめたものです。したがって両方の関数は背理で定義されます。空な型の引数には場合分けが存在しないのです。

small⊤ = Logic.⊤ ,
  propBiimpl→Equiv (⊤ .snd) (snd (Logic.⊤ {ℓ}))
    (λ _ → tt*) (λ _ → tt*)

small⊥ : isSmall (⊥ {ℓ = ℓ-suc ℓ})
small⊥ = (⊥* , isProp⊥*) ,

両方向の背理的な場合分け (λ ()) こそが、偽の証明の内容のすべてです。⊥* には構成子がないため、そこからの関数には定義のための節が一切要りません。これは、構成子の不在が実際の論理的仕事をする、というテーマの最初の登場であり、Δ₀ の節で強い形で再登場します。

  propBiimpl→Equiv isProp⊥* isProp⊥* (λ ()) (λ ())

有界量化子による保存

結合子だけでは量化子を含まない真理値しか扱えず、論理式に有界量化子が一つ現れただけで次節の帰納は途絶えます。この節はその障害を取り除きます。V ℓ 全体を範囲とする量化子は大きな台 S : Type (ℓ-suc ℓ) 上で量化するため、ここまでの構成だけではその真理値を圧縮できません。一方、集合 a で有界な量化子は、意味論の上では a の要素の上だけで量化します。その要素は小さな添字の型で提示されています。単射表示は a を sett ⟪ a ⟫ ⟪ a ⟫↪ として与え、⟪ a ⟫ : Type ℓ です。そこで ⟪ a ⟫ 上で量化すれば、得られる真理値は小さな命題 sm (⟪ a ⟫↪ m) を Π または切り詰められた Σ で組み合わせたものになり、どちらも圧縮できます。

二つの量化を結ぶ橋が ∈-asFiber です。x ∈ᵗ a の要素から、⟪ a ⟫↪ の x 上の実際のファイバー、すなわち添字 m とパス ⟪ a ⟫↪ m ≡ x の対を返します。このファイバーは切り詰められていません。⟪ a ⟫↪ が埋め込みだからです。a の要素から ⟪ a ⟫ の添字を取り戻すのは関数であって、選択ではありません。だから二つの補題の逆方向は、いかなる選択もなしに進みます。

全称の有界量化子は、a のすべての要素 x に対して命題 B x が成り立つと述べます。その真理値は ∀[ x ] (x ∈ˢ a) ⇒ B x で、台全体にわたって索引付けされた含意であり、前件 x ∈ˢ a が注意を要素に限定します。補題は各 B x が小さいこと、証人 sm x = (B' x , e x) を仮定し、全称の主張全体が小さいと結論します。圧縮された命題は、所属をその小さな双子で、台を ⟪ a ⟫ で置き換え、すべての添字 m : ⟪ a ⟫ に対して命題 B' (⟪ a ⟫↪ m) が成り立つと述べます。限界 a は明示的な引数として現れ、族 B は暗黙のままで目標の型から決まります。

small-∀∈ : (a : S) {B : S → hProp (ℓ-suc ℓ)}
         → (∀ x → isSmall (B x))
         → isSmall (∀[ x ∶ S ] (x ∈ˢ a) ⇒ B x)
small-∀∈ a {B} sm = Qsm , propBiimpl→Equiv (snd big) (snd Qsm) fwd bwd
  where

順方向は、もとの主張の証明を圧縮された命題の証明へ変換します。各 x に x ∈ˢ a から B x への含意を割り当てる f が与えられたとき、各添字 m に対して B' (⟪ a ⟫↪ m) の証明を作ります。まず要素 ⟪ a ⟫↪ m で f を適用します。これには前件、つまり ⟪ a ⟫↪ m が a の要素である証明が要りますが、変換 ∈∈ₛ が正準な証人 ∈ₛ⟪ a ⟫↪ m、すなわち添字と ∼ の反射性の対からこれを与えます。得られた B (⟪ a ⟫↪ m) の証明は、同値 e を通されて圧縮された命題に落ち着きます。

  big = ∀[ x ∶ S ] (x ∈ˢ a) ⇒ B x
  Qsm = ∀[ m ∶ ⟪ a ⟫ ] sm (⟪ a ⟫↪ m) .fst
  fwd : ⟨ big ⟩ → ⟨ Qsm ⟩
  fwd f m = equivFun (sm (⟪ a ⟫↪ m) .snd)
                     (f (⟪ a ⟫↪ m) (∈∈ₛ {a = ⟪ a ⟫↪ m} {b = a} .snd (∈ₛ⟪ a ⟫↪ m)))

逆方向で埋め込みが真価を発揮します。各添字 m に B' (⟪ a ⟫↪ m) の証明を割り当てる g が与えられたとき、x∈a : x ∈ᵗ a を満たす各 x に対して B x の証明を作ります。ファイバー mf = ∈-asFiber x∈a は、添字 mf .fst とパス mf .snd : ⟪ a ⟫↪ (mf .fst) ≡ x を与えます。その添字で g を適用すれば B' (⟪ a ⟫↪ (mf .fst)) の証明が得られ、逆の同値がそれを B (⟪ a ⟫↪ (mf .fst)) へ送り、subst がパス mf .snd に沿って B x へ輸送します。調整を行うのは、要素の間の任意の選択ではなくパスです。ファイバーが切り詰められていればこの輸送は不可能で、追加の仮定なしには補題は成り立ちません。

  bwd : ⟨ Qsm ⟩ → ⟨ big ⟩
  bwd g x x∈a =
    subst (λ v → ⟨ B v ⟩) (mf .snd)
          (invEq (sm (⟪ a ⟫↪ (mf .fst)) .snd) (g (mf .fst)))
    where mf = ∈-asFiber {a = x} {b = a} x∈a

存在の有界量化子は、a のある要素 x が B x を満たすと述べます。その真理値は ∃[ x ] (x ∈ˢ a) ⊓ B x、すなわち所属と B の切り詰められた組み合わせであり、圧縮された命題は、B' (⟪ a ⟫↪ m) を満たす添字 m : ⟪ a ⟫ が存在するとだけ主張します。仮定と結論は全称の場合と鏡像ですが、証明の性質は異なります。両側とも切り詰められた存在主張なので、どちらの方向も関数を返さず、切り詰めを切り詰めへ写します。

small-∃∈ : (a : S) {B : S → hProp (ℓ-suc ℓ)}
         → (∀ x → isSmall (B x))
         → isSmall (∃[ x ∶ S ] (x ∈ˢ a) ⊓ B x)
small-∃∈ a {B} sm = Qsm , propBiimpl→Equiv (snd big) (snd Qsm) fwd bwd
  where

順方向では、PT.map が切り詰めの内部で各点の構成を適用します。これは、目標である圧縮された命題が再び命題であるために許されます。各点の段階は、切り詰められた三つ組 (x , x∈a , bx)、すなわち要素、その所属の証拠、B x の証明をほどきます。これが正当なのは、切り詰めの内側で行われるからであり、x の選択を外へ取り出す必要は一度もありません。次に x∈a のファイバーが添字を与え、証明 bx はファイバーのパスに沿って sym (mf .snd) の向きに輸送され、それから同値で圧縮されます。全称の順方向と比べてください。あちらでは関数がはじめから手にあり、こちらではそのようなデータが存在するとしか知りません。

  big = ∃[ x ∶ S ] (x ∈ˢ a) ⊓ B x
  Qsm = ∃[ m ∶ ⟪ a ⟫ ] sm (⟪ a ⟫↪ m) .fst
  fwd : ⟨ big ⟩ → ⟨ Qsm ⟩
  fwd = PT.map λ where
    (x , x∈a , bx) →

逆方向でも、やはり PT.map の下で、添字と B' (⟪ a ⟫↪ m) の証明の切り詰められた対 (m , q) が、性質 B をもつ a の要素へ変換されます。要素は ⟪ a ⟫↪ m であり、その所属の証拠は正準な証人への ∈∈ₛ の適用から、性質の証明は原像 invEq (sm _ .snd) q から得られます。ここでは輸送はまったく要りません。添字は最初から与えられており、要素から取り戻す必要がないからです。二つの方向の非対称性はそのままデータの非対称性です。一方は添字をはじめから持ち、他方は要素から添字を作り出さねばならず、埋め込みだけがその作り出しを関数にします。

      let mf = ∈-asFiber {a = x} {b = a} x∈a
      in mf .fst ,
         equivFun (sm (⟪ a ⟫↪ (mf .fst)) .snd)
                  (subst (λ v → ⟨ B v ⟩) (sym (mf .snd)) bx)
  bwd : ⟨ Qsm ⟩ → ⟨ big ⟩

この一対の補題で、意味論の有界量化子の節はすべて賄われ、次節の帰納は量化子がすべて有界であるどんな論理式も通過できます。使わなかったものに注目してください。どちらの証明にも古典的な原理も選択もリサイズも現れません。実質的に使ったのは、所属の単射表示と、⟪ a ⟫↪ が埋め込みであるという事実だけです。

  bwd = PT.map λ where
    (m , q) → ⟪ a ⟫↪ m , ∈∈ₛ {a = ⟪ a ⟫↪ m} {b = a} .snd (∈ₛ⟪ a ⟫↪ m)
            , invEq (sm (⟪ a ⟫↪ m) .snd) q

小ささから分出へ

この節は、小ささが実を結ぶ場所です。ライブラリの分出構成 SeparationSet は、集合 a と、低い宇宙に値をもつ述語 ϕ : V ℓ → hProp ℓ に対して、a の要素のうち ϕ を満たすもの全体を要素とする集合を作ります。上の宇宙に値をもつ述語では、内部の添字の型がレベル ℓ に属さねばならないため、このような構成は不可能です。下の補題はその適合装置です。各点で小ささの証人をもつ S 上の述語 P が与えられれば、構造の中の集合 s と、所属の仕様「y ∈ˢ s は y ∈ˢ a かつ P y とちょうど同じ」とを、モデルの record の分出フィールドと同じ形式のパスとして返します。

ここで部品が計画へ組み上がります。述語の小ささが最初にどこから供給されるかに関わりなく、前節の有界量化子であれ、最後の本質的に小さな世界であれ、この補題は小さな述語を一度だけ、同じ方法で集合へ変えます。

この主張は注意して読む価値があります。結果は依存対です。構造の集合 s と、各 y に対する hProp (ℓ-suc ℓ) におけるパス (y ∈ˢ s) ≡ ((y ∈ˢ a) ⊓ P y) であり、基礎の命題の間の双条件ではありません。これはモデルの record の分出フィールドの形と一致するため、この構成は分出公理を検証すべきどんな構造にも移植できます。証明は、ライブラリの構成を a と圧縮された述語に適用し、得られた仕様の二つの方向から必要なパスを組み上げます。

separateFromSmall : (a : S) (P : S → hProp (ℓ-suc ℓ))
                  → (∀ y → isSmall (P y))
                  → Σ[ s ∈ S ] (∀ y → (y ∈ˢ s) ≡ ((y ∈ˢ a) ⊓ P y))
separateFromSmall a P sm = Sep.SEPAREE , λ y → ⇔toPath (fwd y) (bwd y)
  where

まず圧縮された述語を組み立てます。ϕₛ y は定義により、各点の小ささの証人から取り出した低い宇宙の代替物 sm y .fst です。次にライブラリのモジュール Sep を a と ϕₛ で具体化し、その結果の集合を Sep.SEPAREE とします。本章でライブラリの分出が使われるのはここだけです。この部でほかに分出するものはすべてこの補題を通ります。

  ϕₛ : S → hProp ℓ
  ϕₛ y = sm y .fst
  module Sep = SeparationSet a ϕₛ
  fwd : ∀ y → ⟨ y ∈ˢ Sep.SEPAREE ⟩ → ⟨ (y ∈ˢ a) ⊓ P y ⟩
  fwd y y∈s = ∈∈ₛ {a = y} {b = a} .snd (Sep.separation-ax y .fst y∈ₛs .fst)

両方向とも、構造の所属 y ∈ˢ Sep.SEPAREE と「y ∈ˢ a かつ P y」との間を翻訳します。順方向では、∈∈ₛ で y∈s を小さな所属へ変換し、ライブラリの仕様 separation-ax y の順方向へ渡して、y ∈ₛ a と圧縮された性質の対を得ます。第一成分は逆の向きの ∈∈ₛ で y ∈ᵗ a へ戻し、第二成分は同値 e の逆で展開します。逆方向はその鏡像です。a での所属を小さな形へ変換し、equivFun で性質の証明を圧縮し、separation-ax y の逆方向に Sep.SEPAREE への所属を作らせ、もう一度 ∈∈ₛ で変換します。集合論の仕事をするのはライブラリの仕様であり、宇宙レベルの帳簿づけをするのは同値です。

            , invEq (sm y .snd) (Sep.separation-ax y .fst y∈ₛs .snd)
    where y∈ₛs = ∈∈ₛ {a = y} {b = Sep.SEPAREE} .fst y∈s
  bwd : ∀ y → ⟨ (y ∈ˢ a) ⊓ P y ⟩ → ⟨ y ∈ˢ Sep.SEPAREE ⟩
  bwd y yp = ∈∈ₛ {a = y} {b = Sep.SEPAREE} .snd (Sep.separation-ax y .snd
               (∈∈ₛ {a = y} {b = a} .fst (yp .fst) , equivFun (sm y .snd) (yp .snd)))

Δ₀ 論理式の評価は小さい

ここまでの節で、小ささの証人の備えができました。原子二つ、結合子四つ、定数二つ、有界量化子二つです。この節は、その備えを Δ₀ の証人自身に関する帰納法で定理へ変えます。Lévy 階層の章で思い出されるように、Δ₀ は帰納的な証人であり、論理式ごとに一つ、その構成子はその論理式が原子から結合子と有界量化子だけで作られていることを証明します。定理は、そのような証人をもつ論理式の真理値がどの環境でも小さいと述べます。証人は帰納的に定義されるので、証明は構成子ごとに一つの場合を持つ帰納法であり、それぞれの場合がまさに備えられた補題の一つです。

場合分けには示唆的な省略があります。非有界量化子 ∀̇ と ∃̇_ の場合は存在しません。証人の型にその構成子がないからです。構成子の不在こそが分類を実現しており、非有界量化子を含む論理式はそもそも Δ₀ の証人をもてないので、帰納法がそれに直面することは決してありません。こうして Lévy 階層は宇宙のコストの計算として機能します。Δ₀ は、そのコストなしに真理値が手に入る、まさにそのフラグメントなのです。

準備として、意味論を一度だけ具体化します。SemanticsV は 𝒮ᵥ 上の、真理値を hProp (ℓ-suc ℓ) にとる充足関係であり、したがって論理式の真理値は、この章がずっと圧縮してきた種類の命題そのものです。環境の型 S ^ n は長さ n のベクトルの記法です。モジュールは定数解釈 ι : K → S でパラメータ化されるので、定理は定数のどんな選び方に対しても成り立ちます。恒等写像という正準な場合は章の末尾で取られます。内部の open SemanticsV.At K ι は、項の評価 ⟦_⟧ と充足 _⊨_ をスコープに入れます。目標の型に注意してください。Δ₀-small は、Δ₀ の証人から、各環境 γ に対する γ ⊨ φ の小ささの証人への関数です。帰納法は証人に対して行われ、論理式と環境はその周りで全称化されています。

module SemanticsV = FOL.Semantics 𝒮ᵥ
open SemanticsV using ( _^_ )

module Δ₀Small {ℓc} {K : Type ℓc} (ι : K → S) where

  open SemanticsV.At K ι

  Δ₀-small : ∀ {n} {φ : Formula K n} → Δ₀ φ → (γ : S ^ n) → isSmall (γ ⊨ φ)

原子の場合は、環境 γ で二つの項を評価したうえで、備えられた最初の二つの補題を直接呼びます。所属は t と u の値への small-∈ の適用に、等号は small-≡ になります。三つの二項結合子の場合も同じく直接です。帰納法の仮定 Δ₀-small c γ と Δ₀-small d γ が部分論理式の真理値の小ささの証人であり、対応する結合子の閉包補題がそれらを組み合わせます。明示的な具体化 {P = γ ⊨ φ} は、証人がどの命題を圧縮するかを記録するだけです。Agda は推論できますが、書き出すことで場合の形が文書化されます。

  Δ₀-small (δ-∈ {t = t} {u}) γ = small-∈ (⟦ t ⟧ γ) (⟦ u ⟧ γ)
  Δ₀-small (δ-≐ {t = t} {u}) γ = small-≡ (⟦ t ⟧ γ) (⟦ u ⟧ γ)
  Δ₀-small (δ-∧ {φ = φ} {ψ} c d) γ =
    small⊓ {P = γ ⊨ φ} {Q = γ ⊨ ψ} (Δ₀-small c γ) (Δ₀-small d γ)
  Δ₀-small (δ-∨ {φ = φ} {ψ} c d) γ =

残る結合子の形の場合は偽であり、次いで二つの有界量化子です。偽には環境がまったく要りません。証人 δ-⊥ は部分論理式を運ばず、この場合はただ small⊥ です。有界量化子の場合が興味の対象です。δ-∀∈ では論理式は ∀̇∈ t φ であり、その真理値は ∀[ x ] (x ∈ˢ ⟦ t ⟧ γ) ⇒ ((x ∷ γ) ⊨ φ) です。これは small-∀∈ が消費する形状そのものであり、a は t の値、族 B x は拡張された環境 x ∷ γ での本体の真理値です。帰納法の仮定は拡張された環境で適用されます。証人 c が証明するのは本体 φ 自身なので、これは正当です。

    small⊔ {P = γ ⊨ φ} {Q = γ ⊨ ψ} (Δ₀-small c γ) (Δ₀-small d γ)
  Δ₀-small (δ-⇒ {φ = φ} {ψ} c d) γ =
    small⇒ {P = γ ⊨ φ} {Q = γ ⊨ ψ} (Δ₀-small c γ) (Δ₀-small d γ)
  Δ₀-small δ-⊥ γ = small⊥
  Δ₀-small (δ-∀∈ {t = t} {φ = φ} c) γ =

存在の有界量化の場合は全称の場合と正確に鏡像で、small-∀∈ の代わりに small-∃∈ を使い、連言の形の真理値 ∃[ x ] (x ∈ˢ ⟦ t ⟧ γ) ⊓ ((x ∷ γ) ⊨ φ) を small-∃∈ の結論に合わせます。これで帰納法は閉じます。証人の型のすべての構成子に場合があり、すべての場合が備えられた補題の一つであり、非有界量化子に残る場合はありません。定理 Δ₀-small は、ここでこれまでの節が孤立した事実から、形式言語についての主張へと変わる地点なのです。

    small-∀∈ (⟦ t ⟧ γ) {B = λ x → (x ∷ γ) ⊨ φ} (λ x → Δ₀-small c (x ∷ γ))
  Δ₀-small (δ-∃∈ {t = t} {φ = φ} c) γ =
    small-∃∈ (⟦ t ⟧ γ) {B = λ x → (x ∷ γ) ⊨ φ} (λ x → Δ₀-small c (x ∷ γ))

命題リサイズを要しない Δ₀ 分出

前節の帰納法と、その前の節の適合装置を合成すれば、本章の中心定理が現れます。正準な定数解釈、すなわち言語の定数が構造の集合そのものであり ι が恒等写像である場合をとります。このとき自由変数を一つもつ Δ₀ 論理式 φ は S 上の各点で小さい述語を定義し、separateFromSmall がそれを集合へ変えます。結果は、Δ₀ 論理式に制限された分出公理図式の完全な実例であり、命題リサイズの原理も古典的公理も選択も一切使わずに証明されます。小ささは帰納法が供給し、残りはライブラリの構成が担います。モデルの章はまだ制限なしの分出公理を証明する必要がありますが、この定理は、Lévy 階層の Δ₀ の階層が V の表示以外に何も要しないことを示しています。

冒頭の二行は正準な解釈を固定します。Δ₀Small id が恒等写像で帰納法を具体化し、自由変数一つの充足関係が _⊨_ として再エクスポートされます。定理の型は、任意の述語の代わりに φ を入れた分出の仕様です。すなわち集合 s で、各 y に対して s への所属が、真理値として、a への所属と「一点環境 y ∷ [] で y が φ を満たす」との連言に等しいもの。証明は separateFromSmall の一度の適用であり、述語 λ y → (y ∷ []) ⊨ φ とその各点の小ささ、すなわちすべての一点環境での Δ₀-small c の適用を渡すだけです。ほかに何も介在しません。Δ₀ の証人 c は帰納法によってちょうど一度消費されるのです。

open Δ₀Small id
open SemanticsV.At S id using ( _⊨_ )

separateΔ₀ : (a : S) (φ : Formula S 1) → Δ₀ φ
           → Σ[ s ∈ S ] (∀ y → (y ∈ˢ s) ≡ ((y ∈ˢ a) ⊓ ((y ∷ []) ⊨ φ)))
separateΔ₀ a φ c = separateFromSmall a (λ y → (y ∷ []) ⊨ φ) (λ y → Δ₀-small c (y ∷ []))

本質的に小さな世界

Δ₀ の定理は、すべての量化子をあたかも V ℓ 全体の上で量化するかのように評価しました。小ささの最後のこの層は、量化の位置を変えることで、そのコストさえも取り払います。上のレベルの型 A が、小さな型 X : Type ℓ からの同値 e : X ≃ A を備えているとします。すると A の上での量化は、段階的に X の上での量化へ置き換えられます。A の要素 a についての主張は、その原像 equivFun e m で読めばよいのです。有界量化子の補題は関連するが別の現象です。あそこでの範囲は集合を提示する添字の型であり、所属がふるいの役を果たしました。ここでは有界性の仮定がまったく残りません。小ささは論理式の形ではなく、それが語られる世界の形によって担われるのです。仮定の向きに注意してください。断言されているのは X から A への同値 e が存在することであり、A 自身は依然として上の宇宙に住みます。

まず全称の方です。主張 ∀[ x ] P x B は A 全体の上で量化しますが、圧縮された命題は代わりに X の上で量化し、すべての m : X に対して圧縮された命題 sm (equivFun e m) .fst が成り立つと述べます。e が同値なので、X 上の量化と A 上の量化は同値な依存関数型を与えます。同値の成分は証明の族 f : ∀ m → ⟨ sm (e m) ⟩ を ∀ a → ⟨ B a ⟩ へ運び、各点でさらに同値と合成し、invEquiv が目標の型の求めどおり、小さな Π から大きな Π へと向きを定めます。small-∀∈ との対比に注意してください。あちらでは前件 x ∈ˢ a がふるいの役を果たしましたが、こちらには前件がなく、同値だけが化約の役を担います。

small-∀ : {A : Type (ℓ-suc ℓ)} {X : Type ℓ} (e : X ≃ A) {B : A → hProp (ℓ-suc ℓ)}
        → (∀ a → isSmall (B a))
        → isSmall (∀[ a ∶ A ] B a)
small-∀ {X = X} e sm = (∀[ m ∶ X ] sm (equivFun e m) .fst)
  , invEquiv (equivΠ e (λ m → invEquiv (sm (equivFun e m) .snd)))

存在の方も同じ計画に従いますが、関数型の代わりに切り詰めが現れます。圧縮された命題は、X の上の小さな証人の切り詰められた Σ です。同値は、A の上の大きな証人の切り詰められた Σ から、Σ-cong-equiv によって得られます。これは対の基底を e に沿って A から X へ変え、各ファイバーを逆向きの各点の同値に沿って変え、PT.propTrunc≃ がさらにその対の同値を切り詰めへ引き上げます。ここでも invEquiv が必要な向きを与えます。二つの補題を合わせると、本質的に小さな型の上での量化は小ささを保存する、ということになります。そして次のコード塊で、本質的に小さいとはレベル ℓ の型と同値であることを意味します。

small-∃ : {A : Type (ℓ-suc ℓ)} {X : Type ℓ} (e : X ≃ A) {B : A → hProp (ℓ-suc ℓ)}
        → (∀ a → isSmall (B a))
        → isSmall (∃[ a ∶ A ] B a)
small-∃ {X = X} e sm = (∃[ m ∶ X ] sm (equivFun e m) .fst)
  , invEquiv (PT.propTrunc≃ (Σ-cong-equiv e (λ m → invEquiv (sm (equivFun e m) .snd))))

帰結は次のとおりです。本質的に小さな制限された構造の上では、Δ₀ の証人がなくても、すべての論理式の評価が小さくなります。構造の上のクラス M を固定し、その制限された台が本質的に小さい、すなわち X : Type ℓ を用いた同値 e : X ≃ (Σ[ x ∈ S ] (x ∈ᶜ M)) の形で仮定します。構造 𝒮ᵥ ↾ M の中では、量化子はその制限された台の上で量化するので、前のコード塊の二つの補題は、有界かどうかにかかわらず、すべての量化子に適用できます。原子は第一射影を通して V の原子的な小ささに帰着します。有界性は論理式に対する構文上の制限であり、本質的な小ささは量化範囲の性質です。後者の仮定があれば、構造帰納法は非有界量化子と有界量化子の両方を扱えます。この内部充足の小ささこそ、可定義性の段階、たとえば構成可能階層が各段階で踏む那段階が、低い宇宙の述語で動けるようにするものです。

モジュールの引数が小さな世界を組み立てます。M は台 S 上のクラスで、真クラスであってもかまいません。大きさの制限は一切ありません。仮定は、小さな型 X : Type ℓ と、X から制限された台 Σ[ x ∈ S ] (x ∈ᶜ M) への同値との組であり、これが世界が本質的に小さいということの正確な意味です。負担はこの同値が存在することにあり、M が何らかの内部的な意味で有界であることにはありません。定数は ι : K → Σ[ x ∈ S ] (x ∈ᶜ M) によって制限された台の中で解釈され、したがって各定数は、第二成分が「第一成分が M に属する」ことの証拠であるような対を指します。

module InnerSmall (M : S → hProp (ℓ-suc ℓ))
                  (X : Type ℓ) (e : X ≃ (Σ[ x ∈ S ] (x ∈ᶜ M)))
                  {ℓc} {K : Type ℓc}
                  (ι : K → Σ[ x ∈ S ] (x ∈ᶜ M)) where

  SM : Type (ℓ-suc ℓ)

二つの略記が記法を固定します。SM は制限された台そのものの名前であり、𝒮M は _↾_ によって M に制限された構造です。その台は SM であり、h-集合性は受け継がれ、二つの関係は第一射影に沿って引き戻されるので、世界の中の等号と所属は V の基礎となる集合で決まります。意味論のモジュールは 𝒮M で具体化され、充足と項の評価の記法は上付き添え字に改名されて、論理式が世界の内側で読まれていることを示します。この改名は public にエクスポートされ、他の章ではこれらの名前で制限された充足を読めます。

  SM = Σ[ x ∈ S ] (x ∈ᶜ M)

  𝒮M : ZFStructure (ℓ-suc ℓ)
  𝒮M = 𝒮ᵥ ↾ M

  module SemanticsM = FOL.Semantics 𝒮M
  open SemanticsM.At K ι renaming ( _⊨_ to _⊨ᵐ_ ; ⟦_⟧ to ⟦_⟧ᵐ ) public

定理の主張は、意図的に Δ₀-small と並行しています。任意のアリティ n の論理式 φ と、制限された要素の任意の環境 δ : SM ^ n に対して、真理値 δ ⊨ᵐ φ は小さい。ここに帰納的な証人は姿を見せません。必要ないからです。ここの帰納法は論理式そのものに対して行われ、台の本質的な小ささが Δ₀ の制限の代わりをします。原子の二つの場合は、世界の中で項を評価して制限された要素を得て、その第一射影に原子的な小ささの補題を適用します。世界の中の所属 (fst xm) ∈ˢ (fst ym) は、周囲の構造の命題そのものであり、その小ささはすでに知られています。

  ⊨ᵐ-small : ∀ {n} (φ : Formula K n) (δ : SM ^ n) → isSmall (δ ⊨ᵐ φ)
  ⊨ᵐ-small (t ∈̇ u)  δ = small-∈ (fst (⟦ t ⟧ᵐ δ)) (fst (⟦ u ⟧ᵐ δ))
  ⊨ᵐ-small (t ≐ u)  δ = small-≡ (fst (⟦ t ⟧ᵐ δ)) (fst (⟦ u ⟧ᵐ δ))
  ⊨ᵐ-small (φ ∧̇ ψ)  δ =
    small⊓ {P = δ ⊨ᵐ φ} {Q = δ ⊨ᵐ ψ} (⊨ᵐ-small φ δ) (⊨ᵐ-small ψ δ)

三つの二項結合子と偽は、まったく同じように通ります。閉包補題 small⊓、small⊔、small⇒ と定数 small⊥ は、消費する命題に関してレベルに対して汎用的なので、世界の中で読まれた真理値にもそのまま適用できます。これこそ、先の節でそれらを独立に切り出した意味です。あれらの証明は V 固有の何かには触れず、hProp (ℓ-suc ℓ) にだけ言及していたのです。

  ⊨ᵐ-small (φ ∨̇ ψ)  δ =
    small⊔ {P = δ ⊨ᵐ φ} {Q = δ ⊨ᵐ ψ} (⊨ᵐ-small φ δ) (⊨ᵐ-small ψ δ)
  ⊨ᵐ-small (φ ⇒̇ ψ)  δ =
    small⇒ {P = δ ⊨ᵐ φ} {Q = δ ⊨ᵐ ψ} (⊨ᵐ-small φ δ) (⊨ᵐ-small ψ δ)
  ⊨ᵐ-small ⊥̇        δ = small⊥

次に量化子で、世界の二つの補題が登場します。非有界の存在量化子 ∃̇ φ の真理値は、制限された台の上の ∃[ xm ] (xm ∷ δ) ⊨ᵐ φ であり、帰納法の仮定が各ファイバー (xm ∷ δ) ⊨ᵐ φ の小ささを与えます。これは small-∃ の形状そのものであり、A に制限された台を、e にその小ささの同値を入れれば、この場合は直接の適用で閉じます。全称の場合は small-∀ を用いた鏡像です。量化が本当に制限された世界の上で行われていることに注意してください。SM の要素は対なので、拡張された環境 xm ∷ δ は制限された要素全体による拡張であり、本体はそれらの上で読まれます。

  ⊨ᵐ-small (∃̇ φ)    δ =
    small-∃ e {B = λ xm → (xm ∷ δ) ⊨ᵐ φ} (λ xm → ⊨ᵐ-small φ (xm ∷ δ))
  ⊨ᵐ-small (∀̇ φ)    δ =
    small-∀ e {B = λ xm → (xm ∷ δ) ⊨ᵐ φ} (λ xm → ⊨ᵐ-small φ (xm ∷ δ))
  ⊨ᵐ-small (∀̇∈ t φ) δ =

有界量化子は、それぞれの場合で小ささの二つの源泉を結合します。∀̇∈ t φ の真理値は、制限された台の上で有界な含意 ∀[ xm ] (fst xm ∈ˢ ⟦ t ⟧ᵐ δ) ⇒ ((xm ∷ δ) ⊨ᵐ φ) です。前件の小ささは原子的な補題から、後件の小ささは帰納法の仮定から得られ、small⇒ が含意を組み立てます。主張全体は、さらに e に沿う small-∀ によって小さくなります。興味深い細部は第一射影 fst xm です。有界性は、制限された要素の基礎となる集合についての主張です。世界の所属関係は V のそれの引き戻しだからです。

    small-∀ e {B = λ xm → (fst xm ∈ˢ fst (⟦ t ⟧ᵐ δ)) ⇒ ((xm ∷ δ) ⊨ᵐ φ)} (λ xm →
      small⇒ {P = fst xm ∈ˢ fst (⟦ t ⟧ᵐ δ)} {Q = (xm ∷ δ) ⊨ᵐ φ}
        (small-∈ (fst xm) (fst (⟦ t ⟧ᵐ δ))) (⊨ᵐ-small φ (xm ∷ δ)))
  ⊨ᵐ-small (∃̇∈ t φ) δ =
    small-∃ e {B = λ xm → (fst xm ∈ˢ fst (⟦ t ⟧ᵐ δ)) ⊓ ((xm ∷ δ) ⊨ᵐ φ)} (λ xm →

存在の有界量化の場合は双対の合成です。真理値は切り詰められた Σ の下で有界性と本体を対にし、small⊓ が二つの小ささの証人を組み合わせ、small-∃ が主張全体を小さな添字の型の上へ移します。この場合で帰納法は完了し、本章のもう一つの主要な結果が立ちます。本質的に小さな世界の中では、非有界量化子を含むすべての論理式が小さな真理値をもつのです。Δ₀ の小ささは論理式の形が担い、本質的な小ささは量化子の範囲が担います。どちらであっても、小さな述語が手もとにあれば、前節の分出がそのまま適用されます。

      small⊓ {P = fst xm ∈ˢ fst (⟦ t ⟧ᵐ δ)} {Q = (xm ∷ δ) ⊨ᵐ φ}
        (small-∈ (fst xm) (fst (⟦ t ⟧ᵐ δ))) (⊨ᵐ-small φ (xm ∷ δ)))

まとめ

小ささとは、一段低い宇宙の命題との同値です (isSmall)。V の原子的な所属と等号は、ライブラリの単射表示を通して圧縮されます。四つの結合子と二つの定数は、対応する低いレベルの演算を通して小ささの証人を運び、有界量化子は、集合の小さな添字の型の上での量化によって圧縮されます。その際に使われるのは、埋め込みの切り詰められていないファイバーです。適合装置 separateFromSmall は、各点で小さいどんな述語も、分出の仕様を備えた集合へ変えます。帰納法 Δ₀-small は Lévy 階層の Δ₀ の階層をそのまま与え、separateΔ₀ は命題リサイズも古典的な公理も選択も要らない Δ₀ 分出へ変えます。Δ₀ の外の論理式にはさらに多くが要り、モデルの章が命題リサイズという名のもとでそれを供給します。最後の節は第二の道を加えました。台が本質的に小さい、つまりレベル ℓ の型と同値である世界の中ではすべての論理式の評価が小さく、これが可定義性の段階を低い宇宙の述語で動かせるようにする理由です。