Bedrockこの章を読むか、読書案内と依存マップで別のルートを選べます。
読書案内 · 依存マップこの章の課題は、構成可能な台の要素をパラメータとして許した一階定義可能部分集合の集まりを、有界論理式で認識することです。この集まりは定義可能冪集合 𝒟ₒ であり、完全な内部冪集合ではありません。内部の記述が正しくなるには、数項のタグ、符号領域、充足関係表がそれぞれ意図した意味をもつ必要があります。
{-# OPTIONS --cubical --safe --guardedness #-}
この構成では、排中律を本書で唯一の明示的な古典的仮定として用います。それでも命題的切り詰めは全体に残ります。存在証明は、ある論理式や表の値が存在することを示しても、それを大域的に選び出しません。
open import Base.Prelude open import Base.Classical using ( LEM )
宇宙レベル ℓ と実例 lem : LEM (ℓ-suc ℓ) を固定します。このモジュールのすべての結果は、最後の健全性と完全性を含め、ちょうどこの仮定のもとで成り立ちます。
module L.GCH.DefinablePowerSetDescription {ℓ : Level} (lem : LEM (ℓ-suc ℓ)) where
対象言語での記述は、意図的に有界に保ちます。所属原子式、連言、含意、有界存在量化子、有界全称量化子だけから組み立て、後で checkΔ₀ がこの構文上の形を検査します。外から与えた論理式を、符号化された充足構成での解釈と比較する際には、定数の写像も用います。
open import FOL.ZFStructure using ( module hPropStructure ) open import FOL.Syntax using ( Formula; var; _∈̇_; _∧̇_; _⇒̇_; ∃̇∈; ∀̇∈ ) open import FOL.LevyHierarchy using ( Δ₀; checkΔ₀ ) open import FOL.Manipulation.ConstantMapping using ( mapFo ) import FOL.Absoluteness
意図する出力は 𝒟ₒ W、すなわち W 上の制限構造で W の要素をパラメータとして定義できる部分集合の集まりです。二つの所属方向を証明すれば、外延性によって候補の出力をこの集合と同一視できます。順序対の符号は、環境、論理式の鍵、表の項目を表します。
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ; extensionalV ) open import V.Coding {ℓ} using ( pr ) open import L.Constructible {ℓ} using ( 𝒮ʟ; isL; isL-trans; 𝒟ₒ; 𝒟ₒ-intro; 𝒟ₒ-inv ) open import L.Definability {ℓ} using ( module DefOf ) open import L.Coding.Model {ℓ} using ( prAtL; container )
論理式 ψ に対し、充足構成はどの一項環境が ψ を満たすかを記録します。橋渡し定理は、そこから W の中で切り出される部分を、ψ が定義する部分集合と同一視します。実際の符号集合は ψ から作られる鍵を含み、実際の充足関係表の関数性がその鍵での値を定めます。これらを使えるのは、候補の符号集合と表を satAt が保証した後だけです。復号が一意になるわけでも、部分集合の定義論理式が選ばれるわけでもありません。
open import L.Coding.SatisfactionBridge {ℓ} lem using ( asConst; defSet-Sat ) open import L.Coding.DefinablePowerSet {ℓ} lem using ( envOne ) open import L.Coding.CodeSet {ℓ} lem using ( keyS; key∈AllCodes ) open import L.Coding.UniformSatisfaction {ℓ} lem using ( module Table; val-at ) open import L.Coding.Satisfaction {ℓ} lem using ( Sat )
記述に現れる量化子はすべて、環境にすでにある集合によって有界でなければなりません。以下の補助量化子は、その範囲内で順序対の符号の二成分を表します。二方向の補題によって、対象言語での充足と対応する意味論的な証人との間を行き来できます。
open import L.Coding.Quantification {ℓ} using ( sh; i0; i1; i3; i6; f0; f1; down ; sndEx; sndAll; sndEx-out; sndAll-in; fillSnd; useSnd ; pr-out; pr-in; sndS ) open import L.Coding.CodeDomain {ℓ} using ( Tags )
Tags は、指定された十個の枠を数項 0 から 9 と解釈します。特に以下の節では、タグ 0 で一項環境を、タグ 1 でアリティ 1 の鍵を認識します。別の述語 satAt はさらに強く、候補のコード領域と表が、その台上のアルファベットと再帰的な充足構成を実現していることを保証します。
open import L.Coding.CodeAlphabet {ℓ} using ( module Alphabet ) open import L.GCH.SatisfactionDescription {ℓ} lem using ( satAt; module SatRead; module Match )
環境は構成可能集合からなる有限ベクトルで表します。積は切り出し関係を定める二つの所属条件を組み合わせます。それらが命題であるため、選択を導入することなく、切り詰められた証人をその条件へ消去できます。
open import Cubical.Data.Nat using ( _+_ ) open import Cubical.Data.Unit using ( tt ) open import Cubical.Data.Vec using ( _∷_; lookup ) open import Cubical.Data.Sigma using ( _×_ ) open import Cubical.Foundations.HLevels using ( isProp× )
証明では、点ごとの所属の同値を集合の等しさへ繰り返し変換します。所属は命題値なので、どちらの所属方向を示すときにも、単に存在する符号・論理式・表示を消去できます。周囲の集合の要素を台の要素として読む必要があるときは、∈-asFiber が表示の添字を復元します。
open import Cubical.Functions.Logic using ( ⇔toPath ) import Cubical.HITs.PropositionalTruncation as PT open PT using ( ∥_∥₁; ∣_∣₁; squash₁ ) open import Cubical.HITs.CumulativeHierarchy.Base using ( V; _∈_; setIsSet ) open import Cubical.HITs.CumulativeHierarchy.Properties using ( ∈-asFiber )
タグとして使うフォン・ノイマン数項は累積階層の中にあります。特に 0 は一変数環境の唯一の項目を示し、1 はここで扱う論理式のアリティを示します。
open import Cubical.HITs.CumulativeHierarchy.Constructions using ( module InfinitySet ) open InfinitySet {ℓ} using ( #_ )
構成可能集合の台を S と書きます。S の要素は基礎の集合とその構成可能性の証明書からなるので、論理式の有界な証人は意図したモデルの内部にとどまります。
open hPropStructure 𝒮ʟ using ( S )
構成可能集合の有限環境で対象言語の論理式が充足されることを γ ⊨ φ と書きます。この記法の背後にある絶対性によって、後の意味論的な議論では、この内部の読みを周囲の累積階層における通常の所属と比較できます。
module AbsL = FOL.Absoluteness.Single 𝒮ᵥ isL isL-trans using ( _^_; _⊨ᵐ_ ) open AbsL using ( _^_ ) renaming ( _⊨ᵐ_ to _⊨_ )
単項環境は、一つの枠の上の二つの有界の節で記述されます。符号化された集合 e のすべての要素が、タグ 0 と値 z の順序対であり、e の中にその対に等しい要素が存在する、というものです。全称の節がほかのすべての要素を排除し、存在の節が空集合を排除します。
singleOf : ∀ {j} → Fin j → Fin j → Fin j → Formula S j singleOf e N0 z = ∀̇∈ (var e) (prAtL i0 (sh 1 N0) (sh 1 z)) ∧̇ ∃̇∈ (var e) (prAtL i0 (sh 1 N0) (sh 1 z))
定義可能部分集合の節には二つの連言肢があります。第一は、符号化された集合 x のすべての要素が w に属し、その一項環境が値 y に属することを述べます。第二は、w の要素 z のうち、その一項環境が y に属するものはすべて x に属することを述べます。合わせると、x が値 y によって w から切り出されることが分かります。
definesB : ∀ {j} → Fin j → Fin j → Fin j → Fin j → Formula S j definesB x w y N0 = ∀̇∈ (var x) ((var i0 ∈̇ var (sh 1 w)) ∧̇ ∃̇∈ (var (sh 1 y)) (singleOf i0 (sh 2 N0) i1)) ∧̇ ∀̇∈ (var w) (∃̇∈ (var (sh 1 y)) (singleOf i0 (sh 2 N0) i1) ⇒̇ (var i0 ∈̇ var (sh 1 x)))
所属の節は候補の値の要素を走ります。各要素について要求するのは、候補領域 C にタグ 1 との対の形をした要素 c があり、表の項目が c と値 y を対にし、その y が当の要素を w から切り出すことだけです。この段階の c は鍵の形をしているにすぎません。後で satAt を仮定して初めて、実際の論理式の鍵として復号できます。
memAt : ∀ {m} → Fin m → Fin m → Fin m → Fin m → (Fin 10 → Fin m) → Formula S m memAt v w T C N = ∀̇∈ (var v) (∃̇∈ (var (sh 1 C)) (sndEx i0 (sh 2 (N f1)) (∃̇∈ (var (sh 4 T)) (sndEx i0 i3 (definesB i6 (sh 7 w) i0 (sh 7 (N f0)))))))
被覆の節は逆向きの条件を与えます。C の要素 c がタグ 1 の鍵の形をもつなら、c での表の値 y と、y によって切り出される候補出力の要素 x が単に存在することを要求します。したがって候補領域の鍵形の要素をすべて覆いますが、それらを実際のアリティ 1 の論理式の鍵すべてと同一視するには、やはり satAt が必要です。
allAt : ∀ {m} → Fin m → Fin m → Fin m → Fin m → (Fin 10 → Fin m) → Formula S m allAt v w T C N = ∀̇∈ (var C) (sndAll i0 (sh 1 (N f1)) (∃̇∈ (var (sh 3 T)) (sndEx i0 i3 (∃̇∈ (var (sh 6 v)) (definesB i0 (sh 7 w) i1 (sh 7 (N f0)))))))
論理式 defAt は、所属の節と被覆の節を連言で結びます。それだけでは候補出力を候補のコード領域と表に関係づけるにすぎません。正しい Tags と satAt のデータを合わせると、二つの節が、出力は 𝒟ₒ W であることを示す二つの包含になります。
opaque defAt : ∀ {m} → Fin m → Fin m → Fin m → Fin m → (Fin 10 → Fin m) → Formula S m defAt v w T C N = memAt v w T C N ∧̇ allAt v w T C N
通常の議論ではこの定義を不透明に保ち、後の証明が長い構文展開ではなく、二つの包含という数学的なインターフェースを使うようにします。展開するのは、有界性の確認と二方向の読みの証明に必要な局所的な範囲だけです。
opaque unfolding defAt
Δ₀ の証拠は、構造的な検査によって産み出されます。論理式が使うのは、変数・所属・連言・含意・有界の量化子だけです。証明されるのは論理式の形であって、記述の正しさではありません。
Δ₀-defAt : ∀ {m} (v w T C : Fin m) (N : Fin 10 → Fin m) → Δ₀ (defAt v w T C N) Δ₀-defAt v w T C N = checkΔ₀ (defAt v w T C N) tt
記述の読みは、それを二つの連言支に分解します。
defAt-out : ∀ {m} (v w T C : Fin m) (N : Fin 10 → Fin m) (γ : S ^ m) → ⟨ γ ⊨ defAt v w T C N ⟩ → ⟨ γ ⊨ memAt v w T C N ⟩ × ⟨ γ ⊨ allAt v w T C N ⟩ defAt-out v w T C N γ h = h
記述の埋めは、二つの連言支を再び対にします。
defAt-in : ∀ {m} (v w T C : Fin m) (N : Fin 10 → Fin m) (γ : S ^ m) → ⟨ γ ⊨ memAt v w T C N ⟩ → ⟨ γ ⊨ allAt v w T C N ⟩ → ⟨ γ ⊨ defAt v w T C N ⟩ defAt-in v w T C N γ h1 h2 = h1 , h2
最初の意味論的な計算では singleOf を扱います。符号化された集合 E と値 Z を固定し、指定されたタグが実際に 0 を表すと仮定します。この仮定の下で、二つの有界な節が集合の等式 E = envOne Z と同値であることを示します。
module _ {j : ℕ} (e N0 z : Fin j) (δ : S ^ j) (q0 : fst (lookup N0 δ) ≡ # 0) where private E = fst (lookup e δ) Z = fst (lookup z δ)
単項の節の読みから、符号化された集合が値の正準な単項環境と等しいことが得られます。順方向では、符号化された集合のすべての要素が、数項ゼロと値の順序対であり、対のアトムの妥当性に沿って運ばれます。
singleOf-out : ⟨ δ ⊨ singleOf e N0 z ⟩ → E ≡ envOne Z singleOf-out (hall , hex) = extensionalV (λ y → ⇔toPath (fwd y) (bwd y)) where fwd : (y : V ℓ) → ⟨ y ∈ E ⟩ → ⟨ y ∈ envOne Z ⟩ fwd y hy = ∣ lift zero , sym (pr-out i0 (sh 1 N0) (sh 1 z) (down (lookup e δ) y hy ∷ δ) (hall (down (lookup e δ) y hy) hy)
逆向きの包含では、正準な一項環境の要素から始めます。存在側の連言肢が符号化された集合のある要素を与え、その対の等式と既知のタグ 0 によって、その要素を最初に与えた要素と同一視できます。この等式に沿って所属を移送すれば、元の要素が符号化された集合に属することが得られます。
∙ cong (λ a → pr a Z) q0) ∣₁ bwd : (y : V ℓ) → ⟨ y ∈ envOne Z ⟩ → ⟨ y ∈ E ⟩ bwd y = PT.rec (snd (y ∈ E)) (λ { (lift zero , qy) → PT.rec (snd (y ∈ E)) (λ { (y' , (y'∈ , hy')) →
envOne Z の要素は順序対 pr (# 0) Z です。したがってタグの枠を数項 0 に書き換えると、この要素は singleOf が要求する順序対と同一視されます。要素そのものが Z と同一視されるわけではありません。
subst (λ u → ⟨ u ∈ E ⟩) (pr-out i0 (sh 1 N0) (sh 1 z) (y' ∷ δ) hy' ∙ cong (λ a → pr a Z) q0 ∙ qy) y'∈ }) hex ; (lift (suc ()) , _) })
逆に、符号化された集合が正準な一項環境に等しいと仮定します。その環境の唯一の添字は 0 なので、各要素は必要な順序対の形をもち、残る後者添字の場合は不可能性で閉じます。正準な 0 番の項目が有界存在の証人を与え、仮定した等式に沿う移送がその所属を与えます。
singleOf-in : E ≡ envOne Z → ⟨ δ ⊨ singleOf e N0 z ⟩ singleOf-in q = (λ y hy → pr-in i0 (sh 1 N0) (sh 1 z) (y ∷ δ) (PT.rec (setIsSet (fst y) (pr (fst (lookup N0 δ)) Z)) (λ { (lift zero , qy) → sym qy ∙ cong (λ a → pr a Z) (sym q0) ; (lift (suc ()) , _) })
要素に名前が与えられ、その所属が運ばれます。そして存在の証人は、ゼロの数項と値の対を、タグの等式に逆らってまとめます。
(subst (λ u → ⟨ fst y ∈ u ⟩) q hy))) , ∣ yS , ( subst (λ u → ⟨ pr (# 0) Z ∈ u ⟩) (sym q) ∣ lift zero , refl ∣₁ , pr-in i0 (sh 1 N0) (sh 1 z) (yS ∷ δ) (cong (λ a → pr a Z) (sym q0)) ) ∣₁ where yS : S
名前のついた要素は、数項ゼロと値の対の、符号化された集合の中での提示です。
yS = down (lookup e δ) (pr (# 0) Z) (subst (λ u → ⟨ pr (# 0) Z ∈ u ⟩) (sym q) ∣ lift zero , refl ∣₁)
集合 X・台 Wv・値 Y の間の切り出しの関係は、各点での双方向です。X のすべての要素は Wv に属しその単項環境が Y の中にあり、Wv の要素のうちその単項環境が Y の中にあるものはすべて X に属します。量化は構成可能な集合の上を行われるので、この関係は構成可能な台の上で述べられます。
Cuts : (X Wv Y : V ℓ) → Type (ℓ-suc ℓ) Cuts X Wv Y = ((z : S) → ⟨ fst z ∈ X ⟩ → ⟨ fst z ∈ Wv ⟩ × ⟨ envOne (fst z) ∈ Y ⟩) × ((z : S) → ⟨ fst z ∈ Wv ⟩ → ⟨ envOne (fst z) ∈ Y ⟩ → ⟨ fst z ∈ X ⟩)
対象言語の節を数学的な切り出し関係と比較するため、x、w、y、タグ 0 の枠を固定します。それぞれの解釈を X、Wv、Y と名付けます。タグの等式があるからこそ、singleOf は正準な一項環境を表せます。
module _ {j : ℕ} (x w y N0 : Fin j) (δ : S ^ j) (q0 : fst (lookup N0 δ) ≡ # 0) where private X = fst (lookup x δ) Wv = fst (lookup w δ) Y = fst (lookup y δ)
Y は構成可能集合なので、一項環境が Y に属するという証明から、その環境を表す台の要素を得られます。この表示があるため、definesB の有界存在量化子は Y の実際の要素を証人にできます。
YS = lookup y δ
単項の節の存在量化を読むと、それが、正準な単項環境の値の中での所属に変換されます。証人は値の要素であり、単項の節が、符号化された項目をその索引の正準な環境と同一視します。
one-out : (z : S) → ⟨ (z ∷ δ) ⊨ ∃̇∈ (var (sh 1 y)) (singleOf i0 (sh 2 N0) i1) ⟩ → ⟨ envOne (fst z) ∈ Y ⟩ one-out z = PT.rec (snd (envOne (fst z) ∈ Y)) (λ { (e , (e∈ , he)) → subst (λ u → ⟨ u ∈ Y ⟩) (singleOf-out i0 (sh 2 N0) i1 (e ∷ z ∷ δ) q0 he) e∈ })
存在量化の埋めは逆です。正準な単項環境は値の中で提示され、単項の節は延長された環境のもとで埋められます。
one-in : (z : S) → ⟨ envOne (fst z) ∈ Y ⟩ → ⟨ (z ∷ δ) ⊨ ∃̇∈ (var (sh 1 y)) (singleOf i0 (sh 2 N0) i1) ⟩ one-in z h = ∣ down YS (envOne (fst z)) h , (h , singleOf-in i0 (sh 2 N0) i1 (down YS (envOne (fst z)) h ∷ z ∷ δ) q0 refl) ∣₁
定義可能部分集合の節を読むと、切り出し関係の二つの方向が得られます。第一の連言肢は、X の各要素が Wv に属し、その一項環境が Y に属することを与えます。第二の連言肢は、この二つの事実から X への所属を戻します。
definesB-out : ⟨ δ ⊨ definesB x w y N0 ⟩ → Cuts X Wv Y definesB-out (h1 , h2) = (λ z hz → h1 z hz .fst , one-out z (h1 z hz .snd)) , (λ z hw he → h2 z hw (one-in z he))
逆に、Cuts X Wv Y の二つの各点的な方向から、対象言語における定義可能部分集合の節の二つの連言肢を満たせます。上の内部変換は、有界な一項環境の証人と、正準な一項環境が Y に属することとの間を正確に行き来します。
definesB-in : Cuts X Wv Y → ⟨ δ ⊨ definesB x w y N0 ⟩ definesB-in (o , i) = (λ z hz → o z hz .fst , one-in z (o z hz .snd)) , (λ z hw he → i z hw (one-out z he))
有界部分集合の各節を読む
完全な読みのモジュールは、四つの集合、すなわち提案された値・台・表・コードの定義域に名前を与えます。
module Read {m : ℕ} (v w T C : Fin m) (N : Fin 10 → Fin m) (γ : S ^ m) (tg : Tags γ N) where private Vv = fst (lookup v γ) Wv = fst (lookup w γ) Tv = fst (lookup T γ)
コードの定義域の底の集合と、タグ一の背後にある数項が名付けられます。所属の節が選ぶのは、タグ一と第二成分の対の形のコードだからです。
Cv = fst (lookup C γ) N1v = fst (lookup (N f1) γ)
所属の節の読みは、提案された値の各要素に対して、切り詰められた記録を与えます。定義域の中の、タグ一とある成分の対として分解される符号、その符号をある値と対にする表の項目、そしてその要素と値の間の切り出しの関係です。記録は切り詰めのもとで存在し、符号や値は選ばれません。
mem-out : ⟨ γ ⊨ memAt v w T C N ⟩ → (x : S) → ⟨ fst x ∈ Vv ⟩ → ∥ Σ[ c ∈ S ] Σ[ p ∈ S ] Σ[ y ∈ S ] (⟨ fst c ∈ Cv ⟩ × ((fst c ≡ pr (# 1) (fst p)) × (⟨ pr (fst c) (fst y) ∈ Tv ⟩ × Cuts (fst x) Wv (fst y)))) ∥₁ mem-out h x x∈ = PT.rec squash₁ (λ { (c , (c∈ , hc)) → PT.rec squash₁
所属の節を読むには、まず候補の符号領域から鍵の形をした要素 c を取り出し、次に c と値 y を対にする表の項目を取り出します。対の仕様が符号化された第二成分を結果に現れる意味論的な等式へ変え、タグの等式が形式的なタグを実際の数項 1 へ書き換えます。
(λ { (p , s , (ec , he)) → PT.rec squash₁ (λ { (e , (e∈ , hy)) → PT.map (λ { (y , s' , (ee , hd)) → c , p , y , ( c∈ , ( ec ∙ cong (λ a → pr a (fst p)) (tg f1) , ( subst (λ u → ⟨ u ∈ Tv ⟩) ee e∈
最も内側の存在は、definesB-out を通して読まれ、要素と表の項目の値 y の間の切り出しの関係を産み出します。
, definesB-out i6 (sh 7 w) i0 (sh 7 (N f0)) (y ∷ s' ∷ e ∷ p ∷ s ∷ c ∷ x ∷ γ) (tg f0) hd ) ) ) }) (sndEx-out i0 i3 (definesB i6 (sh 7 w) i0 (sh 7 (N f0))) (e ∷ p ∷ s ∷ c ∷ x ∷ γ) hy) }) he }) (sndEx-out i0 (sh 2 (N f1)) (∃̇∈ (var (sh 4 T)) (sndEx i0 i3 (definesB i6 (sh 7 w) i0 (sh 7 (N f0))))) (c ∷ x ∷ γ) hc) }) (h x x∈)
所属の節の埋めは逆の構成です。各要素に対して切り詰められた記録を産み出す関数を受け取り、節の充足を組み立てます。
mem-in : ((x : S) → ⟨ fst x ∈ Vv ⟩ → ∥ Σ[ c ∈ S ] Σ[ p ∈ S ] Σ[ y ∈ S ] (⟨ fst c ∈ Cv ⟩ × ((fst c ≡ pr (# 1) (fst p)) × (⟨ pr (fst c) (fst y) ∈ Tv ⟩ × Cuts (fst x) Wv (fst y)))) ∥₁) → ⟨ γ ⊨ memAt v w T C N ⟩ mem-in g x x∈ = PT.map
逆に、候補出力の各要素に対して、このような切り詰められた意味論的記録が与えられているとします。等式 c = pr (# 1) p は有界論理式が要求するアリティ一の形を与え、pr(c,y) の表への所属は表の項目の有界な表示を与えます。
(λ { (c , p , y , (c∈ , (ec , (e∈ , cuts)))) → let ec' : fst c ≡ pr N1v (fst p) ec' = ec ∙ cong (λ a → pr a (fst p)) (sym (tg f1)) δ4 = p ∷ container c (lookup (N f1) γ) p ec' .fst ∷ c ∷ x ∷ γ eS = down (lookup T γ) (pr (fst c) (fst y)) e∈
続いて七つの枠からなる環境を組み立て、definesB-in によって切り出し関係を定義可能部分集合の節へ戻します。
δ7 = y ∷ container eS c y refl .fst ∷ eS ∷ δ4 in c , ( c∈ , fillSnd i0 (c ∷ x ∷ γ) (lookup (N f1) γ) p ec' (∃̇∈ (var (sh 4 T)) (sndEx i0 i3 (definesB i6 (sh 7 w) i0 (sh 7 (N f0))))) ∣ eS , ( e∈ , fillSnd i0 (eS ∷ δ4) c y refl (definesB i6 (sh 7 w) i0 (sh 7 (N f0))) (definesB-in i6 (sh 7 w) i0 (sh 7 (N f0)) δ7 (tg f0) cuts) i3 refl ) ∣₁
鍵の形、表の項目、切り出し条件を符号化した後、外側の有界量化子が、この切り詰められたまとまりを候補出力の元の要素に適用します。したがって、この意味論的記録から所属の節全体の充足を再構成できます。
(sh 2 (N f1)) refl ) }) (g x x∈)
覆いの節の読みは、タグ一と p の対として分解される符号 c を取り、単に、c における表の値 y と、y によって切り出される集合 x を与えます。
all-out : ⟨ γ ⊨ allAt v w T C N ⟩ → (c p : S) → ⟨ fst c ∈ Cv ⟩ → fst c ≡ pr (# 1) (fst p) → ∥ Σ[ y ∈ S ] Σ[ x ∈ S ] (⟨ pr (fst c) (fst y) ∈ Tv ⟩ × (⟨ fst x ∈ Vv ⟩ × Cuts (fst x) Wv (fst y))) ∥₁ all-out h c p c∈ ec = PT.rec squash₁ (λ { (e , (e∈ , hy)) → PT.rec squash₁ (λ { (y , s' , (ee , hx)) → PT.map
証明は、表の項目と三つの枠の存在量化を消去します。そして定義可能な部分集合の節の読みが、要素と表の値の間の切り出しの関係を産み出します。
(λ { (x , (x∈ , hd)) → y , x , ( subst (λ u → ⟨ u ∈ Tv ⟩) ee e∈ , ( x∈ , definesB-out i0 (sh 7 w) i1 (sh 7 (N f0)) (x ∷ y ∷ s' ∷ e ∷ δ3) (tg f0) hd ) ) }) hx }) (sndEx-out i0 i3 (∃̇∈ (var (sh 6 v)) (definesB i0 (sh 7 w) i1 (sh 7 (N f0)))) (e ∷ δ3) hy) })
逆向きの構成では、符号領域の要素 c を固定し、それが pr (# 1) p として表される場合を調べます。意味論的な覆いの仮定は、命題的切り詰めの下で表の値と、その値が切り出す部分集合を与えます。これらの証人が、その表示に対する有界な結論を満たします。
(useSnd i0 (c ∷ γ) (lookup (N f1) γ) p ec' (∃̇∈ (var (sh 3 T)) (sndEx i0 i3 (∃̇∈ (var (sh 6 v)) (definesB i0 (sh 7 w) i1 (sh 7 (N f0)))))) (sh 1 (N f1)) refl (h c c∈)) where ec' : fst c ≡ pr N1v (fst p)
形式的なタグを使う等式は、Tags によって必要なアリティ一の等式へ変換されます。補助的な容器は、成分と符号を有界量化子の範囲内に保つだけであり、意味論的な証人に選択や一意性を加えるものではありません。
ec' = ec ∙ cong (λ a → pr a (fst p)) (sym (tg f1)) δ3 : S ^ (3 + m) δ3 = p ∷ container c (lookup (N f1) γ) p ec' .fst ∷ c ∷ γ
したがって覆いの節を満たす際には、候補の符号領域の要素のうち、アリティ一の鍵の形で表示されたものをすべて扱います。その各表示に対し、意味論的な仮定が命題的切り詰めの下で、表の値、それが切り出す候補出力の要素、および両者の所属を与えます。後で satAt を加えるまでは、これらが実際の論理式の鍵であるとは主張しません。
all-in : ((c p : S) → ⟨ fst c ∈ Cv ⟩ → fst c ≡ pr (# 1) (fst p) → ∥ Σ[ y ∈ S ] Σ[ x ∈ S ] (⟨ pr (fst c) (fst y) ∈ Tv ⟩ × (⟨ fst x ∈ Vv ⟩ × Cuts (fst x) Wv (fst y))) ∥₁) → ⟨ γ ⊨ allAt v w T C N ⟩ all-in g c c∈ = sndAll-in' (λ p s s∈ p∈ ec → PT.map (λ { (y , x , (e∈ , (x∈ , cuts))) →
最も内側の有界存在量化子には、切り出された集合 x と、x が値の集合に属する証明、さらに definesB で符号化したばかりの Cuts の証拠が渡されます。これで逆向きの翻訳が完成します。表の項目とそれが切り出す部分集合についての意味論的な証人から所属の条項の充足が得られ、存在データはすべて命題的切り詰めの中に保たれます。
let eS = down (lookup T γ) (pr (fst c) (fst y)) e∈ δ6 = y ∷ container eS c y refl .fst ∷ eS ∷ p ∷ s ∷ c ∷ γ in eS , ( e∈ , fillSnd i0 (eS ∷ p ∷ s ∷ c ∷ γ) c y refl (∃̇∈ (var (sh 6 v)) (definesB i0 (sh 7 w) i1 (sh 7 (N f0)))) ∣ x , (x∈ , definesB-in i0 (sh 7 w) i1 (sh 7 (N f0)) (x ∷ δ6) (tg f0) cuts) ∣₁ i3 refl ) }) (g c p c∈ (ec ∙ cong (λ a → pr a (fst p)) (tg f1))))
覆いの条項にも同じ二段の存在選択があります。充足関係表の値と、その値が作業集合から切り出す部分集合です。両者を合わせた外向きの読み出しに名前を付けることで、次の議論では、この単に存在する一対の証人を一つの命題値のまとまりとして扱えます。
where sndAll-in' = sndAll-in i0 (sh 1 (N f1)) (∃̇∈ (var (sh 3 T)) (sndEx i0 i3 (∃̇∈ (var (sh 6 v)) (definesB i0 (sh 7 w) i1 (sh 7 (N f0)))))) (c ∷ γ)
有界な記述の正しさ
ここから、有界な記述を実際の定義可能性の演算と比較します。この比較には defAt の充足だけでは足りません。数を表すタグが意図した値をもち、作業集合の枠が W を表し、さらに satAt が符号集合と充足関係表に本来の充足意味論を保証していなければなりません。
module DefRead {m : ℕ} (v w T C E : Fin m) (N : Fin 10 → Fin m) (γ : S ^ m) (W : S) (qw : fst (lookup w γ) ≡ fst W) (tg : Tags γ N) (hs : ⟨ γ ⊨ satAt T w C E N ⟩) where open Alphabet W open Match W private
先に得た二つの読み出しが必要な橋を与えます。SatRead は、記述された符号領域と表を、W 上の実際の符号と充足値に対応させます。Read は defAt を二つの意味論的な切り出し条件として読みます。その上で DefOf (fst W) が、復号されたアリティ一の各論理式を W の一つの部分集合として解釈します。
module SR = SatRead T w C E N γ W qw tg hs module RD = Read v w T C N γ tg module DA = DefOf (fst W) Vv = fst (lookup v γ) Wv = fst (lookup w γ)
表の枠と符号の枠が表す基礎の集合を、それぞれ Tv と Cv と書きます。satAt の役割はまさに、これら記述された集合への所属と、実際の充足関係表および符号領域への所属とを相互に変換できるようにすることです。
Tv = fst (lookup T γ) Cv = fst (lookup C γ)
対応 toS は、アルファベットの上の論理式のすべての定数を、S の対応する定数へ付け替え、周囲の充足で判定できる論理式を作ります。
toS : Formula Ab 1 → Formula S 1 toS = mapFo (asConst W)
表の値の補題は、論理式のキーで記録された値が、付け替えられた論理式の明示的な充足集合に等しいと言います。証明は、表の外向きの射影と、一様な充足の値の同定とを合成します。
valOf : (ψ : Formula Ab 1) (c y : S) → fst c ≡ fst (keyS W ψ) → ⟨ pr (fst c) (fst y) ∈ Tv ⟩ → fst y ≡ fst (Sat W (toS ψ)) valOf ψ c y qc h = SR.T-out c y h .snd ∙ cong fst (val-at W W ψ c (SR.T-out c y h .fst) qc)
中心となる橋は論理式を一つずつ扱います。Cuts が、x は W の要素のうち、その一変数環境が ψ の充足集合に属するものからちょうど成ると述べるなら、x は特定の定義可能部分集合 DA.defSet ψ に等しくなります。この等式は、所属の両方向を示して外延性から得られます。
cut≡ : (ψ : Formula Ab 1) (x : S) → Cuts (fst x) Wv (fst (Sat W (toS ψ))) → DA.defSet ψ ≡ fst x cut≡ ψ x (o , i) = extensionalV (λ z → ⇔toPath (fwd z) (bwd z)) where fwd : (z : V ℓ) → ⟨ z ∈ DA.defSet ψ ⟩ → ⟨ z ∈ fst x ⟩ fwd z = PT.rec (snd (z ∈ fst x))
第一の方向では、DA.defSet ψ への所属から、命題的切り詰めの下で W の要素の表示が得られます。充足の橋によって、その表示の一変数環境は ψ の充足集合に入り、Cuts の内向きの半分が、表示された集合を x に入れます。
(λ { ((q , hq) , e) → i (down W z (subst (λ u → ⟨ u ∈ fst W ⟩) e (ι∈ q))) (subst (λ u → ⟨ z ∈ u ⟩) (sym qw) (subst (λ u → ⟨ u ∈ fst W ⟩) e (ι∈ q))) (subst (λ u → ⟨ envOne u ∈ fst (Sat W (toS ψ)) ⟩) e (subst ⟨_⟩ (defSet-Sat W ψ q) ∣ (q , hq) , refl ∣₁)) })
もう一方の方向では z ∈ x から始めます。Cuts の外向きの半分は、z ∈ W と、その一変数環境が充足集合に属することの両方を与えます。第一の事実は ∈-asFiber によって、W の表示の実際の添字と、そこから z へ戻るパスに変換されます。
bwd : (z : V ℓ) → ⟨ z ∈ fst x ⟩ → ⟨ z ∈ DA.defSet ψ ⟩ bwd z hz = let zS = down x z hz zW = subst (λ u → ⟨ z ∈ u ⟩) qw (o zS hz .fst) fib = ∈-asFiber {a = z} {b = fst W} zW
その表示のパスに沿って環境の所属を移し、defSet-Sat を逆向きに適用します。これにより表示が DA.defSet ψ に属することが分かり、同じパスに沿って戻せば z ∈ DA.defSet ψ が得られて、外延的な等式が完成します。
in subst (λ u → ⟨ u ∈ DA.defSet ψ ⟩) (fib .snd) (subst ⟨_⟩ (sym (defSet-Sat W ψ (fib .fst))) (subst (λ u → ⟨ envOne u ∈ fst (Sat W (toS ψ)) ⟩) (sym (fib .snd)) (o zS hz .snd)))
逆に、DA.defSet ψ がすでに x に等しいとします。Cuts を再構成するには、x の要素を DA.defSet ψ の要素へ書き換え、定義可能部分集合への所属を展開します。すると、その集合を W の要素として表すデータと、対応する一変数環境が充足集合に属する証明が同時に得られます。
cuts-of : (ψ : Formula Ab 1) (x : S) → DA.defSet ψ ≡ fst x → Cuts (fst x) Wv (fst (Sat W (toS ψ))) cuts-of ψ x e = o , i where o : (z : S) → ⟨ fst z ∈ fst x ⟩ → ⟨ fst z ∈ Wv ⟩ × ⟨ envOne (fst z) ∈ fst (Sat W (toS ψ)) ⟩ o z hz = PT.rec (isProp× (snd (fst z ∈ Wv)) (snd (envOne (fst z) ∈ fst (Sat W (toS ψ)))))
この所属を展開すると、W の中の表示と、defSet-Sat を通じて、その一変数環境が必要な充足集合に属することが得られます。表示と元の要素との等式に沿って、二つの結論をどちらも x のその要素へ戻します。
(λ { ((q , hq) , eq) → subst (λ u → ⟨ fst z ∈ u ⟩) (sym qw) (subst (λ u → ⟨ u ∈ fst W ⟩) eq (ι∈ q)) , subst (λ u → ⟨ envOne u ∈ fst (Sat W (toS ψ)) ⟩) eq (subst ⟨_⟩ (defSet-Sat W ψ q) ∣ (q , hq) , refl ∣₁) }) (subst (λ u → ⟨ fst z ∈ u ⟩) (sym e) hz) i : (z : S) → ⟨ fst z ∈ Wv ⟩ → ⟨ envOne (fst z) ∈ fst (Sat W (toS ψ)) ⟩ → ⟨ fst z ∈ fst x ⟩
Cuts の内向きの半分では、W の表示された要素から始め、その一変数環境が ψ を満たすと仮定します。充足の橋がこれを DA.defSet ψ への所属に変え、仮定した等式 DA.defSet ψ = fst x がその要素を x に入れます。
i z hw he = let fib = ∈-asFiber {a = fst z} {b = fst W} (subst (λ u → ⟨ fst z ∈ u ⟩) qw hw) in subst (λ u → ⟨ fst z ∈ u ⟩) e (subst (λ u → ⟨ u ∈ DA.defSet ψ ⟩) (fib .snd) (subst ⟨_⟩ (sym (defSet-Sat W ψ (fib .fst)))
最後の輸送は、選んだ要素の表示とその基礎の集合を揃えるだけです。したがって cut≡ と cuts-of を合わせると、ψ に対する Cuts 述語は、一つの定義可能部分集合 DA.defSet ψ との等しさに対応します。どちらの向きも定義論理式の一意性を主張しません。
(subst (λ u → ⟨ envOne u ∈ fst (Sat W (toS ψ)) ⟩) (sym (fib .snd)) he)))
これで健全性を正確に述べられます。作業集合の枠が W と同一視され、数を表すタグが正しく、satAt が符号集合と充足関係表を正しく保証しているという前提の下で、defAt の充足は値の枠をちょうど 𝒟ₒ (fst W) に定めます。ここで 𝒟ₒ が集めるのは、W の要素をパラメータに使える一階論理式で定義される W の部分集合であり、完全な内部冪集合ではありません。
def-sound : ⟨ γ ⊨ defAt v w T C N ⟩ → Vv ≡ 𝒟ₒ (fst W) def-sound hd = extensionalV (λ x → ⇔toPath (fwd x) (bwd x)) where hm = defAt-out v w T C N γ hd .fst ha = defAt-out v w T C N γ hd .snd
順方向の包含では、所属の節が命題的切り詰めの下で、鍵の形をした符号、充足関係表の項目、その項目が切り出す部分集合を記述する条件を与えます。satAt が候補の符号領域を実際のものと対応させた後、decodeAll は、符号が必要な第二成分をもつアリティ一の論理式が単に存在することだけを与えます。続いて表の値の補題が、その項目の値をこの論理式の充足集合と同一視します。
fwd : (x : V ℓ) → ⟨ x ∈ Vv ⟩ → ⟨ x ∈ 𝒟ₒ (fst W) ⟩
fwd x hx = PT.rec (snd (x ∈ 𝒟ₒ (fst W)))
(λ { (c , p , y , (c∈ , (ec , (e∈ , cuts)))) → PT.rec (snd (x ∈ 𝒟ₒ (fst W)))
(λ { (ψ , qp) →
𝒟ₒ-intro (fst W) x ∣ ψ , cut≡ ψ xS
Cuts の事実が、表の値の同定に沿って、復号された論理式の充足集合の中へ運ばれ、定義可能冪集合の導入が、切り出された集合を 𝒟ₒ の中に置きます。切り詰められた論理式の復号は、命題値の導入の中で消費されます。
(subst (λ u → Cuts x Wv u) (valOf ψ c y (ec ∙ cong (pr (# 1)) qp) e∈) cuts) ∣₁ }) (decodeAll c (SR.C-out c c∈) 1 (fst p) ec) }) (RD.mem-out hm xS hx) where xS : S
値の枠は、所属の条項の外向きの読み出しのために、台の要素として提示されます。
xS = down (lookup v γ) x hx
逆向きの包含では、𝒟ₒ (fst W) への所属から得られるのは、命題的に切り詰められた論理式 ψ と等式 DA.defSet ψ = x だけです。所属命題への消去の内部で、defAt の覆いの側が、この一時的な証人 ψ から作った鍵に対し、表の値と、値の枠に属する集合 x' を与えます。
bwd : (x : V ℓ) → ⟨ x ∈ 𝒟ₒ (fst W) ⟩ → ⟨ x ∈ Vv ⟩ bwd x hx = PT.rec (snd (x ∈ Vv)) (λ { (ψ , e) → PT.rec (snd (x ∈ Vv)) (λ { (y , x' , (e∈ , (x'∈ , cuts))) → subst (λ u → ⟨ u ∈ Vv ⟩)
切り出しの等式が、表の値の同定に沿って運ばれて、切り出された集合の基礎の集合を復元し、輸送がそれを値の枠の中へ置きます。
(sym (cut≡ ψ x' (subst (λ u → Cuts (fst x') Wv u) (valOf ψ (keyS W ψ) y refl e∈) cuts)) ∙ e) x'∈ }) (RD.all-out ha (keyS W ψ) (sndS (keyS W ψ) (# 1) (cd ψ) refl) (SR.C-in (keyS W ψ) (key∈AllCodes W ψ)) refl) }) (𝒟ₒ-inv (fst W) x hx)
完全性は同じ同値関係を逆向きにたどります。作業集合の同一視、正しいタグ、satAt を引き続き仮定すると、値の枠と 𝒟ₒ (fst W) との等式から defAt の充足を構成できます。二つの連言項はそれぞれ、列挙された各集合に定義論理式があることと、アリティ一の各論理式が定める部分集合が必ず現れることを示します。
def-complete : Vv ≡ 𝒟ₒ (fst W) → ⟨ γ ⊨ defAt v w T C N ⟩ def-complete qv = defAt-in v w T C N γ mem all where
それぞれの論理式の表の項目は、すでに定義された再帰の表から選ばれます。その表は、表の中での所属と、明示的な充足集合との同定の両方を保証します。
entry : (ψ : Formula Ab 1) → Σ[ y ∈ S ] (⟨ pr (fst (keyS W ψ)) (fst y) ∈ Tv ⟩ × (fst y ≡ fst (Sat W (toS ψ)))) entry ψ = Table.val W W (keyS W ψ) (key∈AllCodes W ψ) , ( SR.T-in (keyS W ψ) (key∈AllCodes W ψ) , cong fst (val-at W W ψ (keyS W ψ) (key∈AllCodes W ψ) refl) )
所属の連言項では、値の枠の要素を 𝒟ₒ (fst W) へ移し、𝒟ₒ-inv で展開します。定義論理式は命題的切り詰めの下でのみ存在します。その内部で論理式の鍵、対応する表の項目、必要な Cuts の証拠を組み立てますが、定義論理式を大域的に選んだり、標準的なデータとして保持したりはしません。
mem : ⟨ γ ⊨ memAt v w T C N ⟩ mem = RD.mem-in (λ x x∈ → PT.map (λ { (ψ , e) → keyS W ψ , sndS (keyS W ψ) (# 1) (cd ψ) refl , entry ψ .fst , ( SR.C-in (keyS W ψ) (key∈AllCodes W ψ)
ここで用いる表の値は、再帰的な充足関係表がこの論理式の鍵に対してすでに定めた値です。その値と明示的な充足集合との等式に沿って cuts-of を移せば、切り出しの証拠が得られます。この一時的な論理式の証人は終始 PT.map の内部にあり、得られる所属の証人も命題的に切り詰められたままです。
, ( refl , ( entry ψ .snd .fst , subst (λ u → Cuts (fst x) Wv u) (sym (entry ψ .snd .snd)) (cuts-of ψ x e) ) ) ) }) (𝒟ₒ-inv (fst W) (fst x) (subst (λ u → ⟨ fst x ∈ u ⟩) qv x∈)))
覆いの連言項は、符号の領域の中の、アリティ一のキーそれぞれに対して証明されます。対の分解が明示的に名指されます。
all : ⟨ γ ⊨ allAt v w T C N ⟩ all = RD.all-in (λ c p c∈ ec → PT.map (λ { (ψ , qp) → let qc : fst c ≡ fst (keyS W ψ) qc = ec ∙ cong (pr (# 1)) qp
与えられたアリティ一の鍵に対し、復号は、その第二成分を符号にもつ論理式 ψ が単に存在することだけを与えます。定義可能部分集合 DA.defSet ψ は導入によって 𝒟ₒ (fst W) に属し、仮定した等式に沿う輸送で値の枠に入ります。復号は一意な論理式や標準的な論理式を選びません。
xS : S xS = down (lookup v γ) (DA.defSet ψ) (subst (λ u → ⟨ DA.defSet ψ ∈ u ⟩) (sym qv) (𝒟ₒ-intro (fst W) (DA.defSet ψ) ∣ ψ , refl ∣₁)) in entry ψ .fst , xS , ( subst (λ u → ⟨ pr u (fst (entry ψ .fst)) ∈ Tv ⟩) (sym qc) (entry ψ .snd .fst)
充足関係表は、復号された論理式の鍵に対応する値を与え、cuts-of は、その値が作業集合からちょうど DA.defSet ψ を切り出すことを示します。先ほど得た所属と合わせれば、これらのデータは覆いの条項を満たします。decodeAll の結果は命題的に切り詰められ、この命題値の条項にだけ消去されるので、構成は存在だけを記録し、復号された論理式を保持しません。
, ( subst (λ u → ⟨ DA.defSet ψ ∈ u ⟩) (sym qv) (𝒟ₒ-intro (fst W) (DA.defSet ψ) ∣ ψ , refl ∣₁) , subst (λ u → Cuts (DA.defSet ψ) Wv u) (sym (entry ψ .snd .snd)) (cuts-of ψ xS refl) ) ) }) (decodeAll c (SR.C-out c c∈) 1 (fst p) ec))
公開される健全性の向きは、後で実際に使う正確なインターフェースを示します。作業集合の枠が W を表し、Tags が数の枠を固定し、satAt が符号と充足のデータを保証すれば、defAt から 𝒟ₒ (fst W) との等しさが従います。したがって、この有界論理式が意図した意味をもつのは、このように整えられた背景の中です。
def-sound : ∀ {m} (v w T C E : Fin m) (N : Fin 10 → Fin m) (γ : S ^ m) (W : S) → fst (lookup w γ) ≡ fst W → Tags γ N → ⟨ γ ⊨ satAt T w C E N ⟩ → ⟨ γ ⊨ defAt v w T C N ⟩ → fst (lookup v γ) ≡ 𝒟ₒ (fst W) def-sound v w T C E N γ W qw tg hs = DefRead.def-sound v w T C E N γ W qw tg hs
公開される完全性の向きは同じ仮定をもち、含意を逆にします。𝒟ₒ (fst W) との等しさから defAt の充足が再構成されます。二つの定理を合わせると、各要素の代表論理式を選ぶことも、完全な内部冪集合と同一視することもなく、定義可能部分集合の集まりが特徴づけられます。
def-complete : ∀ {m} (v w T C E : Fin m) (N : Fin 10 → Fin m) (γ : S ^ m) (W : S) → fst (lookup w γ) ≡ fst W → Tags γ N → ⟨ γ ⊨ satAt T w C E N ⟩ → fst (lookup v γ) ≡ 𝒟ₒ (fst W) → ⟨ γ ⊨ defAt v w T C N ⟩ def-complete v w T C E N γ W qw tg hs = DefRead.def-complete v w T C E N γ W qw tg hs