Bedrock推移的な整礎関係の崩壊
この章を読むか、読書案内と依存マップで別のルートを選べます。
読書案内 · 依存マップ関係だけでどれほどの集合論的構造が得られるのか。Type ℓ 値の推移的な整礎関係 _≺_ を持つ小さな型 A を固定します。Mostowski の答えは、関係だけから再帰によって関数 col : A → SV.S が定まり、
col p = { col r | r ≺ p }
つまり各点がその前者の崩壊値からなる集合へ写される、というものです。計算法則が各値への所属を特徴付け、関係の推移性によって各崩壊値はここでいう順序数、すなわち自身が推移的で各要素も推移的な集合になります。
有限の例で仕組みを見ます。三点 s、r、p が s ≺ r、r ≺ p、および推移性から従う s ≺ p だけを関係として持つとすると、再帰は col s の要素を何も強制せず、col r = { col s }、col p = { col s, col r } となります。これはまさに von Neumann の 0、1、2 の図です。再帰は点そのものを見ず、前者の錐だけを見ます。
設定の三つの特徴がその後のすべてを形作ります。第一に、A と各繊維 x ≺ y は Type ℓ にあるので、各 p の前者の錐は小さな型 Σ[ r ∈ A ] (r ≺ p) です。階層 V の sett 構成子はまさにこのような小さな族を SV.S の集合に変えます。第二に、sett 集合への所属は構成上命題的切り詰めです。⟨ b ∈ˢ a ⟩ はあるインデックスで族の値が b に等しいことが単に存在すると述べるのであって、選ばれたインデックスが得られるとは言いません。したがって本章では、一方向には与えられたデータから所属を証明し (r ≺ p が col r ∈ˢ col p を与える)、他方向には崩壊値の等式を伴う、単に存在する前者しか得られません。第三に、後の消去の目標は集合の等式や isTransV x といった命題なので、そこへの切り詰めの消去は正当です。_≺_ に対する外延性の仮定は現れず、同じ前者の錐を持つ二点は区別されません。崩壊は正準ですが、単射であるとは主張しません。構成は整礎再帰と輸送だけを用い、ここでは古典的な原理を何も仮定しません。
崩壊は累積階層の集合レベルの台に着地します。したがって出力は A の点ではなく集合です。この台を以下では SV.S と書きます。これは h-集合、すなわち任意の二要素の間の等式型が命題となる型です。所属関係 _∈ˢ_ は各所属の主張を hProp、つまり根底の型 ⟨ b ∈ˢ a ⟩ とその型が命題である証明の対として与えます。したがって所属と推移性は階層本来の関係で直接述べられます。
{-# OPTIONS --cubical --safe --guardedness #-} open import Base.Prelude module L.Mostowski {ℓ : Level} where open import FOL.ZFStructure using ( module hPropStructure )
構成を駆動する要素は二つです。第一は階層の像演算 sett で、小さなインデックス型 X と族 X → V ℓ からその族の値の集合を形作り、所属はあるインデックスが目標に命中するときに単に成り立ちます。第二は整礎性の証明 WellFounded _≺_、すなわち A のすべての要素が ≺ に沿って到達可能であるという主張で、その帰納原理が再帰的に定義された関数を構成し、付随する計算法則が各点での振る舞いを記録します。命題的切り詰めは ∥ _ ∥₁ とその導入 ∣ _ ∣₁ を通して現れます。像への所属は設計上切り詰められているからです。順序数の目標 IsOrd、推移性 isTransV、そしてその命題性の証明 isPropIsTransV は L の構成から来ており、最後の定理がそれらを必要とするときにだけ現れます。
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ ) open import L.Constructible {ℓ} using ( IsOrd; isTransV; isPropIsTransV ) open import Cubical.HITs.CumulativeHierarchy.Base using ( sett ) open import Cubical.Induction.WellFounded using ( WellFounded; module WFI ) import Cubical.HITs.PropositionalTruncation as PT
階層構造は等号と所属がレベル ℓ-suc ℓ の hProp に値を取ります。一方、A と各繊維 x ≺ y は Type ℓ にあるので、各前者の錐は sett を適用できる小さな添字型です。構成に必要な大きさの事実はこれだけで、排中律は仮定しません。
open PT using ( ∣_∣₁; ∥_∥₁ ) module SV = hPropStructure 𝒮ᵥ open SV using ( _∈ˢ_ )
以下では二つの課題を果たします。まず崩壊の二つの所属法則を示します。与えられた前者から要素を構成できる一方、要素から逆に得られるのは、崩壊値の等式を伴って単に存在する前者だけです。次にこの二法則を整礎帰納法で用い、各 p について IsOrd (col p) を証明します。明示的な入力と切り詰められた出力の非対称性は両方の課題で本質的です。
再帰を可能にするのは整礎性です。wf から得られる帰納原理によれば、A 上の族 P を定義するには、各 p で全ての前者 r ≺ p における P の値から P p を構成すれば十分です。推移性の証拠 ≺-trans は col の定義には使われず、得られた集合の推移性を後で証明するときに使われます。
module Mostowski (A : Type ℓ) (_≺_ : A → A → Type ℓ) (wf : WellFounded _≺_) (≺-trans : {x y z : A} → x ≺ y → y ≺ z → x ≺ z) where module W = WFI wf using ( induction; induction-compute ) colStep : (p : A) → (∀ r → r ≺ p → SV.S) → SV.S
再帰の一段は前者の錐の像です。p と、各 r ≺ p に対してすでに col r を知る再帰呼び出し rec が与えられれば、この段は sett (Σ[ r ∈ A ] (r ≺ p)) (λ z → rec (fst z) (snd z)) を形作ります。インデックス型は対 (r , r ≺ p) の全空間であり、族はその対を rec r へ送ります。抽象的には、これがまさに章の冒頭で宣言した崩壊方程式 { col r | r ≺ p } です。段の型が任意の段関数 rec を量化している点に注目してください。おかげで同じデータが定義と、後述の計算法則を通した推論の両方に使えます。
colStep p rec = sett (Σ[ r ∈ A ] (r ≺ p)) (λ z → rec (fst z) (snd z)) opaque col : A → SV.S col = W.induction {P = λ _ → SV.S} colStep col-eq : (p : A) → col p ≡ sett (Σ[ r ∈ A ] (r ≺ p)) (λ z → col (fst z))
関数 col は整礎帰納法で定義されます。その計算規則 col-eq は col p を前者の錐の col による像と同一視します。後の所属証明ではこの等式を使い、再帰的に定義された値と明示的な像の間を移ります。明示的な像への所属には sett が与える切り詰められた逆像の分類があります。
col-eq = W.induction-compute colStep col-in : (p r : A) → r ≺ p → ⟨ col r ∈ˢ col p ⟩ col-in p r rp = subst (λ v → ⟨ col r ∈ˢ v ⟩) (sym (col-eq p)) ∣ (r , rp) , refl ∣₁ col-out : (p : A) (b : SV.S) → ⟨ b ∈ˢ col p ⟩
所属には両方向の計算法則があり、両者は有益な非対称を示します。順方向：r ≺ p が与えられれば col r は col p の要素です。証拠は対 (r , rp) と、col r がインデックス r で命中することを記録するパス refl であり、col-eq p に沿って (等式は逆向きに証明されているので sym の形で) 輸送することで、この明示的な像の要素が型 ⟨ col r ∈ˢ col p ⟩ へ移ります。逆方向：任意の所属 ⟨ b ∈ˢ col p ⟩ から得られるのは、切り詰められた主張、すなわち col r ≡ b となる r ≺ p が単に存在することだけです。証明は所属を col-eq p に沿って明示的な像への所属へ輸送し、それは構成により切り詰められた原像なので、インデックスのデータを等式を伴う前者として読み替えます。ここで特定の r を選ぶことは一切ありません。切り詰め ∥ _ ∥₁ が、所属から分かることの正直な記録です。
→ ∥ Σ[ r ∈ A ] ((r ≺ p) × (col r ≡ b)) ∥₁ col-out p b b∈ = PT.map (λ z → fst (fst z) , snd (fst z) , snd z) (subst (λ v → ⟨ b ∈ˢ v ⟩) (col-eq p) b∈) col-ord : (p : A) → IsOrd (col p)
最後の定理は、すべての崩壊値が順序数であると言います。IsOrd (col p) は対に展開され、col p が推移的であることと、その各要素が推移的であることからなります。証明は p 上の整礎帰納で進み、帰納の仮定 rec が各前者 r ≺ p に対して IsOrd (col r) を供給し、目標はその二つの成分から組み上がります。仮定 ≺-trans が力を発揮するのはまさにここです。二つの節を読む前に、三点の列 s ≺ r ≺ p を思い浮かべてください。関係の推移性こそが、col r についての所属の事実を col p の中で再演することを可能にします。
col-ord = W.induction {P = λ p → IsOrd (col p)} ih where ih : (p : A) → (∀ r → r ≺ p → IsOrd (col r)) → IsOrd (col p) ih p rec = tr , mem where
最初の節は、col p のすべての要素が推移的であるというものです。証明は col-out p x x∈ から始まります。要素 x は、単に存在する前者 r ≺ p に対する col r であり、等式 e : col r ≡ x を伴います。帰納の仮定が isTransV (col r) を供給し、subst isTransV e がその証明を等式に沿って型 isTransV x へ輸送します。切り詰めの消去が正当なのは、目標の isTransV x が命題であり isPropIsTransV x がそれを証明するからです。証拠を取り出すのではなく、単に存在する場合分けから命題を確立しているだけです。
mem : (x : SV.S) → ⟨ x ∈ˢ col p ⟩ → isTransV x mem x x∈ = PT.rec (isPropIsTransV x) (λ z → subst isTransV (snd (snd z)) (rec (fst z) (fst (snd z)) .fst)) (col-out p x x∈) tr : isTransV (col p)
第二の節は col p 自身の推移性を示します。y ∈ x と x ∈ col p が与えられたとき y ∈ col p を示します。まず x ∈ col p を col-out で剥がし、col r ≡ x となる r ≺ p が単に得られます。この等式が与えられた y ∈ x を ⟨ y ∈ˢ col r ⟩ へ輸送し、実行例の中間の環 r がまさにここで列の両端をつなぎます。
tr {x} {y} y∈x x∈col = PT.rec (snd (y ∈ˢ col p)) outer (col-out p x x∈col) where outer : Σ[ r ∈ A ] ((r ≺ p) × (col r ≡ x)) → ⟨ y ∈ˢ col p ⟩ outer (r , rp , e) = PT.rec (snd (y ∈ˢ col p)) inner
これで列が閉じます。y ∈ col r から、r で col-out を適用すると、col s ≡ y となる s ≺ r が単に得られ、その等式を e2 とします。関係の推移性が s ≺ r と r ≺ p を合成して s ≺ p を与え、col-in p s が col s を col p の要素へ引き上げます。最後に e2 に沿った subst が所属の目標の中で col s を y に置き換え、⟨ y ∈ˢ col p ⟩ が得られます。切り詰めの消去はどちらも命題 ⟨ y ∈ˢ col p ⟩ の中に着地し、議論全体が使うのは整礎再帰、輸送、そして推移性の仮定だけです。古典的な原理は本章のどこにも入りません。
(col-out r y (subst (λ v → ⟨ y ∈ˢ v ⟩) (sym e) y∈x)) where inner : Σ[ s ∈ A ] ((s ≺ r) × (col s ≡ y)) → ⟨ y ∈ˢ col p ⟩ inner (s , sr , e2) = subst (λ v → ⟨ v ∈ˢ col p ⟩) e2 (col-in p s (≺-trans sr rp))