この章を読むか、対話型目次と依存グラフで別のルートを選べます。

対話型目次 · 依存グラフ

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

module V.Smallness {ℓ : Level} where

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

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

open import Cubical.HITs.PropositionalTruncation using ( propTrunc≃ )
open import Cubical.Data.Sigma using ( Σ-cong-equiv )
open import Cubical.Data.Sum using ( ⊎-equiv )

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

論理式の意味は意味論のモジュールが与え、ここでは V.Hierarchy の構造 𝒮ᵥ で具体化する。つまり、構造としての装備を施した累積階層で、その関係は hProp (ℓ-suc ℓ) に値をとる。したがって本章が扱う真理値は一段上の宇宙の命題であり、まさに hasSize が語る種類のものである。証明では、これらの命題と低いレベルの代表の間に型同値を構成する。順写像と逆写像の適用に加え、invEquiv で同値の向きを反転し、equivΠ で関数型へ同値を拡張する。命題については、propBiimpl→Equiv が両側の命題性の証明と双方向の含意から同値を構成する。以下の同値はどちらの側も命題なので、この構成子がほとんどの仕事を担う。

open import Cubical.Foundations.Equiv
  using ( invEquiv; equivΠ; propBiimpl→Equiv )

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

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

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

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

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

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

等号の原子は同じ形をしつつ、別の小さな双子を用いる。構造の等号 a ≈ˢ b は双相似 a ∼ b、すなわち二つの集合が同じ要素をもつという主張へ圧縮される。ライブラリの同一性原理は ⟨ a ∼ b ⟩ とパスの型 a ≡ b との間の同値であり、invEquiv がそれを hasSize に必要な方向、すなわち大きな宇宙の等号型 ⟨ 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 ⟩ だからである。二つの圧縮された命題を、基礎の型がやはり積である ⊓ で組み合わせれば、同値は eP と eQ に Σ-cong-equiv を適用して得られる。証明の対を、圧縮された証明の対へ写すだけである。各因子が圧縮できること以外に、命題についての情報は要らない。

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

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

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

  (P' ⊔ Q') , propTrunc≃ (⊎-equiv eP eQ)

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

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

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

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

small⊤ : hasSize ℓ (⊤ {ℓ = ℓ-suc ℓ})

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

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

small⊥ : hasSize ℓ (⊥ {ℓ = ℓ-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 → hasSize ℓ (B x))
         → hasSize ℓ (∀[ x ∶ S ] (x ∈ˢ a) ⇒ B x)
small-∀∈ a {B} sm = Qsm , propBiimpl→Equiv (big .snd) (Qsm .snd) 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 → hasSize ℓ (B x))
         → hasSize ℓ (∃[ x ∶ S ] (x ∈ˢ a) ⊓ B x)
small-∃∈ a {B} sm = Qsm , propBiimpl→Equiv (big .snd) (Qsm .snd) fwd bwd
  where

順方向では、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 = map₁ λ where
    (x , x∈a , bx) →

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

module SemanticsV = FOL.Semantics 𝒮ᵥ

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

open SemanticsV.At K ι

Δ₀-small : ∀ {n} {φ : Formula K n} → Δ₀ φ → (γ : Vec S n) → hasSize ℓ (γ ⊨ φ)

原子の場合は、環境 γ で二つの項を評価したうえで、備えられた最初の二つの補題を直接呼ぶ。所属は 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 → hasSize ℓ (B a))
        → hasSize ℓ (∀[ 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 へ変え、各ファイバーを逆向きの各点の同値に沿って変え、propTrunc≃ がさらにその対の同値を切り詰めへ引き上げる。ここでも invEquiv が必要な向きを与える。二つの補題を合わせると、本質的に小さな型の上での量化は小ささを保存する、ということになる。そして次のコード塊で、本質的に小さいとはレベル ℓ の型と同値であることを意味する。

small-∃ : {A : Type (ℓ-suc ℓ)} {X : Type ℓ} (e : X ≃ A) {B : A → hProp (ℓ-suc ℓ)}
        → (∀ a → hasSize ℓ (B a))
        → hasSize ℓ (∃[ a ∶ A ] B a)
small-∃ {X = X} e sm = (∃[ m ∶ X ] sm (equivFun e m) .fst)
  , invEquiv (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 の論理式 φ と、制限された要素の任意の環境 δ : Vec SM n に対して、真理値 δ ⊨ᵐ φ は小さい。ここに帰納的な証人は姿を見せない。必要ないからである。ここの帰納法は論理式そのものに対して行われ、台の本質的な小ささが Δ₀ の制限の代わりをする。原子の二つの場合は、世界の中で項を評価して制限された要素を得て、その第一射影に原子的な小ささの補題を適用する。世界の中の所属 (xm .fst) ∈ˢ (ym .fst) は、周囲の構造の命題そのものであり、その小ささはすでに知られている。

⊨ᵐ-small : ∀ {n} (φ : Formula K n) (δ : Vec SM n) → hasSize ℓ (δ ⊨ᵐ φ)
⊨ᵐ-small (t ∈̇ u)  δ = small-∈ ((⟦ t ⟧ᵐ δ) .fst) ((⟦ u ⟧ᵐ δ) .fst)
⊨ᵐ-small (t ≐ u)  δ = small-≡ ((⟦ t ⟧ᵐ δ) .fst) ((⟦ u ⟧ᵐ δ) .fst)
⊨ᵐ-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 ] (xm .fst ∈ˢ ⟦ t ⟧ᵐ δ) ⇒ ((xm ∷ δ) ⊨ᵐ φ) である。前件の小ささは原子的な補題から、後件の小ささは帰納法の仮定から得られ、small⇒ が含意を組み立てる。主張全体は、さらに e に沿う small-∀ によって小さくなる。興味深い細部は第一射影 xm .fst である。有界性は、制限された要素の基礎となる集合についての主張である。世界の所属関係は V のそれの引き戻しだからである。

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

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

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

まとめ

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