Bedrockこの章を読むか、読書案内と依存マップで別のルートを選べます。
読書案内 · 依存マップ後の凝縮の議論では、ある集合が与えられた順序数における構成可能段階である、という主張を移す必要があります。初等性が移すのは論理式であって、外部で定義された演算 Lset ではありません。そこで本章は、同じ段階関係を認識する有界な対象言語の論理式を作り、第三の集合をすべての補助的な証人に共通する上界として用います。
{-# OPTIONS --cubical --safe --guardedness #-}
この構成で用いる古典性は、固定された一つの排中律の実例だけに由来します。それでも有界存在の論理式は命題的に切り詰められた存在として読まれるため、古典的な背景から、隠れた表を大域的に選んだデータが得られるわけではありません。
open import Base.Prelude open import Base.Classical using ( LEM )
宇宙レベル ℓ と、レベル ℓ-suc ℓ の命題に対する排中律を固定します。本章の論理式、読み補題、そして最終的な正しさの定理は、すべてこの一つの明示的な古典的仮定に相対して述べられます。
module L.GCH.HierarchyDescription {ℓ : Level} (lem : LEM (ℓ-suc ℓ)) where
ここで対象言語に必要なのは、所属、連言、真、偽、有界量化子だけです。これらの構成子には構造に沿った Δ₀ の証人があります。後で定数が現れないことを示せば、定数域を空のアルファベットへ変えられます。こうして自由変数を残したまま、最終的な三変数の論理式をパラメータなしにします。
open import FOL.ZFStructure using ( module hPropStructure ) open import FOL.Syntax using ( Formula; var; _∈̇_; _∧̇_; ⊤̇; ⊥̇; ∃̇∈; ∀̇∈ ) open import FOL.LevyHierarchy using ( Δ₀; checkΔ₀; δ-∧; δ-∃∈ ) open import FOL.Manipulation.ConstantOccurrences using ( countFo ) open import FOL.Manipulation.ConstantMapping using ( embed )
同じ有界論理式は、構成可能な台の内部でも、周囲の累積階層でも読めます。Δ₀ 絶対性がこの二つの読みを同定します。所属帰納法は、より下の行から現在の表の行を検証し、外延性は、そこから得られる二つの所属の含意を段階の等しさへ変えます。
open import FOL.Manipulation.Relabelling using ( embed-⊨; mapΔ₀ ) import FOL.Absoluteness import FOL.Semantics open import V.Hierarchy {ℓ} using ( 𝒮ᵥ; ∈-induction; extensionalV ) open import V.Coding {ℓ} using ( pr )
段階 Lset b は、それ以前の段階の定義可能冪集合から組み立てられます。その各要素は、ある c ∈ b に対する 𝒟ₒ (Lset c) から来ており、そのような寄与はすべて Lset b に属します。所属についての内向きと外向きの規則がこの二方向を表し、順序数の事実が、後で使う添字が実際に段階の添字であることを保証します。
open import L.Constructible {ℓ} using ( 𝒮ʟ; isL; isL-trans; IsOrd; Lset; Lset-in; Lset-out; Lset-mono; 𝒟ₒ ) open import L.Ordinal {ℓ} using ( mem-ord; suc-ord; #∈ω ) open import L.Axioms.Basic {ℓ} using ( LsetS; Lset-suc ) open import L.Axioms.Numerals {ℓ} using ( numeralL-fst )
一つの定義可能冪集合を内部で認識するには、論理式の符号、充足関係表、環境の塔が必要です。順序対の符号化は、各段階の添字をその記録された値と結びつけます。これらの補助集合はすべて同じ証人集合 z で有界化されるため、記述全体が Δ₀ にとどまります。
open import L.Coding.Expressions {ℓ} using ( sucAtL ) open import L.Coding.NumeralBound {ℓ} lem using ( module Bound ) open import L.Coding.CodeSet {ℓ} lem using ( AllCodes ) open import L.Coding.Model {ℓ} using ( container ) open import L.Coding.Quantification {ℓ} using
対象言語の内部では、集合として符号化された順序対の成分を非有界な演算で射影することはできません。代わりに、有界な成分論理式が小さな容器の中を動き、そこで対を読んだり埋めたりします。十個の名前付きスロットには符号化の記述で使う数項タグが入り、新しい証人で環境を拡張するときには、その名前をずらして位置を保ちます。
( sh; i0; i1; i2; i3; i8; f0; f1; f2; f3; f4; f5; f6; f7; f8; f9 ; down; suc-out; suc-in; sndEx; sndAll; bothAll ; sndEx-out; sndAll-in; bothAll-in; fillSnd; useSnd; useBoth; sndS ) open import L.Coding.CodeDomain {ℓ} using ( Tags; shN ) open import L.Coding.EnvironmentTower {ℓ} lem using ( nn; module Tower )
ここでは三つの意味論的な仕様が合流します。階層表は上界より下の対 (c,Lset c) を記録し、充足の記述は一つの段階上の真正な符号、環境、充足関係のデータを認識し、定義可能冪集合の記述は集合 𝒟ₒ (Lset c) を認識します。健全性が復元する表の性質は Values と Entries だけであり、完全性は正確な仕様 IsHier から始まります。
open import L.Hierarchy {ℓ} lem using ( hierL-spec; IsHier; hier-out; hier-in; Values; Entries ) open import L.GCH.SkolemHull {ℓ} lem using ( module Cnt; erase-Δ₀; isOrd-at-p; Δ₀-isOrd-at-p; _⊨ₚ_ ) open import L.Coding.SatisfactionGraphSet {ℓ} lem using ( module SatGraph ) open import L.GCH.SatisfactionDescription {ℓ} lem using ( satAt; sat-complete ) open import L.GCH.DefinablePowerSetDescription {ℓ} lem using ( defAt; def-sound; def-complete )
完全性には、すべての補助的な証人を含む一つの共通段階が必要です。γ が十分で c ∈ γ なら、Lset γ は c で必要な階層表、符号集合、充足関係表、環境の塔を含みます。後続に関する閉性は次の段階もそこへ入れ、ω ∈ γ は十個の有限な数項タグをすべて与えます。
open import L.GCH.AdequateStages {ℓ} lem using ( Adequate; module Adequate; module At; Lset∈suc )
環境は構成可能集合からなる有限ベクトルです。有界な証人を導入すると、それは先頭に置かれ、以前の各スロットは一つずつ後ろへずれます。有限添字がこのずれを明示します。この管理によって、同じ段階、表、上界の名前を、入れ子になった複数の量化子の中でも保つことができます。
open import Cubical.Data.Nat using ( _+_ ) open import Cubical.Data.Vec using ( _∷_; []; map; lookup ) open import Cubical.Data.Sigma using ( _×_ ) open import Cubical.Data.Unit using ( tt ) open import Cubical.Data.FinData using ( toℕ; weakenFin )
存在論理式の充足が保つのは命題的切り詰めだけです。適切なデータが存在することを記録し、どのデータを使ったかは忘れます。したがって、後で切り詰めを除去するときの行き先は常に命題です。ここでは所属が命題値であり、累積階層の集合の等しさも命題なので、証明で必要な二種類の結論はいずれも正当な行き先になります。
open import Cubical.Functions.Logic using ( ⇔toPath ) import Cubical.Data.Empty as Empty import Cubical.HITs.PropositionalTruncation as PT open PT using ( ∥_∥₁; ∣_∣₁; squash₁ ) open import Cubical.HITs.CumulativeHierarchy.Base using ( V; _∈_; setIsSet )
十個の有限なタグは、階層内部の von Neumann 数項で表されます。零は空集合であり、後の各タグは集合論的な後続によって得られ、十個すべてが ω に属します。所属の読みは、これらの周囲の集合を、構成可能な台の要素としての表示と結びつけます。
open import Cubical.HITs.CumulativeHierarchy.Properties using ( ∈∈ₛ ) open import Cubical.HITs.CumulativeHierarchy.Constructions using ( ∅; ∅-empty; module InfinitySet ) open InfinitySet {ℓ} using ( #_; sucV; ω )
構成可能モデルの台を S と書きます。その要素は、周囲の集合とその構成可能性の証明を組にして提示します。隠れた表と証人はすべてこの台の上で量化され、最後に見えるスロットも、値 a、その段階の添字 p、共通の上界 z をそれぞれ提示します。
open hPropStructure 𝒮ʟ using ( S )
L の内部での充足と周囲の階層での充足は異なる構造を使いますが、パラメータが L から来る Δ₀ 論理式については一致します。補題 abs₀ が両者の橋です。この橋により、完全性は内部で論理式の充足を組み立て、健全性は移された論理式を周囲での段階の等しさとして読み戻せます。
module AbsL = FOL.Absoluteness.Single 𝒮ᵥ isL isL-trans using ( _^_; _⊨ᵐ_; abs₀ ) open AbsL using ( _^_ ) renaming ( _⊨ᵐ_ to _⊨_ ) module SemVᵃ = FOL.Semantics 𝒮ᵥ
論理式 defIn w z N body は、四重の有界存在量化子を使って、充足関係表 T、符号集合 C、環境の塔 E、値 d を z の中に置きます。充足の記述は w の値上の T、C、E を検証し、定義可能冪集合の記述は d をその値の定義可能冪集合と同定し、body はその d に対する追加の条件を述べます。充足が保つのはこれらの証人の命題的切り詰めだけであり、この論理式は z を一意には特徴づけません。
defIn : ∀ {k} → Fin k → Fin k → (Fin 10 → Fin k) → Formula S (4 + k) → Formula S k defIn w z N body = ∃̇∈ (var z) (∃̇∈ (var (sh 1 z)) (∃̇∈ (var (sh 2 z)) (∃̇∈ (var (sh 3 z)) (satAt i3 (sh 4 w) i2 i1 (shN 4 N) ∧̇ (defAt i0 (sh 4 w) i3 i2 (shN 4 N) ∧̇ body)))))
内向きの包含を表す intoAt は、各 x ∈ v が、それ以前の段階の添字 c ∈ b によって説明されることを述べます。すなわち、f の順序対の形をしたある要素が c で値 w を記録し、x は w の定義可能冪集合に属します。外側の有界な形は ∀[ x ∈ v ] ∃[ c ∈ b ] ... であり、残りの有界な証人が、その行と冪集合を認識するためのデータを展開します。
intoAt : ∀ {m} → Fin m → Fin m → Fin m → Fin m → (Fin 10 → Fin m) → Formula S m intoAt v b f z N = ∀̇∈ (var v) (∃̇∈ (var (sh 1 b)) (∃̇∈ (var (sh 2 f)) (sndEx i0 i1 (defIn i0 (sh 5 z) (shN 5 N) (var i8 ∈̇ var i0)))))
逆向きの包含を表す overAt は、c ∈ b と、対 (c,w) として提示される f の要素を動きます。そのような提示ごとに、w の定義可能冪集合のすべての要素が v に属することを要求します。この節は、そのような対として提示されない f の要素については何も述べないため、候補表全体から任意の余分な要素を排除するものとは読めません。
overAt : ∀ {m} → Fin m → Fin m → Fin m → Fin m → (Fin 10 → Fin m) → Formula S m overAt v b f z N = ∀̇∈ (var b) (∀̇∈ (var (sh 1 f)) (sndAll i0 i1 (defIn i0 (sh 4 z) (shN 4 N) (∀̇∈ (var i0) (var i0 ∈̇ var (sh 9 v))))))
連言 stepAt は二つの包含をまとめます。b より下に記録された対の行に相対して、intoAt は v に余分な要素がないことを述べ、overAt は定義可能冪集合からの寄与が一つも欠けないことを述べます。表の値が正しいことは、後の読み補題が別に要求する仮定です。
stepAt : ∀ {m} → Fin m → Fin m → Fin m → Fin m → (Fin 10 → Fin m) → Formula S m stepAt v b f z N = intoAt v b f z N ∧̇ overAt v b f z N
approxAt の前半は被覆を与えます。すべての c ∈ b について、f に順序対の形をした何らかの項目があります。後半は、f の要素が対 (c,w) として提示されたときに stepAt w c f z N を検査します。f の各要素が対であることも、記録された各第一成分が b より下にあることも述べません。したがって approx-out が復元するのは正確に Values f b × Entries f b であり、表全体と階層グラフとの等しさでも、大域的に余分な要素がないという性質でもありません。
approxAt : ∀ {m} → Fin m → Fin m → Fin m → (Fin 10 → Fin m) → Formula S m approxAt f b z N = ∀̇∈ (var b) (∃̇∈ (var (sh 1 f)) (sndEx i0 i1 ⊤̇)) ∧̇ ∀̇∈ (var f) (bothAll i0 (stepAt i0 i1 (sh 4 f) (sh 4 z) (shN 4 N)))
節 hierAt a p f z N は、p より下の近似と、p における最後の一段階を結びつけます。近似から Values と Entries が得られれば、最後の一段階は a を Lset p と同定します。逆に、正確な階層表 IsHier p f と十分な証人の供給があれば、二つの連言を埋められます。これは、最終的な三変数の論理式が有界な証人の背後に隠す、局所的な段階関係です。
hierAt : ∀ {m} → Fin m → Fin m → Fin m → Fin m → (Fin 10 → Fin m) → Formula S m hierAt a p f z N = approxAt f p z N ∧̇ stepAt a p f z N
タグの節は、十の枠を数項に固定します。最初の枠には要素がないので、それは空集合です。
pins : ∀ {m} → (Fin 10 → Fin m) → Formula S m pins N = ∀̇∈ (var (N f0)) ⊥̇ ∧̇ ( sucAtL (N f0) (N f1) ∧̇ ( sucAtL (N f1) (N f2) ∧̇ ( sucAtL (N f2) (N f3) ∧̇ ( sucAtL (N f3) (N f4) ∧̇ ( sucAtL (N f4) (N f5) ∧̇ ( sucAtL (N f5) (N f6)
残りの九つの枠は九つの後続の主張でつながれ、こうして十の枠は、数項の 0 から 9 にちょうどなります。
∧̇ ( sucAtL (N f6) (N f7) ∧̇ ( sucAtL (N f7) (N f8) ∧̇ sucAtL (N f8) (N f9) ))))))))
階層表を表す有界な節
後の記述で十個のタグを使うには、対象言語での固定条件が意味論的な記録 Tags γ N と一致しなければなりません。次の二つの補題が両方向を示します。一方は pins から数項の等式を読み、もう一方はその等式から pins を再構成します。
module PinsRead {m : ℕ} (N : Fin 10 → Fin m) (γ : S ^ m) where
タグの節の読みは、まず最初の枠が空であることを示します。要素をもたないのです。
pins-out : ⟨ γ ⊨ pins N ⟩ → Tags γ N pins-out (h0 , hs) = go where q0 : fst (lookup (N f0) γ) ≡ # 0 q0 = extensionalV (λ y → ⇔toPath
空であることは、両方向の外延性の議論です。最初の枠のどんな要素も偽の節と矛盾し、そもそも空集合には要素がありません。
(λ y∈ → Empty.rec* (h0 (down (lookup (N f0) γ) y y∈) y∈)) (λ y∈ → Empty.rec (∅-empty y (∈∈ₛ {a = y} {b = ∅} .fst y∈))))
補助補題 up は数項の鎖を一つ進めます。スロット i が # k を表し、sucAtL i j が成り立つなら、その健全な読みはスロット j を sucV (# k)、したがって数項 # (suc k) と同定します。
up : (i j : Fin m) (k : ℕ) → ⟨ γ ⊨ sucAtL i j ⟩ → fst (lookup i γ) ≡ # k → fst (lookup j γ) ≡ # (suc k) up i j k h q = suc-out i j γ h ∙ cong sucV q
零についての等式から始め、最初の五つの後続の節によって q1 から q5 が順に得られます。したがって f1 から f5 が名付けるスロットは、それぞれ数項一から五と同定されます。
q1 = up (N f0) (N f1) 0 (hs .fst) q0 q2 = up (N f1) (N f2) 1 (hs .snd .fst) q1 q3 = up (N f2) (N f3) 2 (hs .snd .snd .fst) q2 q4 = up (N f3) (N f4) 3 (hs .snd .snd .snd .fst) q3 q5 = up (N f4) (N f5) 4 (hs .snd .snd .snd .snd .fst) q4
残り四つの後続の節が同じ鎖を続け、q6 から q9 を与えます。これにより、スロット f6 から f9 は数項六から九と同定され、数項についての読みが完成します。
q6 = up (N f5) (N f6) 5 (hs .snd .snd .snd .snd .snd .fst) q5 q7 = up (N f6) (N f7) 6 (hs .snd .snd .snd .snd .snd .snd .fst) q6 q8 = up (N f7) (N f8) 7 (hs .snd .snd .snd .snd .snd .snd .snd .fst) q7 q9 = up (N f8) (N f9) 8 (hs .snd .snd .snd .snd .snd .snd .snd .snd) q8
記録 Tags γ N は、Fin 10 の各要素について対応する数項の等式を要求します。最初の四つの場合は q0、q1、q2、q3 を返し、零から三までのタグに対応します。
go : Tags γ N go zero = q0 go (suc zero) = q1 go (suc (suc zero)) = q2 go (suc (suc (suc zero))) = q3
go の次の五つの場合は q4 から q8 を返します。入れ子の後続として書かれたこれらのパターンは、追加の算術的な議論なしに、タグ四から八を尽くします。
go (suc (suc (suc (suc zero)))) = q4 go (suc (suc (suc (suc (suc zero))))) = q5 go (suc (suc (suc (suc (suc (suc zero)))))) = q6 go (suc (suc (suc (suc (suc (suc (suc zero))))))) = q7 go (suc (suc (suc (suc (suc (suc (suc (suc zero)))))))) = q8
Fin 10 に残る唯一の場合は、零の九回目の後続であり、q9 を返します。これで場合分けは、Tags γ N が要求する十個すべての数項の等式を与えます。
go (suc (suc (suc (suc (suc (suc (suc (suc (suc zero))))))))) = q9
逆向きには、スロットがすでに Tags γ N を満たすとします。零のスロットの要素と仮定されたものは、タグの等式に沿って空集合の要素へ移されるため、存在できません。同じタグの等式が、九つの後続の節を埋めるためのデータも与えます。
pins-in : Tags γ N → ⟨ γ ⊨ pins N ⟩ pins-in tg = (λ x x∈ → Empty.rec (∅-empty (fst x) (∈∈ₛ {a = fst x} {b = ∅} .fst (subst (λ u → ⟨ fst x ∈ u ⟩) (tg f0) x∈)))) , ( st f0 f1 refl , ( st f1 f2 refl , ( st f2 f3 refl , ( st f3 f4 refl , ( st f4 f5 refl , ( st f5 f6 refl
各後続の節は、二つのタグのスロットを対応する数項の等式に沿って書き換えた後、後続論理式の内向きの読みを適用して再構成します。
, ( st f6 f7 refl , ( st f7 f8 refl , st f8 f9 refl )))))))) where st : (j k : Fin 10) → # (toℕ k) ≡ sucV (# (toℕ j)) → ⟨ γ ⊨ sucAtL (N j) (N k) ⟩ st j k e = suc-in (N j) (N k) γ (tg k ∙ e ∙ cong sucV (sym (tg j)))
十個の名前付きスロットが必要な数項の値をもつ環境 δ を固定します。w にある底集合を Wv、z にある底集合を Zv とします。前者は定義可能性を解釈する段階であり、後者は四つの証人を含まなければならない共通の上界です。
module DefInRead {k : ℕ} (w z : Fin k) (N : Fin 10 → Fin k) (body : Formula S (4 + k)) (δ : S ^ k) (tg : Tags δ N) where private Wv = fst (lookup w δ) Zv = fst (lookup z δ)
四つの証人は T、C、E、d の順に束縛されます。新しい束縛子は環境の先頭を拡張するため、本体は d ∷ E ∷ C ∷ T ∷ δ で評価されます。したがって先頭の四つのスロットは、定義可能冪集合の値、環境の塔、符号集合、充足関係表をこの順に指します。
δ4 : (T C E d : S) → S ^ (4 + k) δ4 T C E d = d ∷ E ∷ C ∷ T ∷ δ
defIn を読むとき、四つの証人 T、C、E、d を囲む命題的切り詰めは保たれます。その結論が意図的に残すのは、d ∈ z、d = 𝒟ₒ Wv、そして拡張された環境で本体が成り立つことだけです。T、C、E が z に属する証明と、内部の充足および冪集合の記述の証明は、この弱い主張を導く途中で消費されます。
defIn-out : ⟨ δ ⊨ defIn w z N body ⟩ → ∥ Σ[ T ∈ S ] Σ[ C ∈ S ] Σ[ E ∈ S ] Σ[ d ∈ S ] (⟨ fst d ∈ Zv ⟩ × ((fst d ≡ 𝒟ₒ Wv) × ⟨ δ4 T C E d ⊨ body ⟩)) ∥₁ defIn-out = PT.rec squash₁ (λ { (T , (T∈ , h1)) → PT.rec squash₁ (λ { (C , (C∈ , h2)) → PT.rec squash₁ (λ { (E , (E∈ , h3)) → PT.map (λ { (d , (d∈ , (hs , (hd , hb)))) →
四重の切り詰めから証人を取り出した後、def-sound は充足の記述 hs と定義可能冪集合の記述 hd を組み合わせます。ここに残される唯一の等式は、その結論 d = 𝒟ₒ Wv であり、本体の証明はそのまま先へ渡されます。
T , C , E , d , ( d∈ , ( def-sound i0 (sh 4 w) i3 i2 i1 (shN 4 N) (δ4 T C E d) (lookup w δ) refl tg hs hd , hb )) }) h3 }) h2 }) h1 })
逆に、意味論的なデータから defIn を示すには、真正な証人を明示的に与える必要があります。w で表される構成可能な台 W、四つの集合とそれらが z に属する証明、真正な充足関係表、符号集合、環境の塔、定義可能冪集合とのそれぞれの同定、そして本体の証明を与えます。したがってこの向きでは、外向きの読みが意図的に忘れるデータを仮定します。
defIn-in : (W : S) → Wv ≡ fst W → (T C E d : S) → ⟨ fst T ∈ Zv ⟩ → ⟨ fst C ∈ Zv ⟩ → ⟨ fst E ∈ Zv ⟩ → ⟨ fst d ∈ Zv ⟩ → fst T ≡ fst (SatGraph.pairs W) → fst C ≡ fst (AllCodes W) → fst E ≡ fst (Tower.tower W) → fst d ≡ 𝒟ₒ (fst W) → ⟨ δ4 T C E d ⊨ body ⟩ → ⟨ δ ⊨ defIn w z N body ⟩ defIn-in W qw T C E d T∈ C∈ E∈ d∈ qT qC qE qd hb =
内向きの読みでは、まず sat-complete が、真正な充足関係表、符号集合、環境の塔が satAt を満たすことを示します。次に def-complete が、その証明と与えられた d の等式を使って、定義可能冪集合の節を示します。与えられた本体の証明で連言が完成し、その後、四つの証人とそれぞれの所属証明が、入れ子の命題的切り詰めの中へ順に導入されます。
∣ T , ( T∈ , ∣ C , ( C∈ , ∣ E , ( E∈ , ∣ d , ( d∈ , ( hs , ( def-complete i0 (sh 4 w) i3 i2 i1 (shN 4 N) (δ4 T C E d) W qw tg hs qd , hb ))) ∣₁ ) ∣₁ ) ∣₁ ) ∣₁ where hs : ⟨ δ4 T C E d ⊨ satAt i3 (sh 4 w) i2 i1 (shN 4 N) ⟩ hs = sat-complete i3 (sh 4 w) i2 i1 (shN 4 N) (δ4 T C E d) W qw qT qC qE tg
述語 Supply は、c が順序数なら、defIn が必要とする四つの証人がすでに共通の上界の中にあることを述べます。その四つとは、段階 Lset c の充足グラフ、符号集合、環境の塔、および次の段階 Lset (sucV c) です。
Supply : (Zv : V ℓ) (c : V ℓ) → IsOrd c → Type (ℓ-suc ℓ) Supply Zv c oc = ⟨ fst (SatGraph.pairs (LsetS c oc)) ∈ Zv ⟩ × ( ⟨ fst (AllCodes (LsetS c oc)) ∈ Zv ⟩ × ( ⟨ fst (Tower.tower (LsetS c oc)) ∈ Zv ⟩
第四の成分が次の段階であり、近似の後続の一歩に必要なものです。
× ⟨ Lset (sucV c) ∈ Zv ⟩ ))
環境 γ における一つの候補となる階層の段階を固定します。候補の結果を Vv、それ以前の添字の集合を Bv、候補表の底集合を Fv と書きます。問うのは、Fv の関係する行が正しく、かつ存在すると分かったとき、二つの有界な包含から Vv = Lset Bv が強制されるかどうかです。
module StepRead {m : ℕ} (v b f z : Fin m) (N : Fin 10 → Fin m) (γ : S ^ m) (tg : Tags γ N) where private Vv = fst (lookup v γ) Bv = fst (lookup b γ) Fv = fst (lookup f γ)
共通の上界の底集合を Zv と書きます。これは、補助的な充足関係、符号、環境の塔、定義可能冪集合の証人をどこで見つけられるかを制御します。一段階から得たい等式には Zv は現れません。この上界は記述を可能にしますが、得られる段階の値の一部にはなりません。
Zv = fst (lookup z γ)
内向きの本体では、d は defIn が認識する定義可能冪集合であり、x は外側の v 上の有界全称量化子が導入した要素です。原子論理式の本体は x ∈ d を述べます。記録された値 w を Lset c と同定すれば、これはある c ∈ b に対する 𝒟ₒ (Lset c) への所属になります。
intoBody : Formula S (5 + m) intoBody = defIn i0 (sh 5 z) (shN 5 N) (var i8 ∈̇ var i0)
over の本体は定義可能冪集合の記述であり、その内側の論理式は、記述された集合のすべての要素が候補となる次の値に属することを述べます。これは合併の等式に必要な逆向きの包含を与えます。
overBody : Formula S (4 + m) overBody = defIn i0 (sh 4 z) (shN 4 N) (∀̇∈ (var i0) (var i0 ∈̇ var (sh 9 v)))
一段階の読み補題は、Bv より下の各対の行が正しい値をもつこと (Values) と、Bv より下の各添字に正準な行があること (Entries) を別々に仮定します。ちょうどこの二つの仮定のもとで、stepAt の二つの部分が反対向きの所属の含意を与え、外延性から Vv = Lset Bv が得られます。これらの仮定が制約するのは関係する対の行だけであり、候補表の無関係な要素を排除するものではありません。
step-out : ⟨ γ ⊨ stepAt v b f z N ⟩ → Values (lookup f γ) Bv → Entries (lookup f γ) Bv → Vv ≡ Lset Bv step-out (hi , ho) vals ents = extensionalV (λ x → ⇔toPath (fwd x) (bwd x)) where fwd : (x : V ℓ) → ⟨ x ∈ Vv ⟩ → ⟨ x ∈ Lset Bv ⟩ fwd x x∈ = PT.rec (snd (x ∈ Lset Bv)) (λ { (c , (c∈ , h1)) → PT.rec (snd (x ∈ Lset Bv))
前向きの包含では、intoAt が段階の添字 c ∈ Bv、表の対の行 (c,w)、そして x を含む定義可能冪集合の値 d を与えます。仮定 Values は w を Lset c と同定するので、d = 𝒟ₒ (Lset c) です。段階への内向きの規則 Lset-in が、この寄与から x を Lset Bv へ運びます。
(λ { (q , (q∈ , h2)) → PT.rec (snd (x ∈ Lset Bv)) (λ { (w , s , (eq , h3)) → PT.rec (snd (x ∈ Lset Bv)) (λ { (T , C , E , d , (d∈ , (qd , hx))) → Lset-in Bv (fst c) x c∈ (subst (λ u → ⟨ x ∈ u ⟩) (qd ∙ cong 𝒟ₒ (vals c w c∈ (subst (λ u → ⟨ u ∈ Fv ⟩) eq q∈))) hx) })
入れ子の存在形を読む各段階で、命題的切り詰めは保たれます。まず sndEx-out が、対の形をした表の項目から第二成分 w が単に存在することを復元し、次に defIn-out が、補助データと、d を w の定義可能冪集合と同定する等式が単に存在することを復元します。各切り詰めは、所属命題 x ∈ Lset Bv へ直接除去されます。
(DefInRead.defIn-out i0 (sh 5 z) (shN 5 N) (var i8 ∈̇ var i0) (w ∷ s ∷ q ∷ c ∷ xS ∷ γ) tg h3) }) (sndEx-out i0 i1 intoBody (q ∷ c ∷ xS ∷ γ) h2) }) h1 }) (hi xS x∈) where
証明は周囲の要素 x ∈ Vv から始まりますが、論理式は構成可能な台 S の上で解釈されます。演算 down はこの所属証明を使って x を台の要素 xS として提示します。xS を環境の先頭に置くと、新しく束縛されたスロットは同じ底集合 x を表します。
xS : S xS = down (lookup v γ) x x∈
step-out の逆向きの包含は、実際の段階 Lset Bv の要素を候補の値 Vv に入れます。これは Lset Bv の切り詰められた段階分解を消去し、x がその定義可能冪集合に属するような、より前の段階 δ についての主張へ帰着させます。
bwd : (x : V ℓ) → ⟨ x ∈ Lset Bv ⟩ → ⟨ x ∈ Vv ⟩ bwd x x∈ = PT.rec (snd (x ∈ Vv)) put (Lset-out Bv x x∈) where put : Σ[ δ ∈ V ℓ ] (⟨ δ ∈ Bv ⟩ × ⟨ x ∈ 𝒟ₒ (Lset δ) ⟩) → ⟨ x ∈ Vv ⟩ put (δ , (δ∈ , xD)) = PT.rec (snd (x ∈ Vv))
Lset-out がより前の添字 δ を示すと、完全性が正準な表の項目 (δ, Lset δ) を与えます。over の節をこの項目に適用し、さらに defIn-out がそこで有界化された集合 d を 𝒟ₒ (Lset δ) と同一視します。したがって、その全称な本体は与えられた x を候補の値 Vv に入れます。この向きで使うのは Entries が与える正準な項目であり、Values への別の訴えは要りません。
(λ { (T , C , E , d , (d∈ , (qd , hsub))) → hsub (down d x (subst (λ u → ⟨ x ∈ u ⟩) (sym qd) xD)) (subst (λ u → ⟨ x ∈ u ⟩) (sym qd) xD) }) (DefInRead.defIn-out i0 (sh 4 z) (shN 4 N) (∀̇∈ (var i0) (var i0 ∈̇ var (sh 9 v))) (w ∷ container q c w refl .fst ∷ q ∷ c ∷ γ) tg (useSnd i0 (q ∷ c ∷ γ) c w refl overBody i1 refl (ho c δ∈ q (ents c δ∈))))
名づけられる二つの対象は、符号化された引数と符号化された対です。どちらも、所属の証明を下降して台の要素として提示されます。
where c : S c = down (lookup b γ) δ δ∈ q : S q = down (lookup f γ) (pr δ (Lset δ)) (ents c δ∈)
行の値 w は、対の提示から読まれ、本体の充足が消費する成分です。
w : S w = sndS q δ (Lset δ) refl
ステップの条項の内向きの方向には、五つの仮定が要ります。界の順序数性、提案された値と界での段階の同定、界での表の正しさと完備さ、そして界の各要素のための補助の証人を証人の界の中に置く供給関数です。証明は二つの連言項に分かれます。
step-in : (ob : IsOrd Bv) → Vv ≡ Lset Bv → Values (lookup f γ) Bv → Entries (lookup f γ) Bv → ((c : V ℓ) (oc : IsOrd c) → ⟨ c ∈ Bv ⟩ → Supply Zv c oc) → ⟨ γ ⊨ stepAt v b f z N ⟩ step-in ob vq vals ents sup = into , over where
into の連言項は、提案された値の要素 x から外向きに読まれます。界での段階の切り詰められた分解が、より前の順序数と定義可能冪集合への所属を名指し、存在の導入がそれを二つの有界量化子に満たします。
into : ⟨ γ ⊨ intoAt v b f z N ⟩ into x x∈ = PT.rec squash₁ put (Lset-out Bv (fst x) (subst (λ u → ⟨ fst x ∈ u ⟩) vq x∈)) where put : Σ[ δ ∈ V ℓ ] (⟨ δ ∈ Bv ⟩ × ⟨ fst x ∈ 𝒟ₒ (Lset δ) ⟩) → ⟨ (x ∷ γ) ⊨ ∃̇∈ (var (sh 1 b)) (∃̇∈ (var (sh 2 f)) (sndEx i0 i1 intoBody)) ⟩
入れ子になった有界存在量化子は、命題的切り詰めからデータを取り出すことなく満たされます。証明は δ を台の要素 c として提示し、Entries によって正準な対を q として提示し、fillSnd で対の分解を与えます。残る本体が hb です。充足は命題なので、各構成子は ∃[]-syntax に組み込まれた命題的切り詰めを保ちます。
put (δ , (δ∈ , xD)) = ∣ c , ( δ∈ , ∣ q , ( ents c δ∈ , fillSnd i0 (q ∷ c ∷ x ∷ γ) c w refl intoBody hb i1 refl ) ∣₁ ) ∣₁ where oδ : IsOrd δ oδ = mem-ord {A = Bv} ob δ δ∈
三つの台の要素は、それぞれ異なる根拠から得られます。所属 δ ∈ Bv はより前の添字を c として提示し、正準な対が表に属するという証明はその対を q として提示し、δ の順序数性によって LsetS は段階 Lset δ を w として提示できます。有界な証人を組み立てる際には、これらの由来を区別することが大切です。
c : S c = down (lookup b γ) δ δ∈ q : S q = down (lookup f γ) (pr δ (Lset δ)) (ents c δ∈) w : S
ここで w は構成可能な台における実際の段階 Lset δ です。供給の仮定を δ に適用すると、その充足関係表、符号集合、環境の塔、後継段階がいずれも Zv に属するという証明が得られます。この四つの界とそれらを同定する等式により、defIn-in は残る課題を数学的事実 x ∈ 𝒟ₒ (Lset δ) に帰着させます。
w = LsetS δ oδ s = sup δ oδ δ∈ hb : ⟨ (w ∷ container q c w refl .fst ∷ q ∷ c ∷ x ∷ γ) ⊨ intoBody ⟩ hb = DefInRead.defIn-in i0 (sh 5 z) (shN 5 N) (var i8 ∈̇ var i0) (w ∷ container q c w refl .fst ∷ q ∷ c ∷ x ∷ γ) tg w refl
四つの有界な対象は、実際の充足関係表、符号集合、環境の塔、そして Lset (sucV δ) です。供給の仮定はそれぞれが Zv に属することを証明し、最初の三つは反射律によって記述が要求する構造と一致します。最後に Lset-suc δ が四つ目を 𝒟ₒ (Lset δ) と同一視するので、もとの x の所属を論理式の本体へ移せます。
(SatGraph.pairs w) (AllCodes w) (Tower.tower w) (LsetS (sucV δ) (suc-ord oδ)) (s .fst) (s .snd .fst) (s .snd .snd .fst) (s .snd .snd .snd) refl refl refl (Lset-suc δ) (subst (λ u → ⟨ fst x ∈ u ⟩) (sym (Lset-suc δ)) xD)
over の連言を示すため、c ∈ Bv、表の要素 q、そして q を対 (c,w) として提示する仕方を固定します。すると正しさにより w は Lset c と同一視されます。残る目標は y について一様です。すべての y ∈ 𝒟ₒ w が候補の値 Vv に属さなければなりません。これは候補の値を Bv における段階と同一視するために必要な第二の包含です。
over : ⟨ γ ⊨ overAt v b f z N ⟩ over c c∈ q q∈ = sndAll-in i0 i1 overBody (q ∷ c ∷ γ) (λ w s s∈ w∈ e → let wq : fst w ≡ Lset (fst c) wq = vals c w c∈ (subst (λ u → ⟨ u ∈ Fv ⟩) e q∈) oc : IsOrd (fst c)
c の順序数性は界から受け継がれ、段階は台の要素として提示され、供給の関数が c で四つの証人を作ります。
oc = mem-ord {A = Bv} ob (fst c) c∈ W : S W = LsetS (fst c) oc s' = sup (fst c) oc c∈ in DefInRead.defIn-in i0 (sh 4 z) (shN 4 N) (∀̇∈ (var i0) (var i0 ∈̇ var (sh 9 v)))
c における供給は、実際の充足関係表、符号集合、環境の塔、後継段階をすべて Zv の中に有界化するので、defIn-in は定義可能冪集合の記述を示せます。y がそこで記述された集合に属するとき、Lset-suc c によりこれは y ∈ 𝒟ₒ (Lset c) となり、さらに c ∈ Bv と Lset-in によって y ∈ Lset Bv が得られます。最後に Vv ≡ Lset Bv に沿って移せば、候補の値への所属が従います。
(w ∷ s ∷ q ∷ c ∷ γ) tg W wq (SatGraph.pairs W) (AllCodes W) (Tower.tower W) (LsetS (sucV (fst c)) (suc-ord oc)) (s' .fst) (s' .snd .fst) (s' .snd .snd .fst) (s' .snd .snd .snd) refl refl refl (Lset-suc (fst c)) (λ y y∈d → subst (λ u → ⟨ fst y ∈ u ⟩) (sym vq) (Lset-in Bv (fst c) (fst y) c∈ (subst (λ u → ⟨ fst y ∈ u ⟩) (Lset-suc (fst c)) y∈d))))
近似の読み手は、表・界・証人の界・タグの対応・環境をパラメータとします。三つの基礎の集合が一度だけ名づけられます。
module ApproxRead {m : ℕ} (f b z : Fin m) (N : Fin 10 → Fin m) (γ : S ^ m) (tg : Tags γ N) where private Fv = fst (lookup f γ) Bv = fst (lookup b γ) Zv = fst (lookup z γ)
ステップの本体は、四つずらした枠でのステップの条項です。
stepBody : Formula S (4 + m)
stepBody = stepAt i0 i1 (sh 4 f) (sh 4 z) (shN 4 N)
近似の条項の外向きの読み出しは、界での表の正しさと完備さを作ります。述語 P は、それぞれの入力について証明すべきことを記録します。記録された値がその入力での段階であること。結果が正確に Values と Entries であることに注意してください。表が対でない要素や、界の外を第一成分とする項目を含まないとは述べていません。
approx-out : ⟨ γ ⊨ approxAt f b z N ⟩ → IsOrd Bv → Values (lookup f γ) Bv × Entries (lookup f γ) Bv approx-out (hd , hs) ob = vals , ents where P : V ℓ → Type (ℓ-suc ℓ) P c = ⟨ c ∈ Bv ⟩ → (w : S) → ⟨ pr c (fst w) ∈ Fv ⟩ → fst w ≡ Lset c
被覆の節は、各 c ∈ Bv に対して、第一成分が c である対を提示する表の要素が命題的に切り詰められた意味で存在すると述べます。その対を読むと値 w が現れ、もとの所属の証明は正準な記法 pr c w へ移されます。結果は命題的に切り詰められたままなので、entryOf は後の命題的推論に存在を与えますが、値を大域的に選ぶことはありません。
entryOf : (c : S) → ⟨ fst c ∈ Bv ⟩ → ∥ Σ[ w ∈ S ] ⟨ pr (fst c) (fst w) ∈ Fv ⟩ ∥₁
entryOf c c∈ = PT.rec squash₁
(λ { (q , (q∈ , h)) → PT.map (λ { (w , s , (e , _)) → w , subst (λ u → ⟨ u ∈ Fv ⟩) e q∈ })
(sndEx-out i0 i1 ⊤̇ (q ∷ c ∷ γ) h) })
(hd c c∈)
帰納段階では、c ∈ Bv を満たす任意の記録された対 (c,w) を検証します。その所属の証明から近似の第二の節が stepAt w c を与え、帰納の仮定が c より下の各入力での正しさを与えます。さらに被覆の節がそこで対応する正準な項目を与えます。したがって StepRead.step-out は、記録された値がちょうど Lset c であると結論できます。
step : (c : V ℓ) → ((y : V ℓ) → ⟨ y ∈ c ⟩ → P y) → P c
step c IH c∈ w rec =
StepRead.step-out i0 i1 (sh 4 f) (sh 4 z) (shN 4 N) env tg
(useBoth i0 (q ∷ γ) cS w refl stepBody (hs q rec)) vals' ents'
where
ここで関係する集合を構成可能な台の中に提示します。所属 c ∈ Bv から台の要素 cS が得られ、pr c (fst w) が表に属するという仮定から q が得られます。値 w はすでに帰納述語へ渡された台の要素です。次の環境は、この三つの提示をステップの論理式が要求する枠に置きます。
cS : S cS = down (lookup b γ) c c∈ q : S q = down (lookup f γ) (pr c (fst w)) rec env : S ^ (4 + m)
拡張された環境は、ステップの読み出しのための四つの枠を組み立てます。界の順序数性がより小さい入力を界の下に制限し、より小さい入力での正しさの読み出しは、帰納の仮定の制限です。
env = w ∷ cS ∷ container q cS w refl .fst ∷ q ∷ γ in' : (y : S) → ⟨ fst y ∈ c ⟩ → ⟨ fst y ∈ Bv ⟩ in' y y∈ = ob .fst {x = c} {y = fst y} y∈ c∈ vals' : Values (lookup f γ) c vals' y w' y∈ rec' = IH (fst y) y∈ (in' y y∈) w' rec'
より小さい入力での完備さも同じ制限で復元されます。より小さい入力ごとに、切り詰められた項目が消費され、帰納の仮定の値の等式が、正準な項目を所定の位置へ運びます。
ents' : Entries (lookup f γ) c ents' y y∈ = PT.rec (snd (pr (fst y) (Lset (fst y)) ∈ Fv)) (λ { (w' , rec') → subst (λ u → ⟨ pr (fst y) u ∈ Fv ⟩) (IH (fst y) y∈ (in' y y∈) w' rec') rec' }) (entryOf y (in' y y∈))
Bv より下での正しさは、基礎にある入力 c に対する周囲の所属帰納によって得られます。述語 P c は c ∈ Bv を条件とします。この所属は定理を必要な界に制限すると同時に、Bv の順序数性を通じて、より小さい各入力に帰納の仮定を適用できるようにします。帰納の結論を任意の記録された値に適用すると Values が得られます。
vals : Values (lookup f γ) Bv vals c w c∈ rec = ∈-induction {P = P} step (fst c) c∈ w rec
界での完備さは、切り詰められた項目と、今証明した正しさを合成します。値の等式が、記録された項目を正準な項目へ運びます。
ents : Entries (lookup f γ) Bv ents c c∈ = PT.rec (snd (pr (fst c) (Lset (fst c)) ∈ Fv)) (λ { (w , rec) → subst (λ u → ⟨ pr (fst c) u ∈ Fv ⟩) (vals c w c∈ rec) rec }) (entryOf c c∈)
近似の条項の内向きの方向は、より強い意味論的な仮定からはじまります。表が界で階層を実現することです。この非対称は意図的なものです。外向きの方向が証明するのは二つの表の条件だけで、内向きの方向が消費するのは、階層の完全な仕様です。
approx-in : (ob : IsOrd Bv) → IsHier Bv (lookup f γ) → ((c : V ℓ) (oc : IsOrd c) → ⟨ c ∈ Bv ⟩ → Supply Zv c oc) → ⟨ γ ⊨ approxAt f b z N ⟩ approx-in ob sp sup = dom , steps where
階層の仕様の外向きの読み出しは、記録されたそれぞれの対について、入力が界の下にあり、値がそこの段階に等しいと言います。
hout : (c w : S) → ⟨ pr (fst c) (fst w) ∈ Fv ⟩ → ⟨ fst c ∈ Bv ⟩ × (fst w ≡ Lset (fst c)) hout = hier-out Bv ob (lookup f γ) sp
内向きの読み出しは、界の下のすべての正準な対が記録されていると言います。
hin : (c : S) → ⟨ fst c ∈ Bv ⟩ → ⟨ pr (fst c) (Lset (fst c)) ∈ Fv ⟩ hin = hier-in Bv ob (lookup f γ) sp
定義域の連言項は、界の下のそれぞれの入力で段階を提示し、正準な対を表の中へ注入することで証明されます。
dom : ⟨ γ ⊨ ∀̇∈ (var b) (∃̇∈ (var (sh 1 f)) (sndEx i0 i1 ⊤̇)) ⟩ dom c c∈ = ∣ q , ( hin c c∈ , fillSnd i0 (q ∷ c ∷ γ) c w refl ⊤̇ (λ z → z) i1 refl ) ∣₁ where w : S w = LsetS (fst c) (mem-ord {A = Bv} ob (fst c) c∈)
正準な対は、所属の証明を下降して台の要素として提示されます。
q : S q = down (lookup f γ) (pr (fst c) (Lset (fst c))) (hin c c∈)
近似の第二の連言は、表の各要素 q と、q を対 (c,w) として提示する各方法について示す必要があります。そのような提示のもとでは、階層の厳密な仕様から c ∈ Bv と w ≡ Lset c の両方が得られ、c におけるステップの論理式を証明する準備が整います。ここでは、候補の表の任意の要素がそのような対の提示をもつとは主張していません。
steps : ⟨ γ ⊨ ∀̇∈ (var f) (bothAll i0 stepBody) ⟩ steps q q∈ = bothAll-in i0 stepBody (q ∷ γ) (λ c w s s∈ c∈s w∈s e → let rec : ⟨ pr (fst c) (fst w) ∈ Fv ⟩ rec = subst (λ u → ⟨ u ∈ Fv ⟩) e q∈ c∈ : ⟨ fst c ∈ Bv ⟩
入力は、階層の外向きの読み出しによって界の下にあり、順序数性は受け継がれます。そして StepRead.step-in が、制限された正しさと完備さと、より小さい入力ごとの供給を含む、五つの仮定をすべて受け取ります。
c∈ = hout c w rec .fst oc : IsOrd (fst c) oc = mem-ord {A = Bv} ob (fst c) c∈ in StepRead.step-in i0 i1 (sh 4 f) (sh 4 z) (shN 4 N) (w ∷ c ∷ s ∷ q ∷ γ) tg oc (hout c w rec .snd) (λ d w' d∈ rec' → hout d w' rec' .snd)
現在の入力 c より下での完全性は hier-in から得られます。順序数である界の推移性が d ∈ c ∈ Bv を d ∈ Bv に変え、そこで正準な項目の存在が分かります。補助的な界は別の根拠から来ます。与えられた供給関数 sup を同じ推移性に沿って制限したものです。したがって、階層の仕様が表の項目を与え、sup が四つの有界な符号化対象を与えます。
(λ d d∈ → hin d (ob .fst {x = fst c} {y = fst d} d∈ c∈)) (λ d od d∈ → sup d od (ob .fst {x = fst c} {y = d} d∈ c∈)))
階層の読みには四つの特別な枠があります。候補の段階 a、その段階の添字 p、近似表 f、そして共通の証人の界 z です。タグの写像は符号化の論理式が使う十個の数項の位置を解釈し、環境はこれらすべての枠に台の要素を与えます。
module HierRead {m : ℕ} (a p f z : Fin m) (N : Fin 10 → Fin m) (γ : S ^ m) (tg : Tags γ N) where private Av = fst (lookup a γ) Pv = fst (lookup p γ) Zv = fst (lookup z γ)
階層の論理式の健全性の定理はこう言います。論理式が成立し、順序数の枠が順序数であれば、層の枠は順序数の枠での段階に等しい、と。証明は、近似と最後のステップを別々に読みます。
hier-sound : ⟨ γ ⊨ hierAt a p f z N ⟩ → IsOrd Pv → Av ≡ Lset Pv hier-sound (ha , hs) op = StepRead.step-out a p f z N γ tg hs (ve .fst) (ve .snd) where ve = ApproxRead.approx-out f p z N γ tg ha op
階層の論理式の完備性の定理は、添字の枠の順序数性、層の枠と段階の同定、添字での実際の階層の表、そして供給の関数を受け取り、充足を作ります。
hier-complete : (op : IsOrd Pv) → Av ≡ Lset Pv → IsHier Pv (lookup f γ) → ((c : V ℓ) (oc : IsOrd c) → ⟨ c ∈ Pv ⟩ → Supply Zv c oc) → ⟨ γ ⊨ hierAt a p f z N ⟩ hier-complete op aq sp sup = ApproxRead.approx-in f p z N γ tg op sp sup
証明は、階層の仕様からの内向きの近似と、最後のステップを合成します。後者の正しさと完備さの条項は、より小さい入力ごとに、階層の仕様から外向きに読まれます。
, StepRead.step-in a p f z N γ tg op aq (λ c w c∈ rec → hier-out Pv op (lookup f γ) sp c w rec .snd) (hier-in Pv op (lookup f γ) sp) sup
近似と完成した階層を読む
内部のモジュールは、対象言語の中で構成可能階層を最終的に表す論理式を封印します。
module Inner where
十四枠の環境は十個の数項タグから始まります。weakenFin を繰り返すと、各添字は数値上の位置を変えずに Fin 14 へ埋め込まれるので、N14 は零番から九番までの枠を占めます。これは、先頭の十項がフォン・ノイマン数項である、後に用いる具体的な環境と一致します。
N14 : Fin 10 → Fin 14 N14 k = weakenFin (weakenFin (weakenFin (weakenFin k)))
末尾の四つの枠が内側の論理式の数学的データを完成させます。十番の枠は表 ff、十一番は候補の段階 aa、十二番はその段階の添字 pp、十三番は共通の界 zz を保持します。したがって環境全体の順序は、十個のタグに続いて f、a、p、z となります。
ff aa pp zz : Fin 14 ff = sh 10 (i0 {3}) aa = sh 11 (i0 {2}) pp = sh 12 (i0 {1}) zz = sh 13 (i0 {0})
内側の論理式は二つの数学的要件を連言します。pins N14 は最初の十枠を符号化の記述に必要な数項タグとして固定し、hierAt aa pp ff zz N14 は ff が pp より下の階層を近似し、aa が pp におけるその次の値であり、補助データがすべて zz で有界化されることを述べます。不透明性により、この大きな論理式は証明済みの読み補題の背後に保たれます。
opaque inner : Formula S 14 inner = pins N14 ∧̇ hierAt aa pp ff zz N14
有界性を証明するため、検査器はこの局所的な範囲で inner と、封印された記述 satAt、defAt を展開できます。この限定された展開により、大きな連言が原子論理式、結合子、有界量化子だけから作られていることが分かります。この証明境界の外では、展開された論理式を正規化するのではなく、読み補題によって数学的内容を取り出します。
opaque unfolding inner satAt defAt
局所的な展開の後、checkΔ₀ inner tt は構造的な Δ₀ の証人を与えます。inner に現れる量化子はすべて有界です。これはこの特定の論理式に対する構文的な検証であり、checkΔ₀ が有界性を双方向に決定するという主張ではありません。外側のモジュールとそこから公開される結果は、引き続き lem : LEM (ℓ-suc ℓ) をパラメータとします。
Δ₀-inner : Δ₀ inner Δ₀-inner = checkΔ₀ inner tt
封印された論理式の読み出しも、同じ展開の境界を通して公開されます。
opaque unfolding inner
連言の外向きの読み出しは、その二つの連言項の対です。連言とは命題の対だからです。
inner-out : (γ : S ^ 14) → ⟨ γ ⊨ inner ⟩ → ⟨ γ ⊨ pins N14 ⟩ × ⟨ γ ⊨ hierAt aa pp ff zz N14 ⟩ inner-out γ h = h
逆に、pin の節と階層の節の証明は、それらの連言を満たすために必要な二つの成分をなします。inner-out と合わせると、後で必要となる正確な二方向が得られます。大きな論理式から二つの数学的部分を取り出すことも、両方を証明した後で論理式を再構成することもできます。
inner-in : (γ : S ^ 14) → ⟨ γ ⊨ pins N14 ⟩ → ⟨ γ ⊨ hierAt aa pp ff zz N14 ⟩ → ⟨ γ ⊨ inner ⟩ inner-in γ h1 h2 = h1 , h2
suc n 個の位置をもつ外側の環境に対して、lastFin はその最後の位置を表します。以下の各適用では、その位置に新しい存在量化子の界となる共通の集合が置かれています。有界量化子が導入する証人は本体の新しい先頭位置を占め、lastFin が指す位置ではありません。
lastFin : {n : ℕ} → Fin (suc n) lastFin {zero} = zero lastFin {suc n} = suc (lastFin {n})
演算 wrap は、本体の先頭にある証人の位置を存在量化し、その証人が外側の最後の位置で名づけられた集合に属することを要求します。そのため、有界性を保ったまま項数が一つ減ります。この演算を繰り返すことで、十個の数項タグと表がそれぞれ量化され、いずれも共通の界 z の要素であることが要求されます。
wrap : {n : ℕ} → Formula S (suc (suc n)) → Formula S (suc n) wrap {n} φ = ∃̇∈ (var (lastFin {n})) φ
Δ₀ の証人は、包む操作の下でも保たれます。有界の存在量化は、それ自体が有界の構成だからです。
δ-wrap : {n : ℕ} {φ : Formula S (suc (suc n))} → Δ₀ φ → Δ₀ (wrap {n} φ) δ-wrap d = δ-∃∈ d
五回の包む操作が、十の数項の枠のうち五つを消費し、自由な位置を十四から九へと一つずつ減らします。
s13 = wrap {12} inner s12 = wrap {11} s13 s11 = wrap {10} s12 s10 = wrap {9} s11 s9 = wrap {8} s10
さらに五回の包む操作が、自由な位置を九から四へ減らし、層・順序数の添字・表・証人の界だけを残します。
s8 = wrap {7} s9 s7 = wrap {6} s8 s6 = wrap {5} s7 s5 = wrap {4} s6 s4 = wrap {3} s5
十一回目の包みは、再び z を界として、残る補助的な枠である階層の表 f を存在量化します。自由な位置はちょうど三つ、順に (a,p,z)、すなわち候補の段階、その段階の添字、共通の証人の界だけになります。したがって three は三項論理式であって文ではありません。後の消去は使われていない定数領域を取り除きますが、この三つの自由変数は取り除きません。
three : Formula S 3 three = wrap {2} s4
証人の論理式は十一回包まれます。共通の界の内側で導入された有界の存在量化子の一つひとつに対応します。各包みが Δ₀ の証拠の一層を加えるため、包まれた論理式は全体を通して有界のままです。
Δ₀-three : Δ₀ three Δ₀-three = δ-wrap (δ-wrap (δ-wrap (δ-wrap (δ-wrap (δ-wrap (δ-wrap (δ-wrap (δ-wrap (δ-wrap (δ-wrap Δ₀-inner))))))))))
包まれた論理式に定数が含まれないことを確かめるため、この計算では密封された inner、satAt、defAt の定義を参照できます。この局所的な展開が明らかにするのは出現回数の簡約に必要な構文だけであり、周囲の議論では大きな論理式そのものを読み補題と書き補題を通して扱います。
opaque unfolding inner satAt defAt
three における定数の出現回数は零です。残る三つの位置は a、p、z のための自由変数であり、定数ではありません。この計算のために密封された部分を展開すると、論理式のすべての項が変数から作られているため、等式は定義的に簡約されます。
count-three : countFo three ≡ 0 count-three = refl
three は定数を含まないので、消去は定数域を構成可能な台から空の型へ変えつつ、変数と量化子の構造を保ちます。したがって得られる erased は無パラメータですが、アリティは三のままです。これを元の定数域へ埋め込むと three が復元されます。
erased : Formula (⊥* {ℓ-suc ℓ}) 3 erased = Cnt.erase three count-three
消去は Δ₀ の証拠も保ちます。変更されるのは、もともと出現しない定数記号だけです。そのため three の各有界量化子は有界なままであり、同じ構造的な議論によって erased が Δ₀ であることが示されます。
Δ₀-erased : Δ₀ erased Δ₀-erased = erase-Δ₀ three count-three Δ₀-three
意味論的には、一層の包みは命題的に切り詰められた有界の証人です。境界の要素 x が本体を満たすたびに P が得られるなら、unwrap はその切り詰められた存在を P へ除去します。P : hProp という宣言が、この除去に必要な命題性をちょうど与えます。
unwrap : {n : ℕ} (φ : Formula S (suc (suc n))) (γ : S ^ (suc n)) {P : hProp (ℓ-suc ℓ)} → ((x : S) → ⟨ fst x ∈ fst (lookup (lastFin {n}) γ) ⟩ → ⟨ (x ∷ γ) ⊨ φ ⟩ → ⟨ P ⟩) → ⟨ γ ⊨ wrap {n} φ ⟩ → ⟨ P ⟩ unwrap φ γ {P} k h = PT.rec (snd P) (λ { (x , xz , hx) → k x xz hx }) h
wrap-in は、名指された要素とその拡張での本体の充足から、有界の存在量化を組み立てます。有界の存在量化子の導入規則です。
wrap-in : {n : ℕ} (φ : Formula S (suc (suc n))) (γ : S ^ (suc n)) (x : S) → ⟨ fst x ∈ fst (lookup (lastFin {n}) γ) ⟩ → ⟨ (x ∷ γ) ⊨ φ ⟩ → ⟨ γ ⊨ wrap {n} φ ⟩ wrap-in φ γ x m h = ∣ x , (m , h) ∣₁
構成可能な階層を表すパラメータなし論理式
表に現れる論理式 levelFo には、三つの自由な位置 (a,p,z) があります。これは p が順序数であるという主張と、z で有界化された消去後の階層記述との連言です。したがって健全性の結論が a と p だけに言及しても、z は論理式の入力として残ります。
levelFo : Formula (⊥* {ℓ-suc ℓ}) 3 levelFo = isOrd-at-p ∧̇ Inner.erased
levelFo の二つの連言項はいずれも Δ₀ であり、Δ₀ のクラスは連言について閉じています。したがって連言の構成子は、非有界量化子を導入することなく、二つの有界性の証拠を Δ₀-levelFo の証拠へまとめます。
Δ₀-levelFo : Δ₀ levelFo Δ₀-levelFo = δ-∧ Δ₀-isOrd-at-p Inner.Δ₀-erased
読みの補題は、定数のない任意の Δ₀ 論理式に対して三つのパスを合成します。制限された台から周囲の階層への Δ₀ 絶対性、空の定数域の埋め込みによる充足の不変性、そして空の解釈の一意性です。結果は二つの充足の命題の等式です。
read : {n : ℕ} {φ : Formula (⊥* {ℓ-suc ℓ}) n} → Δ₀ φ → (δ : S ^ n) → (δ ⊨ embed φ) ≡ (map fst δ ⊨ₚ φ) read {n} {φ} dφ δ = AbsL.abs₀ (mapΔ₀ Empty.rec* dφ) δ ∙ embed-⊨ 𝒮ᵥ {K = S} fst φ (map fst δ)
このパスの最後の等式が扱うのは定数の解釈です。定数域が空なので、どの解釈も各点で空型の除去から得られる解釈と一致します。関数外延性がそれを正準な空の解釈と同一視し、その結果、直前の埋め込みの比較は同じ無パラメータ論理式の外側での読みへ到達します。
∙ cong (λ ι → SemVᵃ.At._⊨_ (⊥* {ℓ-suc ℓ}) ι (map fst δ) φ) (funExt (λ b → Empty.rec* b))
外向きの順序数の読みは、順序数性の原子の二つの節を、p の基底集合の推移性とその各要素の推移性へと展開します。すべての項目は p の提示を通して降ろされます。
ord-out : (a p z : S) → ⟨ (a ∷ p ∷ z ∷ []) ⊨ embed isOrd-at-p ⟩ → IsOrd (fst p) ord-out a p z h = ( λ {x} {y} y∈x x∈p → h .fst (down p x x∈p) x∈p (down (down p x x∈p) y y∈x) y∈x ) , ( λ x x∈p {y} {u} u∈y y∈x → h .snd (down p x x∈p) x∈p (down (down p x x∈p) y y∈x) y∈x
順序数性の第二の条項では、x ∈ p、y ∈ x、u ∈ y を取ります。この三段の所属を構成可能な台へ降ろすと、論理式の第二の連言項から u ∈ x が得られます。これは p の各要素 x の推移性そのものであり、第一の条項と合わせて IsOrd p が得られます。
(down (down (down p x x∈p) y y∈x) u u∈y) u∈y )
内向きの順序数の読みは、順序数性の証明から二つの節を組み立てます。すべての項目は L の要素としてまとめられます。
ord-in : (a p z : S) → IsOrd (fst p) → ⟨ (a ∷ p ∷ z ∷ []) ⊨ embed isOrd-at-p ⟩ ord-in a p z op = (λ x x∈p y y∈x → op .fst {x = fst x} {y = fst y} y∈x x∈p) , (λ x x∈p y y∈x u u∈y → op .snd (fst x) x∈p {x = fst y} {y = fst u} u∈y y∈x)
健全性の議論はここから、隠された論理式を十四のスロットで読む形に移ります。目的は、有界な補助証人を捨てつつ、その数学的帰結、すなわちスロット a の値がスロット p を添字とする構成可能な段階であることを残すことです。
private module Sound where open Inner
finish 補題は inner の二つの連言項を分けて読みます。pins の読み補題は第一項を、階層の読み補題が必要とする十個の数項の等式へ変えます。第二項の近似から hier-sound が復元するのは Values × Entries だけですが、p の順序数性が与えられれば、それで最後のステップを a = Lset p と読むには十分です。ここでは、隠れた表に不正な形の要素がないことも、p の外を第一成分とする項目がないことも主張していません。
finish : (γ : S ^ 14) → ⟨ γ ⊨ inner ⟩ → IsOrd (fst (lookup pp γ)) → fst (lookup aa γ) ≡ Lset (fst (lookup pp γ)) finish γ h op = HierRead.hier-sound aa pp ff zz N14 γ tg (inner-out γ h .snd) op where tg : Tags γ N14
固定された数項は pins の読みによって外向きに読まれ、対象言語の節から十の数項の等式が導かれます。
tg = PinsRead.pins-out N14 γ (inner-out γ h .fst)
内部の健全性補題は、構成可能な台の三要素 a、p、z から始め、そこで embed levelFo が成り立つと仮定します。まず消去の逆等式を用いて、十一回包まれた論理式の充足を復元します。求める結論は、a の基礎集合と、p の基礎集合を添字とする Lset とを比較するものです。
sound-L : (a p z : S) → ⟨ (a ∷ p ∷ z ∷ []) ⊨ embed levelFo ⟩ → fst a ≡ Lset (fst p) sound-L a p z (ho , hφ) = go (subst (λ ψ → ⟨ (a ∷ p ∷ z ∷ []) ⊨ ψ ⟩) (Cnt.erase-inv three count-three) hφ) where ordp : IsOrd (fst p)
順序数性の連言項は、外向きの順序数の読みを通して p の順序数性の証明を生み出します。これが階層の読みの残りの入力です。
ordp = ord-out a p z ho
最後まで残す等式を命題 G としてまとめます。累積階層の集合は h-集合をなすので、setIsSet によりこの等式型が hProp であることが分かります。したがって、命題的に切り詰められた各有界証人を、特定の証人を外へ取り出すことなく G へ除去できます。
G : hProp (ℓ-suc ℓ) G = (fst a ≡ Lset (fst p)) , setIsSet (fst a) (Lset (fst p))
健全性は十一の有界の存在量化を一つずつ展開し、切り詰められた証人を命題の等式の中で消費します。展開の順序は論理式の束縛の順序を反映します。
go : ⟨ (a ∷ p ∷ z ∷ []) ⊨ three ⟩ → ⟨ G ⟩ go = unwrap s4 (a ∷ p ∷ z ∷ []) {G} λ F mF → unwrap s5 (F ∷ a ∷ p ∷ z ∷ []) {G} λ x9 m9 → unwrap s6 (x9 ∷ F ∷ a ∷ p ∷ z ∷ []) {G} λ x8 m8 →
続く五回の除去で、数項の証人 x7 から x3 までを復元します。各段階で環境は先頭側へ伸びますが、最後のスロットは常に z のままです。十一個の証人はすべてこの共通の境界から得られます。
unwrap s7 (x8 ∷ x9 ∷ F ∷ a ∷ p ∷ z ∷ []) {G} λ x7 m7 → unwrap s8 (x7 ∷ x8 ∷ x9 ∷ F ∷ a ∷ p ∷ z ∷ []) {G} λ x6 m6 → unwrap s9 (x6 ∷ x7 ∷ x8 ∷ x9 ∷ F ∷ a ∷ p ∷ z ∷ []) {G} λ x5 m5 → unwrap s10 (x5 ∷ x6 ∷ x7 ∷ x8 ∷ x9 ∷ F ∷ a ∷ p ∷ z ∷ []) {G} λ x4 m4 → unwrap s11 (x4 ∷ x5 ∷ x6 ∷ x7 ∷ x8 ∷ x9 ∷ F ∷ a ∷ p ∷ z ∷ []) {G} λ x3 m3 →
最も内側の証人が展開を完成させます。十四スロットの環境と順序数性の証明が finish の補題に渡され、二つの基底集合の等式が生まれます。
unwrap s12 (x3 ∷ x4 ∷ x5 ∷ x6 ∷ x7 ∷ x8 ∷ x9 ∷ F ∷ a ∷ p ∷ z ∷ []) {G} λ x2 m2 → unwrap s13 (x2 ∷ x3 ∷ x4 ∷ x5 ∷ x6 ∷ x7 ∷ x8 ∷ x9 ∷ F ∷ a ∷ p ∷ z ∷ []) {G} λ x1 m1 → unwrap inner (x1 ∷ x2 ∷ x3 ∷ x4 ∷ x5 ∷ x6 ∷ x7 ∷ x8 ∷ x9 ∷ F ∷ a ∷ p ∷ z ∷ []) {G} λ x0 m0 hm → finish (x0 ∷ x1 ∷ x2 ∷ x3 ∷ x4 ∷ x5 ∷ x6 ∷ x7 ∷ x8 ∷ x9 ∷ F ∷ a ∷ p ∷ z ∷ []) hm ordp
周囲の集合 a、p、z が構成可能であるとき、それぞれの構成可能性の証拠によって、これらを構成可能な台の要素として提示できます。Δ₀ 絶対性を逆向きに読むと、levelFo の周囲での充足がそれらの提示による充足へ移り、内部の健全性の議論を適用できます。基礎集合へ戻せば a = Lset p が得られます。したがって、三つの入力がすべて構成可能であることは明示的な仮定であり、論理式から導かれる結論ではありません。
level-sound : (a p z : V ℓ) → ⟨ isL a ⟩ → ⟨ isL p ⟩ → ⟨ isL z ⟩ → ⟨ (a ∷ p ∷ z ∷ []) ⊨ₚ levelFo ⟩ → a ≡ Lset p level-sound a p z la lp lz h = Sound.sound-L (a , la) (p , lp) (z , lz) (subst ⟨_⟩ (sym (read Δ₀-levelFo ((a , la) ∷ (p , lp) ∷ (z , lz) ∷ []))) h)
完全性のため、妥当性のデータをもつ lam と順序数 p ∈ lam を固定します。順序数性のフィールドにより lam は段階の添字となり、対応する段階は Lset lam です。残るフィールドは後者閉包、ω の所属、および lam の下で必要となる符号化の証人を与えます。これらを用いて、特定の境界 Lset lam が段階 Lset p の記述に必要なすべての証人を含むことを示します。
private module Complete (lam : V ℓ) (ad : Adequate lam) (p : V ℓ) (op : IsOrd p) (p∈λ : ⟨ p ∈ lam ⟩) where open Inner open Adequate lam ad using ( ord; succ; ω∈; wit )
十分な段階 lam の推移性は、その順序数性から取り出されます。入れ子になった二つの所属が一つに合成されます。
private tr : (x y : V ℓ) → ⟨ x ∈ lam ⟩ → ⟨ y ∈ x ⟩ → ⟨ y ∈ lam ⟩ tr x y x∈ y∈ = ord .fst {x = x} {y = y} y∈ x∈
空集合は十分な段階に属します。∅ ∈ ω ∈ lam の連鎖に推移性を適用した結果です。
∅∈λ : ⟨ ∅ ∈ lam ⟩ ∅∈λ = tr ω ∅ ω∈ (#∈ω zero)
数項の有界性の議論を、lam における構成可能階層へ特殊化します。順序数性、後者閉包、∅ ∈ lam から、各模型数項の基礎集合が Lset lam に属することが従います。これが、後で十個のタグ数項すべてに必要となる共通の境界を与えます。
module B = Bound lam ord succ ∅∈λ using ( num∈λ )
K = Lset lam と置きます。これは第三の自由入力 zS が表す共通の境界集合です。階層表、十個の数項、そして各行を正当化するすべての補助集合が K に属することを示す必要があります。
K : V ℓ K = Lset lam
c ∈ lam なら、後者閉包から sucV c ∈ lam が得られます。後者段階についての標準的な事実により Lset c ∈ Lset (sucV c) となり、さらに sucV c ∈ lam に沿う単調性によって、この所属を Lset c ∈ K へ持ち上げられます。後では同じ補題を sucV c に適用し、後者閉包をもう一度用いて Lset (sucV c) ∈ K を得ます。これが c の行に必要な定義可能冪集合の証人です。
Lset∈K : (c : V ℓ) → ⟨ c ∈ lam ⟩ → ⟨ Lset c ∈ K ⟩ Lset∈K c c∈ = Lset-mono {α = lam} {β = sucV c} (succ c c∈) (Lset∈suc c)
数項の有界性定理は、まず模型の数項の基礎集合を K に入れます。射影等式 numeralL-fst がその集合を周囲のフォン・ノイマン数項 # k と同一視し、それに沿う輸送から # k ∈ K が得られます。したがって十個の数項の証人は、階層表と同じ境界を満たします。
num∈K : (k : ℕ) → ⟨ # k ∈ K ⟩ num∈K k = subst (λ u → ⟨ u ∈ K ⟩) (numeralL-fst k) (B.num∈λ k)
四つの集合に名前が与えられます。段階 Lset p、順序数 p、段階 Lset lam、そして p における階層の表で、それぞれ適切な台の中にあります。
aS pS zS F : S aS = LsetS p op pS = p , At.cL p op zS = LsetS lam ord F = At.hier p op
環境 E はここで、十四のスロットへの完全な割り当てを記録します。先頭から順に、数項 0 から 9、p における実際の階層表、意図した値 Lset p、添字 p、そして共通の境界 Lset lam が並びます。これは inner がデータを読むスロットの順序とちょうど一致します。
E : S ^ 14
E = nn 0 ∷ nn 1 ∷ nn 2 ∷ nn 3 ∷ nn 4 ∷ nn 5 ∷ nn 6 ∷ nn 7 ∷ nn 8 ∷ nn 9
∷ F ∷ aS ∷ pS ∷ zS ∷ []
タグの仮定は、最初の四つのタグのスロットを、それぞれみずからの数項と定義的に同一視します。
tg : Tags E N14 tg zero = refl tg (suc zero) = refl tg (suc (suc zero)) = refl tg (suc (suc (suc zero))) = refl
続く五つの場合は、添字 4 から 8 までのタグのスロットを検証します。各参照は E の対応する項目へ簡約されるので、これらのスロットは定義上それぞれ数項 4 から 8 です。
tg (suc (suc (suc (suc zero)))) = refl tg (suc (suc (suc (suc (suc zero))))) = refl tg (suc (suc (suc (suc (suc (suc zero)))))) = refl tg (suc (suc (suc (suc (suc (suc (suc zero))))))) = refl tg (suc (suc (suc (suc (suc (suc (suc (suc zero)))))))) = refl
最後の場合は、添字 9 にある十番目のタグのスロットが数項 9 であることを確かめます。これで Tags E N14 が要求する十個の等式が、明示された環境上の計算によってすべて得られました。
tg (suc (suc (suc (suc (suc (suc (suc (suc (suc zero))))))))) = refl
順序数 p の各要素 c に対して、供給の補題は四つの対象、すなわち充足のグラフ、コードの集合、環境の塔、次の段階 Lset (sucV c) を K に入れます。連鎖 c ∈ p ∈ lam と lam の推移性によって、まず c が lam に属することが分かり、妥当性の証人を使えるようになります。
sup : (c : V ℓ) (oc : IsOrd c) → ⟨ c ∈ p ⟩ → Supply K c oc sup c oc c∈ = w .snd .snd .fst , ( w .snd .fst , ( w .snd .snd .snd , Lset∈K (sucV c) (succ c c∈λ) )) where c∈λ : ⟨ c ∈ lam ⟩ c∈λ = tr p c p∈λ c∈
それぞれの c の証人は妥当性のデータから読まれ、順序数のすべての要素のための供給が閉じられます。
w = wit c c∈λ oc
内側の論理式はここで E において成り立ちます。pins の書き補題が数項の連言項を与えます。階層の連言項については、hier-complete が p の順序数性、候補となる値と Lset p の反射的な同一視、hierL-spec が与える正確な階層表、そして妥当性から上で各行について導いた供給を用います。ここでは強化された段階仮定を使いません。
hm : ⟨ E ⊨ inner ⟩ hm = inner-in E (PinsRead.pins-in N14 E tg) (HierRead.hier-complete aa pp ff zz N14 E tg op refl (hierL-spec p (At.cL p op) op) sup)
p における妥当性の証人は、実際の階層表 F の基礎集合を共通の境界集合 K に入れます。これにより、F を最も外側の有界な証人として導入するために必要な所属の証拠が得られます。
FK : ⟨ fst F ∈ K ⟩ FK = wit p p∈λ op .fst
残る仕事は、階層表と数項のデータを十一個の有界存在量化子の内側へ隠すことです。最も外側の導入には実際の階層表 F を用い、その K への所属は直前に示しました。続く二回の導入には数項 9 と 8 を用い、それぞれが同じ共通の境界に属するという証拠を添えます。
h3 : ⟨ (aS ∷ pS ∷ zS ∷ []) ⊨ three ⟩ h3 = wrap-in s4 (aS ∷ pS ∷ zS ∷ []) F FK ( wrap-in s5 (F ∷ aS ∷ pS ∷ zS ∷ []) (nn 9) (num∈K 9) ( wrap-in s6 (nn 9 ∷ F ∷ aS ∷ pS ∷ zS ∷ []) (nn 8) (num∈K 8) (
同じ導入規則によって数項 7 から 3 までを挿入します。それらの所属証明はすべて num∈K から得られるので、各量化子の証人は K = Lset lam の内部にあります。周囲で非有界な探索を行って証人を得ているわけではありません。
wrap-in s7 (nn 8 ∷ nn 9 ∷ F ∷ aS ∷ pS ∷ zS ∷ []) (nn 7) (num∈K 7) ( wrap-in s8 (nn 7 ∷ nn 8 ∷ nn 9 ∷ F ∷ aS ∷ pS ∷ zS ∷ []) (nn 6) (num∈K 6) ( wrap-in s9 (nn 6 ∷ nn 7 ∷ nn 8 ∷ nn 9 ∷ F ∷ aS ∷ pS ∷ zS ∷ []) (nn 5) (num∈K 5) ( wrap-in s10 (nn 5 ∷ nn 6 ∷ nn 7 ∷ nn 8 ∷ nn 9 ∷ F ∷ aS ∷ pS ∷ zS ∷ []) (nn 4) (num∈K 4) ( wrap-in s11 (nn 4 ∷ nn 5 ∷ nn 6 ∷ nn 7 ∷ nn 8 ∷ nn 9 ∷ F ∷ aS ∷ pS ∷ zS ∷ []) (nn 3) (num∈K 3) (
最後に数項 2、1、0 を挿入します。最後の導入後に得られる拡張環境はちょうど E であり、そこで hm がすでに inner を証明しています。したがって、入れ子になった導入によって、十一回包まれた論理式が表に残る三つ組 (Lset p,p,Lset lam) で満たされることが示されます。
wrap-in s12 (nn 3 ∷ nn 4 ∷ nn 5 ∷ nn 6 ∷ nn 7 ∷ nn 8 ∷ nn 9 ∷ F ∷ aS ∷ pS ∷ zS ∷ []) (nn 2) (num∈K 2) ( wrap-in s13 (nn 2 ∷ nn 3 ∷ nn 4 ∷ nn 5 ∷ nn 6 ∷ nn 7 ∷ nn 8 ∷ nn 9 ∷ F ∷ aS ∷ pS ∷ zS ∷ []) (nn 1) (num∈K 1) ( wrap-in inner (nn 1 ∷ nn 2 ∷ nn 3 ∷ nn 4 ∷ nn 5 ∷ nn 6 ∷ nn 7 ∷ nn 8 ∷ nn 9 ∷ F ∷ aS ∷ pS ∷ zS ∷ []) (nn 0) (num∈K 0) hm))))))))))
消去の逆等式は、erased を構成可能な定数域へ埋め込むと three が復元されることを述べます。したがって、その等式の逆向きに h3 を輸送すれば、同じ三スロットの環境における embed erased の充足が得られます。変わるのは定数域だけであり、十一個の有界証人とその共通の境界は、すでに構成したもののままです。
hφ : ⟨ (aS ∷ pS ∷ zS ∷ []) ⊨ embed erased ⟩ hφ = subst (λ ψ → ⟨ (aS ∷ pS ∷ zS ∷ []) ⊨ ψ ⟩) (sym (Cnt.erase-inv three count-three)) h3
完全性は二つの連言項から組み立てられます。順序数性の原子は ord-in によって成り立ち、消去後の証人の論理式は証明されたばかりの輸送によって成り立ちます。読みの補題が両方を周囲の充足の中へ移します。
complete : ⟨ (Lset p ∷ p ∷ Lset lam ∷ []) ⊨ₚ levelFo ⟩ complete = subst ⟨_⟩ (read Δ₀-levelFo (aS ∷ pS ∷ zS ∷ [])) (ord-in aS pS zS op , hφ)
完全性定理は、ここで得られる存在方向を正確に述べます。γ が十分で順序数 p を含むなら、三つ組 (Lset p,p,Lset γ) は levelFo を満たします。後の CondensationTransfer では、この Δ₀ の核の外側に非有界存在量化子を加え、三つの座標すべてを初等性によって移し、健全性を用いて移された第一座標を対応する構成可能な段階として認識します。この定理は、任意の第三座標が使えるとも、第三座標が論理式によって一意に定まるとも主張しません。
level-complete : (γ : V ℓ) → Adequate γ → (p : V ℓ) → IsOrd p → ⟨ p ∈ γ ⟩ → ⟨ (Lset p ∷ p ∷ Lset γ ∷ []) ⊨ₚ levelFo ⟩ level-complete γ ad p op p∈ = Complete.complete γ ad p op p∈