部分符号で閉じた領域上で再帰を固定する

階層の符号からなる添字集合を固定し、認識された各構成子の形が要求する直下の論理式部分符号について閉じていると仮定します。さらに、台のスロット、タグの各スロット、環境の塔が標準的な意味をもち、表が完全な表仕様を満たすと仮定します。すると本章の前半は局所的な一意性を示します。既知の論理式のキーがその添字集合に属し、そのキーで表項目が与えられていれば、その項目の基礎集合は再帰的に定義された充足関係集合に等しくなります。後半は閉性を用いず、台、タグ、環境の塔、値の一致、復号、全域性、領域について明示された仮定から表の各節を組み立てます。どちらの向きも、大域的に選ばれた充足関係関数を与えるものではありません。

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

議論は、明示的に与えた排中律の実例に相対して進みます。古典論理は、導入済みの充足関係集合、環境集合、表の構成を支えますが、命題的切り詰めを取り除くわけではありません。復号された論理式や子論理式の表の値は、存在だけが分かる場合があります。

open import Base.Prelude
open import Base.Classical using ( LEM )

モジュールは宇宙レベルを固定し、古典的な仮定に名前を与えます。以下の各定理は、どのレベルの排中律の実例を消費するかを正確に記録します。

module L.Coding.PinnedRecursion {ℓ : Level} (lem : LEM (ℓ-suc ℓ)) where

構造再帰は論理式文法の十個の構成子、すなわち所属と等号の原子論理式、連言、選言、含意、偽、二つの非有界量化子、∀[]-syntax、∃[]-syntax に沿って進みます。定数の付け替えにより、同じ構文木をまず台の要素からなるアルファベット上で読み、次に構成可能な台の上で読むことができ、構成子の形は変わりません。

open import FOL.ZFStructure using ( module hPropStructure )
open import FOL.Syntax using
  ( Formula; Term; var; _∈̇_; _≐_; _∧̇_; _∨̇_; _⇒̇_; ⊥̇; ∃̇∈; ∀̇∈; ∃̇_; ∀̇_ )
import FOL.Absoluteness
open import FOL.Manipulation.ConstantMapping using ( mapFo; mapFo-comp )

論理式キーは、アリティと構文符号を集合論的な順序対で組み合わせたものです。この構成には、累積階層で直接行うものと、構成可能性の証明を伴って L の内部で行うものがあります。対、数項、論理式符号についての射影定理により、両者の基礎にある階層集合が一致することを示します。

open import V.Hierarchy {ℓ} using ( 𝒮ᵥ )
open import V.Coding {ℓ} using ( pr; pr-inj; #-inj′; module VCode )
open import L.Constructible {ℓ} using ( 𝒮ʟ; isL; isL-trans )
open import L.Axioms.Numerals {ℓ} using ( numeralL; numeralL-fst )
open import L.Coding.Model {ℓ} using ( module LCode; prʟ-fst; codeBridge )

閉性条件は、論理式の充足関係がもつ再帰的依存関係に正確に従います。二項結合子では同じアリティの二つの子論理式が、非有界量化子では後続アリティの本体が必要です。∀[]-syntax と ∃[]-syntax では、後続アリティの論理式本体だけが必要です。後二者がもつ項の符号は節の内部で評価され、閉じた領域への所属を要求されません。

open import L.Coding.Expressions {ℓ} using ( consAtL )
open import L.Coding.Closure {ℓ} using ( closedAt; binShapeAt; unShapeAt; bothSameAt; oneSuccAt; succSndAt; binSameClosed-out; unSuccClosed-out; binSuccClosed-out )
open import L.Coding.EnvironmentSet {ℓ} lem using ( envSet )
open import L.Coding.CodeConstructibility {ℓ} using ( sglʟ; cupʟ; tree; tree-inv )
open import L.Coding.CodeSet {ℓ} lem using ( AllCodes; AllCodes-out; keyS; codeS )

論理式 ψ に対し、Sat は再帰的に定義された、充足する環境の標準的な集合を与えます。一方、充足関係の表は符号化されたキーと値の対を格納します。定理は、そこに与えられた値を Sat ψ と比較します。表の全域性が子論理式の値を与えるのは命題的切り詰めのもとだけなので、その値を等式の証明には使えても、再利用可能な選択関数にはできません。

open import L.Coding.Satisfaction {ℓ} lem using
  ( Sat )
open import L.Coding.SatisfactionBridge {ℓ} lem using ( asConst )
open import L.Coding.SatisfactionTable {ℓ} lem using
  ( keyʟ; slot; satTable; entry-out; inSlot; ent-slot ) renaming ( total to slotTotal )

零から九までのタグが十個の構成子の節を選びます。環境塔は各自然数アリティ n に対し、数項 # n と長さ n の符号化された環境集合との対を記録します。この二種類の座標により、節は構文上の構成子と、その充足関係集合を特徴づけるアリティの両方を認識できます。

open import L.Coding.Quantification {ℓ} using
  ( f0; f1; f2; f3; f4; f5; f6; f7; f8; f9; sh; i0; i1; i2; i3; i4; i7; i8
  ; fstS; sndS; bigAnd-in; bigAnd-out )
open import L.Coding.EnvironmentTower {ℓ} lem using ( nn; towerAt; module TowerRead )
open import L.Coding.CodeDomain {ℓ} using ( Tags )

表の仕様には三つの数学的な部分があります。領域の各キーには何らかの値があり、各表項目は領域に属するキーと値の対であり、十個の構成子はそれぞれの意味論的な節を満たします。節の意味論は最後の部分を外延に関する事実として読みます。候補の値と標準的な再帰値が環境集合上で同じ外延をもてば、外延性により両者の基礎となる階層集合が同一視されます。

open import L.Coding.CodeAlphabet {ℓ} using ( module Alphabet )
open import L.Coding.SatisfactionClauses {ℓ} using ( tmIs; tableAt; module Clause; module Rel )
open import L.Coding.SatisfactionClauseSemantics {ℓ} lem using
  ( extB-out; extB-in; ExtFact; ext-unique; module Frame; module RelRead; module Bridge )
open import Cubical.Data.Nat using ( _+_ )

節の環境は有限ベクトルであり、枠を拡張すると以前の座標はすべてずれます。参照と移送によって、それらの座標を対応させ続けます。命題的切り詰めの内側に隠れた証人を消去する先は命題値の目標に限られます。固定の証明では基礎となる階層集合の等式へ、節を埋める証明では固定された対象言語の節の充足へ消去します。これらの消去から、再利用可能な値、復号結果、枠のデータが取り出されることはありません。

open import Cubical.Data.Vec using ( _∷_; lookup )
open import Cubical.Data.Sigma using ( _×_ )
open import Cubical.Foundations.Prelude using ( subst2 )
import Cubical.Data.Empty as Empty
import Cubical.HITs.PropositionalTruncation as PT

命題的切り詰めは、証人が存在することを保ちつつ、それがどの証人であったかを忘れます。したがって、その消去先は命題値でなければなりません。階層における所属は命題値であり、階層 V は h-集合なので、その二つの集合の等式も命題です。このため、以下で用いる消去の正当な行き先になります。

open PT using ( ∥_∥₁; squash₁ )
open import Cubical.HITs.CumulativeHierarchy.Base using ( V; _∈_; setIsSet )
open import Cubical.HITs.CumulativeHierarchy.Properties using ( ⟪_⟫ )
open import Cubical.HITs.CumulativeHierarchy.Constructions using ( module InfinitySet )
open InfinitySet {ℓ} using ( #_; sucV )

構成子タグは Fin 10 の要素として格納されますが、構文符号では通常の自然数の数項を使います。写像 toℕ は上界の証明を忘れ、符号化された対に現れる数項の自然数を取り出します。元の上界により、現れうるタグは零から九までに限られます。

open import Cubical.Data.FinData using ( toℕ )

L 上の一階構造の台を S と書きます。S の要素は、基礎となる階層集合と、その構成可能性の証明からなります。本章の結論の多くは第一射影だけを比較します。充足関係に必要な数学的内容は、表される集合の等しさだからです。

open hPropStructure 𝒮ʟ using ( S )

対象言語の節は、L が担う一階構造で解釈されます。したがって γ ⊨ φ は、その構造の有限環境 γ が論理式 φ を充足することを意味します。後の橋渡し補題は、この内部的な充足の主張を、外部で定義された集合 SatW ψ への所属と比較します。

module AbsL = FOL.Absoluteness.Single 𝒮ᵥ isL isL-trans using ( _^_; _⊨ᵐ_ )
open AbsL using ( _^_ ) renaming ( _⊨ᵐ_ to _⊨_ )

鍵、タグ、復号された論理式を対応させる

まず、論理式のキーへの二つの経路を比較します。外側の経路は、アルファベットの記号を階層へ埋め込み、周囲の数項と対にします。内側の経路は、定数を構成可能な集合として付け替え、論理式を L の内部で符号化し、内部の数項と対にします。

module _ (A : S) where
  keyBridge : ∀ {n} (ψ : Formula ⟪ fst A ⟫ n)
            → fst (keyS A ψ) ≡ fst (keyʟ (mapFo (asConst A) ψ))
  keyBridge {n} ψ =
      cong (pr (# n))

証明はまず構文符号の成分をそろえます。定数を付け替えてから外部の符号を取ることは、付け替えた論理式の内部符号を射影することと一致します。次にアリティの数項をそろえ、最後に内部の順序対を射影します。得られるパスは二つのキーの第一射影を結ぶものであり、付随する構成可能性の証明が定義的に同じだとは主張しません。

        ( cong (λ χ → VCode.⌜ χ ⌝) (sym (mapFo-comp (asConst A) fst ψ))
        ∙ sym (codeBridge (mapFo (asConst A) ψ)) )
    ∙ cong (λ w → pr w (fst LCode.⌜ mapFo (asConst A) ψ ⌝))
        (sym (numeralL-fst n))
    ∙ sym (prʟ-fst (numeralL n) LCode.⌜ mapFo (asConst A) ψ ⌝)

一致のモジュールは、一つの台 W に対して述べられます。そのアルファベットが、形を照合する項と論理式の構文を供給します。

module Match (W : S) where
  open Alphabet W

MatchN は、タグで索引づけられた形状の記録の族です。タグ 0 と 1 では、アトムの二つの項とその符号化された対を名指し、タグ 2 から 4 では、二項結合子の直接の部分論理式とその符号化された対を名指します。この族は、すでに知られている論理式で索引づけられるので、任意の集合の解析器ではありません。

  MatchN : ∀ {n} → ℕ → Formula Ab n → V ℓ → Type (ℓ-suc ℓ)
  MatchN {n}  ψ r = Σ[ t ∈ Term Ab n ] Σ[ u ∈ Term Ab n ] ((ψ ≡ t ∈̇ u) × (r ≡ pr (ct t) (ct u)))
  MatchN {n}  ψ r = Σ[ t ∈ Term Ab n ] Σ[ u ∈ Term Ab n ] ((ψ ≡ t ≐ u) × (r ≡ pr (ct t) (ct u)))
  MatchN {n}  ψ r = Σ[ a ∈ Formula Ab n ] Σ[ b ∈ Formula Ab n ] ((ψ ≡ a ∧̇ b) × (r ≡ pr (cd a) (cd b)))
  MatchN {n}  ψ r = Σ[ a ∈ Formula Ab n ] Σ[ b ∈ Formula Ab n ] ((ψ ≡ a ∨̇ b) × (r ≡ pr (cd a) (cd b)))

タグ四から八も同じ形の表を続けます。タグ四は含意と二つの論理式符号を、タグ五は数項零をペイロードとする偽を記録します。タグ六と七は二つの非有界量化子の後続アリティの本体を記録し、タグ八は ∀[]-syntax の現在のアリティにおける項符号と後続アリティの本体を記録します。

  MatchN {n}  ψ r = Σ[ a ∈ Formula Ab n ] Σ[ b ∈ Formula Ab n ] ((ψ ≡ a ⇒̇ b) × (r ≡ pr (cd a) (cd b)))
  MatchN  ψ r = (ψ ≡ ⊥̇) × (r ≡ # )
  MatchN {n}  ψ r = Σ[ a ∈ Formula Ab (suc n) ] ((ψ ≡ ∃̇ a) × (r ≡ cd a))
  MatchN {n}  ψ r = Σ[ a ∈ Formula Ab (suc n) ] ((ψ ≡ ∀̇ a) × (r ≡ cd a))
  MatchN {n}  ψ r = Σ[ t ∈ Term Ab n ] Σ[ a ∈ Formula Ab (suc n) ] ((ψ ≡ ∀̇∈ t a) × (r ≡ pr (ct t) (cd a)))

タグ九は ∃[]-syntax に対応するペイロード、すなわち現在のアリティの項符号と後続アリティの論理式符号との対をもちます。この補助族は十以上の自然数タグでは空型です。したがって MatchN が記述するのは正確に十個の構成子形ですが、タグの等式に沿う移送を可能にするため、すべての自然数上で定義されています。

  MatchN {n}  ψ r = Σ[ t ∈ Term Ab n ] Σ[ a ∈ Formula Ab (suc n) ] ((ψ ≡ ∃̇∈ t a) × (r ≡ pr (ct t) (cd a)))
  MatchN (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc _)))))))))) ψ r = Empty.⊥*

輸送の補助は、一致の記録をタグとペイロードの間で変換します。対の単射性が符号化された対の等式をタグとペイロードの成分に分け、数項の単射性がタグの索引を運び、一致の記録がその両方に沿って置き換えられます。

  private
    at : ∀ {n} (ψ : Formula Ab n) (j k : ℕ) (r : V ℓ) → pr (# j) (cd ψ) ≡ pr (# j) (cd ψ)
       → MatchN j ψ r → (r' : V ℓ) → pr (# j) r ≡ pr (# k) r' → MatchN k ψ r'
    at ψ j k r _ mj r' e =
      subst2 (λ i x → MatchN i ψ x) (#-inj′ (pr-inj e .fst)) (pr-inj e .snd) mj

タグの読み手 matchAt は、任意の集合を復号するものではありません。すでに与えられた論理式から始まり、その論理式のコードがタグ付きの対と等しいことを述べ、一致の記録を返します。論理式についての場合分けがその固有のタグを露わにし、輸送の補助がそれを与えられたタグに付け替えます。

  matchAt : ∀ {n} (ψ : Formula Ab n) (k : ℕ) (r : V ℓ) → cd ψ ≡ pr (# k) r → MatchN k ψ r
  matchAt (t ∈̇ u) k r e = at (t ∈̇ u)  k _ refl (t , u , (refl , refl)) r e
  matchAt (t ≐ u) k r e = at (t ≐ u)  k _ refl (t , u , (refl , refl)) r e
  matchAt (a ∧̇ b) k r e = at (a ∧̇ b)  k _ refl (a , b , (refl , refl)) r e
  matchAt (a ∨̇ b) k r e = at (a ∨̇ b)  k _ refl (a , b , (refl , refl)) r e

残りの各式も探索は行いません。各構造の場合で、既知の構成子が標準的なタグとペイロードを直接与えます。含意は二つの子論理式符号を、偽は零を、二つの非有界量化子はそれぞれ本体の符号を、∀[]-syntax は項と本体の符号を与えます。その後、同じ移送補助が、これらの標準的なデータを入力の等式が指定するタグとペイロードに合わせます。

  matchAt (a ⇒̇ b) k r e = at (a ⇒̇ b)  k _ refl (a , b , (refl , refl)) r e
  matchAt ⊥̇ k r e = at ⊥̇  k _ refl (refl , refl) r e
  matchAt (∃̇ a) k r e = at (∃̇ a)  k _ refl (a , (refl , refl)) r e
  matchAt (∀̇ a) k r e = at (∀̇ a)  k _ refl (a , (refl , refl)) r e
  matchAt (∀̇∈ t a) k r e = at (∀̇∈ t a)  k _ refl (t , a , (refl , refl)) r e

∃[]-syntax の標準的なタグは九であり、ペイロードは境界を表す項の符号と後続アリティの本体符号との対です。この最後の構造分岐により、matchAt はすべての論理式構成子を扱います。その結論は依然として、入力としてすでに与えられた論理式の形を記述するだけです。

  matchAt (∃̇∈ t a) k r e = at (∃̇∈ t a)  k _ refl (t , a , (refl , refl)) r e

いま c が標準的な符号集合に属し、アリティの数項 # n とペイロード z の対として表示されているとします。AllCodes W への所属からは、命題的切り詰めのもとで、あるアリティ n₁、そのアリティの論理式 ψ₁、そして c とそのキーとの等式が得られます。残る仕事は n₁ を指定された n と一致させることです。

  decodeAll : (c : S) → ⟨ fst c ∈ fst (AllCodes W) ⟩ → (n : ℕ) (z : V ℓ) → fst c ≡ pr (# n) z
            → ∥ Σ[ ψ ∈ Formula Ab n ] (z ≡ cd ψ) ∥₁
  decodeAll c c∈ n z e = PT.map
    (λ { (n₁ , ψ₁ , e₁) →
      let q = pr-inj (sym e₁ ∙ e)

対符号化の単射性により、二つのアリティ数項と二つのペイロードがそれぞれ等しくなり、数項の単射性からパス n₁ ≡ n が得られます。この依存パスに沿って ψ₁ を移送し、cd-subst でその符号を補正すると、アリティが正確に n で符号が z である論理式を得ます。結果は命題的切り詰めされたままなので、選ばれた復号器も、復号された論理式の一意性も与えません。

          nq = #-inj′ (q .fst)
      in subst (Formula Ab) nq ψ₁ , (sym (q .snd) ∙ sym (cd-subst nq ψ₁)) })
    (AllCodes-out W c c∈)

部分符号で閉じた領域上の一意性

健全性の議論は、任意に与えた符号領域 C に局所化されています。候補となる表 T に加え、格納された台が W であること、十個のタグ位置が正しい数項をもつこと、環境の位置が正しい塔であること、C が必要な直下の論理式部分符号について閉じていること、そして T がまとめられた表の仕様を満たすことを仮定します。これらの仮定は、すべての論理式キーが C に属するとは述べません。

module SatSoundC {m : ℕ} (T w C E : Fin m) (N : Fin  → Fin m) (γ : S ^ m) (W : S)
  (qw : fst (lookup w γ) ≡ fst W) (tg : Tags γ N)
  (hE : ⟨ γ ⊨ towerAt E w (N f0) ⟩) (hcl : ⟨ γ ⊨ closedAt C ⟩)
  (hT : ⟨ γ ⊨ tableAt T w C E N ⟩) where
  open Alphabet W

表、符号領域、環境塔の各位置に格納された基礎階層集合を、それぞれ Tv、Cv、Ev と書きます。原子論理式では Cv における再帰的な参照は不要です。その項符号は原子論理式の橋渡しによって直接解釈されます。再帰呼出しが生じるのは、構成子が直下の子論理式をもつ場合だけです。

  open Bridge W
  private
    Tv = fst (lookup T γ)
    Cv = fst (lookup C γ)
    Ev = fst (lookup E γ)

台 W の基礎階層集合を Wv と書きます。量化子の橋渡しはこの集合を量化の範囲として用い、原子論理式の橋渡しは同じ台が定めるアルファベット上で項の符号を解釈します。証明は値を階層集合として比較するので、固定の結論は第一射影の等式であり、S にある証明付きレコード全体の等式ではありません。

    Wv = fst W

環境塔は論理式のアリティに対応する行を与え、節の枠はその行を論理式キー、タグ付き符号、候補となる表の値と組み合わせます。この枠で構成子の節を読むと、候補の値をその要素によって特徴づける意味論的関係が現れます。

    module TR = TowerRead E w (N f0) γ W qw (tg f0) hE
    module Fr = Frame T w C E N γ tg
    module Cl = Clause T w C E N
    module R = Rel T w N

まとめられた仮定 hT は、全域性、表項目のキーが C 上にあるという主張、十個の構成子の節の連言からなります。固定の証明は、全域性から子論理式の表項目を得て、構成子の節から値を特徴づけます。対象となる候補の表項目は命題に直接与えられているため、領域についての主張 hOn は包から取り出されますが、この一意性の議論では使われません。

    hTot = hT .fst
    hOn = hT .snd .fst
    hTen = hT .snd .snd

十個の構成子の節は、Fin 10 で添字づけられた一つの有限連言として格納されています。読み手 bigAnd-out はこれを族 cl k に変えるので、各構造の場合は、ほかの九個の節を変更せずに、その構成子タグが指定する節だけを選べます。

    cl : (k : Fin ) → ⟨ γ ⊨ Cl.clause k ⟩
    cl = bigAnd-out γ  Cl.clause hTen

場合のモジュールは、一つの帰納の一歩のデータをまとめます。論理式、そのタグ、そのペイロードの集合、コードとペイロードの等式、コードの定義域の中でのキーの所属、候補の表の項目、そして項目の所属です。塔の読みが、論理式のアリティのための正準な塔の項目を供給します。

    module Case {n : ℕ} (ψ : Formula Ab n) (k : Fin ) (rS : S)
      (ep : cd ψ ≡ pr (# (toℕ k)) (fst rS)) (c∈ : ⟨ fst (keyS W ψ) ∈ Cv ⟩)
      (y : S) (mem : ⟨ pr (fst (keyS W ψ)) (fst y) ∈ Tv ⟩) where
      q∈ : ⟨ pr (# n) (fst (envSet W n)) ∈ Ev ⟩
      q∈ = TR.entry-in n

論理式符号は初め標準的な数項 # k を用いて書かれています。タグの等式によってこの数項を位置 N k に格納された値へ書き換えると、得られた等式は節の入力形式に合います。その後、枠 δ12 は周囲の環境の前に十二個の座標を加えます。そこにはアリティの行、論理式キーと符号、ペイロード、候補の値が含まれます。

      ep' : fst (codeS W ψ) ≡ pr (fst (lookup (N k) γ)) (fst rS)
      ep' = ep ∙ cong (λ a → pr a (fst rS)) (sym (tg k))
      δ12 : S ^ ( + m)
      δ12 = Fr.At.δ12 (nn n) (envSet W n) (keyS W ψ) (codeS W ψ) rS y q∈ refl k ep' mem
      rel : ⟨ δ12 ⊨ R.relN (toℕ k) ⟩

選んだ節をこの具体的な枠に適用すると、タグで添字づけられた関係 relN k の充足が得られます。次に関係の読み手を δ12 に固定します。後の構成子別の読み手はこの同じ枠を拡張し、rel を原子論理式、二項結合子、量化子に適した外延の事実へ分解します。

      rel = Fr.clause-out k (cl k) (nn n) (envSet W n) (keyS W ψ) (codeS W ψ) rS y q∈ c∈ refl ep mem
      module RR = RelRead T w N δ12

子論理式のキーが Cv に属するなら、表の全域性から得られるのは、値 ya とそのキーにおける表項目との対を命題的切り詰めしたものだけです。したがって sub が証明するのは単なる存在であり、値を選ぶことではありません。各再帰の場合は、この証人を階層集合の等式へ直接消去し、h-集合構造によってその行き先が命題になります。

    sub : ∀ {n} (a : Formula Ab n) → ⟨ fst (keyS W a) ∈ Cv ⟩
        → ∥ Σ[ ya ∈ S ] ⟨ pr (fst (keyS W a)) (fst ya) ∈ Tv ⟩ ∥₁
    sub a a∈ = Fr.total-out hTot (keyS W a) a∈

中心的な述語は条件つきです。ψ のキーがコードの定義域にあれば、そのキーのもとで記録されたすべての表の値 y の底の集合は、ψ の再帰的な充足集合の底の集合と同じです。この条件つきの形が正直な形です。定義域の外のキーについては何も主張しません。

  Pinned : ∀ {n} (ψ : Formula Ab n) → Type (ℓ-suc ℓ)
  Pinned ψ = ⟨ fst (keyS W ψ) ∈ Cv ⟩
           → (y : S) → ⟨ pr (fst (keyS W ψ)) (fst y) ∈ Tv ⟩ → fst y ≡ fst (SatW ψ)

Pinned の証明は、与えられた論理式についての構造再帰として組み立てられます。再帰呼出しは、構文の構成子が直接与える子論理式にだけ行われます。C の要素についての再帰でも、任意の符号についての整礎再帰でもなく、論理式キーと同定されていない符号に値を定義する試みでもありません。

  private

符号化された論理式のペイロードの集合は、コードの等式から、対の射影によって復元されます。

    payS : ∀ {n} (ψ : Formula Ab n) (k : ℕ) (r : V ℓ) → cd ψ ≡ pr (# k) r → S
    payS ψ k r e = sndS (codeS W ψ) (# k) r e

三つの二項結合子は同じ再帰パターンを共有します。各パラメータは、構成子、タグとペイロードの等式、対応する対象言語の関係、意味論的な橋渡しを指定します。この橋渡しは、拡張された環境の二つの座標が二つの子論理式の標準的な充足関係集合に等しいという等式を仮定し、そこから複合論理式の標準値についての外延の事実を作ります。

    binCase : ∀ {n} (op : ∀ {j} → Formula S j → Formula S j → Formula S j)
              (opA : Formula Ab n → Formula Ab n → Formula Ab n) (k : Fin )
              (a b : Formula Ab n) (code : cd (opA a b) ≡ pr (# (toℕ k)) (pr (cd a) (cd b)))
              (relIs : R.relN (toℕ k) ≡ R.binRel op)
              (bridge : ∀ {j} (env : S ^ j) (ya yb : Fin j)

橋渡しは、指定された座標に二つの子の値を含む環境について述べられます。別の閉性の読み手が、複合キーの Cv への所属から、同じアリティの二つの子キーの所属を取り出します。これにより、全域性がどの子表項目を与えても、再帰仮定によってそれぞれを SatW a と SatW b に同定できます。

                      → fst (lookup ya env) ≡ fst (SatW a) → fst (lookup yb env) ≡ fst (SatW b)
                      → ExtFact (fst (SatW (opA a b))) (fst (envSet W n))
                          (λ z → ⟨ (z ∷ env) ⊨ op (var i0 ∈̇ var (suc ya)) (var i0 ∈̇ var (suc yb)) ⟩))
            → (cl2 : ⟨ fst (keyS W (opA a b)) ∈ Cv ⟩
                   → ⟨ fst (keyS W a) ∈ Cv ⟩ × ⟨ fst (keyS W b) ∈ Cv ⟩)

複合論理式が固定されることを示すため、命題的切り詰めされた左の値、右の値、二項関係の証人を順に消去します。どの消去も、最終的には等式 fst y ≡ fst (SatW (opA a b)) を目標とします。V は h-集合なのでこの等式は命題であり、消去によって子の値や枠のデータの恒久的な選択が残ることはありません。

            → Pinned a → Pinned b → Pinned (opA a b)
    binCase {n} op opA k a b code relIs bridge cl2 ia ib c∈ y mem =
      PT.rec (setIsSet _ _) (λ { (ya , ma) → PT.rec (setIsSet _ _) (λ { (yb , mb) →
        PT.rec (setIsSet _ _)
          (λ { (s , s₁ , e₁ , s₂ , e₂ , ext) →

二項関係の読み手は、二つの子論理式の符号、キー、値、および補助的な証人によって共通の節の枠を拡張します。この拡張環境では、節が候補 y の外延の事実を与え、橋渡しが SatW (opA a b) の対応する外延の事実を与えます。定理 ext-unique はこの二つの事実に集合の外延性を適用し、両者の基礎集合を等しくします。

            let env = yb ∷ keyS W b ∷ s₂ ∷ e₂ ∷ ya ∷ keyS W a ∷ s₁ ∷ e₁ ∷ codeS W b ∷ codeS W a ∷ s ∷ K.δ12
                P : S → Type (ℓ-suc ℓ)
                P z = ⟨ (z ∷ env) ⊨ R.binBody op ⟩
            in ext-unique y (SatW (opA a b)) (envSet W n) P ext
                 (bridge env i4 i0 (ia (cl2 c∈ .fst) ya ma) (ib (cl2 c∈ .snd) yb mb)) })

関係の読みは、節からタグの同一視を通して得られ、部分の値は表の全域性から、まず左の部分、次に右の部分の順で得られます。

          (K.RR.bin-out op (subst (λ φ → ⟨ K.δ12 ⊨ φ ⟩) relIs K.rel)
             (codeS W a) (codeS W b) (keyS W a) ya (keyS W b) yb refl ma refl mb refl) })
        (sub b (cl2 c∈ .snd)) })
        (sub a (cl2 c∈ .fst))
      where

局所モジュール K は、複合論理式そのもの、その構成子タグ、対になった子論理式符号のペイロードの構成可能な表現、複合キーの領域への所属、候補の表項目を記録します。これにより、二項の場合の議論全体に一つの具体的な節の枠が固定され、再帰仮定は二つの直下の子論理式だけに関わります。

      module K = Case (opA a b) k (payS (opA a b) (toℕ k) (pr (cd a) (cd b)) code) code c∈ y mem

二つの非有界量化子も一つの再帰の場合を共有します。本体は後続アリティをもち、ペイロードはその本体の符号だけです。意味論的な橋渡しは、固定された台の座標と、本体の表の値の座標を受け取ります。その値を SatW a と同定すると、橋渡しは envSet W n 上で量化された論理式の標準的な充足関係集合を特徴づけます。

    quCase : ∀ {n} (q : ∀ {j} → Term S j → Formula S (suc j) → Formula S j)
             (qA : Formula Ab (suc n) → Formula Ab n) (k : Fin )
             (a : Formula Ab (suc n)) (code : cd (qA a) ≡ pr (# (toℕ k)) (cd a))
             (relIs : R.relN (toℕ k) ≡ R.quRel q)
             (bridge : ∀ {j} (env : S ^ j) (wi yai : Fin j)

台の座標は元の周囲の環境に残り、枠を拡張した後は添字のずらしによって参照されます。子論理式の値は、関係の証人が新しく露わにする座標です。閉性から後続アリティの本体キーの所属が得られ、再帰仮定はそのキーにおけるすべての表項目を、本体の標準的な充足関係集合に同定します。これにより橋渡しは、対象言語の量化子を Wv 上の量化に正確に対応させます。

                     → fst (lookup wi env) ≡ Wv → fst (lookup yai env) ≡ fst (SatW a)
                     → ExtFact (fst (SatW (qA a))) (fst (envSet W n))
                         (λ z → ⟨ (z ∷ env) ⊨ q (var (suc wi)) (∃̇∈ (var (suc (suc yai))) (consAtL i0 i1 i2)) ⟩))
           → (cl1 : ⟨ fst (keyS W (qA a)) ∈ Cv ⟩ → ⟨ fst (keyS W a) ∈ Cv ⟩)
           → Pinned a → Pinned (qA a)

証明はまず命題的切り詰めされた本体の値を消去し、次に量化子関係の読み取りから得た命題的切り詰めされた証人を消去します。その証人は、後続の数項、本体キー、その値、補助座標によって共通の節の枠を拡張します。どちらの消去も、候補の値と標準的な量化された充足関係集合との等式を目標とするため、本体の値が大域的に選ばれることはありません。

    quCase {n} q qA k a code relIs bridge cl1 ia c∈ y mem =
      PT.rec (setIsSet _ _) (λ { (ya , ma) →
        PT.rec (setIsSet _ _)
          (λ { (s , s' , e' , ext) →
            let env = nn (suc n) ∷ s' ∷ ya ∷ keyS W a ∷ s ∷ e' ∷ K.δ12

拡張環境において、関係の節は候補の表の値 y に関する外延の事実を与えます。再帰仮定が橋渡しに必要な等式を与え、橋渡しは、ずらされた台の座標における等式を使って、SatW (qA a) に対応する外延の事実を与えます。最後に ext-unique の集合外延性が二つの基礎集合を同定します。

                P : S → Type (ℓ-suc ℓ)
                P z = ⟨ (z ∷ env) ⊨ R.quBody q ⟩
            in ext-unique y (SatW (qA a)) (envSet W n) P ext (bridge env (sh  w) i2 qw (ia (cl1 c∈) ya ma)) })
          (K.RR.qu-out q (subst (λ φ → ⟨ K.δ12 ⊨ φ ⟩) relIs K.rel) (keyS W a) ya (nn (suc n)) ma refl refl) })
        (sub a (cl1 c∈))

ここで K が具体化されるのは、量化された論理式 qA a であり、その本体 a ではありません。ペイロードの表現は本体の符号から作られますが、領域への所属と候補の表項目は量化された論理式のキーに属します。本体は、後続アリティにある唯一の再帰的な子論理式として別に現れます。

      where
      module K = Case (qA a) k (payS (qA a) (toℕ k) (cd a) code) code c∈ y mem

有界量化子の構成子符号には二つのペイロード成分があります。境界を与える項の符号と、アリティが一つ大きい本体論理式の符号です。そこでこの場合の補題は、構成子のタグとペイロードの等式、対応する関係の節、五つのスロットで固定して表した意味論的本体、その本体に対する外延の橋、そして後で実際に必要となる唯一の閉性の含意を仮定します。その含意は、複合論理式の鍵が領域に属すれば本体の鍵も領域に属すというものです。項の符号について領域の閉性は仮定しません。

    bqCase : ∀ {n} (q : ∀ {j} → Term S j → Formula S (suc j) → Formula S j)
             (c : ∀ {j} → Formula S j → Formula S j → Formula S j)
             (qA : Term Ab n → Formula Ab (suc n) → Formula Ab n) (k : Fin )
             (t : Term Ab n) (a : Formula Ab (suc n)) (code : cd (qA t a) ≡ pr (# (toℕ k)) (pr (ct t) (cd a)))
             (relIs : R.relN (toℕ k) ≡ R.bqRel q c)

本体の等式は、有界量化子の本体が五つのずらした枠でどのように綴られるかを記録します。これにより、橋を、呼び出し側の正確な枠の添字に依存しない固定された論理式の形で述べられます。

             (body : ∀ {j} → Fin j → Fin j → Fin j → Fin j → Fin j → Formula S ( + j))
             (bodyIs : ∀ {j} (wi ti yai N0i N1i : Fin j)
                     → body wi ti yai N0i N1i
                     ≡ q (var (suc wi)) (c (tmIs (suc (suc ti)) i1 i0 (suc (suc N0i)) (suc (suc N1i)))
                         (q (var (suc (suc wi))) (c (var i0 ∈̇ var i1) (∃̇∈ (var (suc (suc (suc yai)))) (consAtL i0 i1 i3))))))

この橋は、有界論理式について再帰的に定めた充足集合を、符号化された環境上で五つのスロットをもつ意味論的本体が記述する外延と対応させます。ここでは量化子と結合子がまだパラメータなので、同じ主張が有界全称の場合と有界存在の場合の両方を扱います。したがって、すべての場合にある要素の存在を主張していると読んではいけません。証明では、この外延事実を表の節から読み取った外延事実と比較します。

             (bridge : ∀ {j} (env : S ^ j) (wi ti yai N0i N1i : Fin j)
                     → fst (lookup wi env) ≡ Wv → fst (lookup ti env) ≡ ct t → fst (lookup yai env) ≡ fst (SatW a)
                     → fst (lookup N0i env) ≡ #  → fst (lookup N1i env) ≡ # 
                     → ExtFact (fst (SatW (qA t a))) (fst (envSet W n)) (λ z → ⟨ (z ∷ env) ⊨ body wi ti yai N0i N1i ⟩))
           → (cl1 : ⟨ fst (keyS W (qA t a)) ∈ Cv ⟩ → ⟨ fst (keyS W a) ∈ Cv ⟩)

複合論理式の鍵が領域に属すことから本体の鍵が領域に属すことが従い、さらに本体の鍵にある表の値がすでに固定されていると仮定します。このとき、複合論理式の鍵に与えられた任意の表の値も固定されます。全域性が与える本体の値は単に存在するだけであり、有界量化子の節の読み出しもその証人を命題的切り詰めの内側に置きます。結論は階層の基礎集合どうしの等式であり命題なので、ここではその両方を消去できます。一方、複合論理式の表の値は結論の前提として直接与えられており、全域性から得るものでも、切り詰めの内側にあるものでもありません。

           → Pinned a → Pinned (qA t a)
    bqCase {n} q c qA k t a code relIs body bodyIs bridge cl1 ia c∈ y mem =
      PT.rec (setIsSet _ _) (λ { (ya , ma) →
        PT.rec (setIsSet _ _)
          (λ { (s , s₁ , s' , e' , ext) →

節の証人を読み取った後、証明は後続アリティ、本体の表の値と鍵、本体の符号、そして境界を与える項の符号を含む拡張環境を組み立てます。その同じ環境で、ext-unique は二つの外延事実を比較します。一方は候補となる表の値を特徴づける節の外延事実であり、他方は再帰的な充足集合を特徴づける橋の外延事実です。本体の等式に沿って運ぶことで、両者に現れる述語が一致します。

            let env = nn (suc n) ∷ s' ∷ ya ∷ keyS W a ∷ s₁ ∷ e' ∷ codeS W a ∷ tS ∷ s ∷ K.δ12
                P : S → Type (ℓ-suc ℓ)
                P z = ⟨ (z ∷ env) ⊨ R.bqBody q c ⟩
            in ext-unique y (SatW (qA t a)) (envSet W n) P ext
                 (subst (λ φ → ExtFact (fst (SatW (qA t a))) (fst (envSet W n)) (λ z → ⟨ (z ∷ env) ⊨ φ ⟩))

まず閉性から本体の鍵が領域に属すことを得て、次に帰納仮定によって、全域性から得た本体の表の値を再帰的な充足集合と同定します。この同定と、台、項の符号、二つのタグに関する等式を合わせると、橋の仮定がすべて満たされます。有界量化子の節を外向きに読むと、四つの補助的な対象と一つの外延事実が得られますが、それらはこの局所的な比較にだけ使われます。

                    (bodyIs (sh  w) i7 i2 (sh  (N f0)) (sh  (N f1)))
                    (bridge env (sh  w) i7 i2 (sh  (N f0)) (sh  (N f1)) qw refl (ia (cl1 c∈) ya ma) (tg f0) (tg f1))) })
          (K.RR.bq-out q c (subst (λ φ → ⟨ K.δ12 ⊨ φ ⟩) relIs K.rel) tS (codeS W a) (keyS W a) ya (nn (suc n)) refl ma refl refl) })
        (sub a (cl1 c∈))
      where

名づけられた三つの成分がこの場合を支えます。台の要素として提示されたペイロード、項の符号を載せる第一の射影、そして、合成キーでの表の項目をもつ十二の枠のフレームを供給する場合のモジュールです。

      rS : S
      rS = payS (qA t a) (toℕ k) (pr (ct t) (cd a)) code
      tS : S
      tS = fstS rS (ct t) (cd a) refl
      module K = Case (qA t a) k rS code c∈ y mem

原子論理式には論理式としての子がないので、この場合には閉性の含意も再帰仮定も要りません。構成子のペイロードは二つの項の符号の対です。残りの仮定は、対応する原子関係の節を同定し、台の等式、二つの項の符号の等式、二つのタグの等式から、原子論理式の再帰的な充足集合についての外延事実を与える橋を用意します。

    atomCase : ∀ {n} (opA : ∀ {j} → Term Ab j → Term Ab j → Formula Ab j) (k : Fin )
               (t u : Term Ab n) (code : cd (opA t u) ≡ pr (# (toℕ k)) (pr (ct t) (ct u)))
               (rel : Formula S ( + m))
               (relIs : R.relN (toℕ k) ≡ R.atomRel rel)
               (bridge : ∀ (env : S ^ ( + m)) (wi ti ui N0i N1i : Fin ( + m))

橋のパラメータは原子論理式の外延事実を述べます。充足関係集合には、項の値が対象言語の関係を満たす環境がちょうど含まれます。結論は、この原子論理式のキーが領域に属し、表項目が与えられていれば、その論理式が固定されることを述べます。

                       → fst (lookup wi env) ≡ Wv → fst (lookup ti env) ≡ ct t → fst (lookup ui env) ≡ ct u
                       → fst (lookup N0i env) ≡ #  → fst (lookup N1i env) ≡ # 
                       → ExtFact (fst (SatW (opA t u))) (fst (envSet W n)) (λ z → ⟨ (z ∷ env) ⊨ atomEx wi ti ui N0i N1i rel ⟩))
             → Pinned (opA t u)
    atomCase {n} opA k t u code rel relIs bridge c∈ y mem =

原子の節からは、補助的な集合と候補となる表の値についての外延事実が、単なる存在として得られます。その集合と二つの項の符号から作った環境では、原子の橋が再帰的な充足値について第二の外延事実を与えます。累積階層の等式は命題なので、節の隠された証人を消去でき、ext-unique によって二つの基礎集合が同定されます。

      PT.rec (setIsSet _ _)
        (λ { (s , ext) →
          let env = uS ∷ tS ∷ s ∷ K.δ12
              P : S → Type (ℓ-suc ℓ)
              P z = ⟨ (z ∷ env) ⊨ R.atomBody rel ⟩

橋は、拡張された環境で、二つのタグの等式と台の等式とともに適用され、原子の本体の外延の事実を作ります。原子の関係の外向きの読み出しが、中間の集合を供給します。

          in ext-unique y (SatW (opA t u)) (envSet W n) P ext
               (bridge env (sh  w) i1 i0 (sh  (N f0)) (sh  (N f1)) qw refl refl (tg f0) (tg f1)) })
        (K.RR.atom-out rel (subst (λ φ → ⟨ K.δ12 ⊨ φ ⟩) relIs K.rel) tS uS refl)
      where
      rS : S

名づけられた三つの成分が原子の場合を支えます。台の要素としてのペイロード、その第一と第二の射影としての二つの項の符号、そして十二の枠のフレームを供給する場合のモジュールです。

      rS = payS (opA t u) (toℕ k) (pr (ct t) (ct u)) code
      tS uS : S
      tS = fstS rS (ct t) (ct u) refl
      uS = sndS rS (ct t) (ct u) refl
      module K = Case (opA t u) k rS code c∈ y mem

この所属原子では、表示された環境における充足は、二つの基礎集合の間の所属命題と定義上同じです。したがって memAgree の二つの向きはいずれも恒等写像です。これは原子の橋がこの箇所で必要とする局所的な一致であり、ほかの関係記号については何も主張しません。

    memAgree : ∀ {j} (env : S ^ j) (z v x : S)
             → (⟨ (x ∷ v ∷ z ∷ env) ⊨ var i1 ∈̇ var i0 ⟩ → ⟨ fst v ∈ fst x ⟩) × (⟨ fst v ∈ fst x ⟩ → ⟨ (x ∷ v ∷ z ∷ env) ⊨ var i1 ∈̇ var i0 ⟩)
    memAgree env z v x = (λ h → h) , (λ h → h)

等号の一致は、等号の原子についても同じことを言います。対象言語の等号は、基礎の集合の同一性です。

    eqAgree : ∀ {j} (env : S ^ j) (z v x : S)
            → (⟨ (x ∷ v ∷ z ∷ env) ⊨ var i1 ≐ var i0 ⟩ → fst v ≡ fst x) × ((fst v ≡ fst x) → ⟨ (x ∷ v ∷ z ∷ env) ⊨ var i1 ≐ var i0 ⟩)
    eqAgree env z v x = (λ h → h) , (λ h → h)

二項の結合子のための閉じの補題は、形の充足から下向きの閉じを読み出します。合成キーが領域にあれば、両方の成分キーも領域にある、というものです。証明は、二項の閉じの消去を一度適用するだけです。

    clSame : (n k : ℕ) → ⟨ γ ⊨ binShapeAt C k (bothSameAt C) ⟩
           → (ψ a b : Formula Ab n) → cd ψ ≡ pr (# k) (pr (cd a) (cd b))
           → ⟨ fst (keyS W ψ) ∈ Cv ⟩ → ⟨ fst (keyS W a) ∈ Cv ⟩ × ⟨ fst (keyS W b) ∈ Cv ⟩
    clSame n k h ψ a b e c∈ =
      binSameClosed-out C k γ h (keyS W ψ) (nn n) (codeS W a) (codeS W b) c∈ (cong (pr (# n)) e)

次の形の二項閉性補題では、形の証明を受け取る前に二つの子論理式を固定します。結論は変わりません。ペイロードがその二つの論理式の符号の対である鍵が領域に属すれば、両方の子の鍵も領域に属します。この引数順序により、構造再帰の各分岐は共通の閉性の事実を自分の二つの子に特殊化できます。

    clBin : (n k : ℕ) (a b : Formula Ab n)
          → ⟨ γ ⊨ binShapeAt C k (bothSameAt C) ⟩
          → (ψ : Formula Ab n) → cd ψ ≡ pr (# k) (pr (cd a) (cd b))
          → ⟨ fst (keyS W ψ) ∈ Cv ⟩ → ⟨ fst (keyS W a) ∈ Cv ⟩ × ⟨ fst (keyS W b) ∈ Cv ⟩
    clBin n k a b h ψ e = clSame n k h ψ a b e

非有界量化子では、閉性は構成子のペイロードに含まれる唯一の論理式成分だけをたどります。したがって、アリティ n の量化された論理式の鍵が領域に属すれば、後続アリティにある本体の鍵も領域に属します。この主張は、ここで提示された構成子符号に局所的なものであり、領域の任意の要素を復号するものではありません。

    clQu : (n k : ℕ) (a : Formula Ab (suc n)) (ψ : Formula Ab n)
         → ⟨ γ ⊨ unShapeAt C k (oneSuccAt C) ⟩ → cd ψ ≡ pr (# k) (cd a)
         → ⟨ fst (keyS W ψ) ∈ Cv ⟩ → ⟨ fst (keyS W a) ∈ Cv ⟩
    clQu n k a ψ h e c∈ =
      unSuccClosed-out C k γ h (keyS W ψ) (nn n) (codeS W a) c∈ (cong (pr (# n)) e)

有界量化子のペイロードでは、第一成分が項の符号、第二成分が本体論理式の符号です。閉性の条件がたどるのは第二成分だけであり、複合論理式の鍵が領域に属すことから、後続アリティにある本体の鍵が領域に属すことを導きます。境界を与える項の符号について、領域への所属は意図的に何も結論しません。

    clBq : (n k : ℕ) (t : Term Ab n) (a : Formula Ab (suc n)) (ψ : Formula Ab n)
         → ⟨ γ ⊨ binShapeAt C k (succSndAt C) ⟩ → cd ψ ≡ pr (# k) (pr (ct t) (cd a))
         → ⟨ fst (keyS W ψ) ∈ Cv ⟩ → ⟨ fst (keyS W a) ∈ Cv ⟩
    clBq n k t a ψ h e c∈ =
      binSuccClosed-out C k γ h (keyS W ψ) (nn n) tS (codeS W a) c∈ (cong (pr (# n)) e)

名づけられた二つの成分が、有界量化子のための閉じを支えます。台の要素として提示されたペイロードと、項の符号を載せるその第一の射影です。

      where
      pS : S
      pS = sndS (codeS W ψ) (# k) (pr (ct t) (cd a)) e
      tS : S
      tS = fstS pS (ct t) (cd a) refl

釘づけの述語は、論理式の構造についての構造再帰で証明されます。所属の原子は、所属の関係に対する恒等の一致とともに原子の場合を適用し、下位の論理式の仮定を一切消費しません。

  pinned : ∀ {n} (ψ : Formula Ab n) → Pinned ψ
  pinned (t ∈̇ u) = atomCase _∈̇_ f0 t u refl (var i1 ∈̇ var i0) refl
    (λ env wi ti ui N0i N1i qw' qt qu q0 q1 →
      AtomBridge.atomBridge t u env wi ti ui N0i N1i qw' qt qu q0 q1 _∈̇_ (λ v x → ⟨ v ∈ x ⟩)
        (var i1 ∈̇ var i0) (memAgree env) (λ δ h → h) (λ δ h → h))

等号の原子は、等号に対する恒等の一致とともに原子の場合を適用します。連言の場合は、連言の橋とタグ二での二項の閉じとともに二項の場合を適用し、二つの下位の論理式の釘づけの仮定を消費します。

  pinned (t ≐ u) = atomCase _≐_ f1 t u refl (var i1 ≐ var i0) refl
    (λ env wi ti ui N0i N1i qw' qt qu q0 q1 →
      AtomBridge.atomBridge t u env wi ti ui N0i N1i qw' qt qu q0 q1 _≐_ (λ v x → v ≡ x)
        (var i1 ≐ var i0) (eqAgree env) (λ δ h → h) (λ δ h → h))
  pinned {n} (a ∧̇ b) = binCase _∧̇_ _∧̇_ f2 a b refl refl (andBridge a b) (clBin n  a b (hcl .fst) (a ∧̇ b) refl) (pinned a) (pinned b)

選言と含意は、それぞれのタグで同じ二項のパターンに従います。偽には下位の論理式がなく、その一意性は、偽の条項の外向きの読み出しと偽の橋から直接証明されます。両方が合わせて空の外延を作るからです。

  pinned {n} (a ∨̇ b) = binCase _∨̇_ _∨̇_ f3 a b refl refl (orBridge a b) (clBin n  a b (hcl .snd .fst) (a ∨̇ b) refl) (pinned a) (pinned b)
  pinned {n} (a ⇒̇ b) = binCase _⇒̇_ _⇒̇_ f4 a b refl refl (impBridge a b) (clBin n  a b (hcl .snd .snd .fst) (a ⇒̇ b) refl) (pinned a) (pinned b)
  pinned {n} ⊥̇ c∈ y mem = ext-unique y (SatW ⊥̇) (envSet W n) (λ z → ⟨ (z ∷ K.δ12) ⊨ ⊥̇ ⟩) (extB-out i0 i8 ⊥̇ K.δ12 K.rel) (botBridge n K.δ12)
    where
    module K = Case ⊥̇ f5 (nn ) refl c∈ y mem

二つの非有界量化子の分岐は、それぞれ存在の橋と全称の橋を使います。閉性によって量化された論理式の鍵から後続アリティの本体の鍵へ領域への所属を移し、再帰仮定によって橋が必要とする本体の値を固定します。有界全称の分岐も同じ局所的な形を取りますが、その構成子符号には項の符号も含まれます。この分岐は全称の ∀[]-syntax の橋を用いて有界の場合を適用し、閉性はここでも本体だけをたどります。

  pinned {n} (∃̇ a) = quCase ∃̇∈ ∃̇_ f6 a refl refl (exBridge a) (clQu n  a (∃̇ a) (hcl .snd .snd .snd .fst) refl) (pinned a)
  pinned {n} (∀̇ a) = quCase ∀̇∈ ∀̇_ f7 a refl refl (allBridge a) (clQu n  a (∀̇ a) (hcl .snd .snd .snd .snd .fst) refl) (pinned a)
  pinned {n} (∀̇∈ t a) = bqCase ∀̇∈ _⇒̇_ ∀̇∈ f8 t a refl refl bqAll (λ _ _ _ _ _ → refl)
    (λ env wi ti yai N0i N1i qw' qt qa q0 q1 → BqBridge.allInBridge t a env wi ti yai N0i N1i qw' qt qa q0 q1)
    (clBq n  t a (∀̇∈ t a) (hcl .snd .snd .snd .snd .snd .fst) refl) (pinned a)

有界存在の分岐は、存在の ∃[]-syntax の橋を用いて有界の場合を適用します。対応する閉性の成分が与えるのは、後続アリティにある本体の鍵の領域への所属だけであり、その後で再帰仮定が本体の表の値を固定します。境界を与える項は橋の中で評価され、別の再帰部分問題にはなりません。

  pinned {n} (∃̇∈ t a) = bqCase ∃̇∈ _∧̇_ ∃̇∈ f9 t a refl refl bqEx (λ _ _ _ _ _ → refl)
    (λ env wi ti yai N0i N1i qw' qt qa q0 q1 → BqBridge.exInBridge t a env wi ti yai N0i N1i qw' qt qa q0 q1)
    (clBq n  t a (∃̇∈ t a) (hcl .snd .snd .snd .snd .snd .snd) refl) (pinned a)

すべての充足関係の節を満たす

ここから逆向きの接続を証明します。節から再帰的な値を取り出すのではなく、表に表示された値がすでに再帰的に定めた充足集合と一致すると仮定し、その一致を使って各節を検証します。作業集合 W は、この向きで一貫して使うアルファベット、充足の橋、構成子符号の照合を定めます。

module _ (W : S) where
  open Alphabet W
  open Bridge W
  open Match W

一つの環境の中で、表、台、論理式符号の領域、環境の塔の各スロットを固定し、十個の数項タグと塔の仕様を与えます。中心となる仮定 val≡ は条件付きです。既知の論理式の鍵と、その鍵にある与えられた表の要素に対して、その要素の基礎の値を論理式の再帰的な充足集合と同定します。すべての鍵が表されるとは主張せず、表の要素を選ぶこともしません。

  module SatHoldsC {m : ℕ} (T w C E : Fin m) (N : Fin  → Fin m) (γ : S ^ m)
    (qw : fst (lookup w γ) ≡ fst W) (tg : Tags γ N)
    (hE : ⟨ γ ⊨ towerAt E w (N f0) ⟩)
    (val≡ : ∀ {n} (ψ : Formula Ab n) (c yc : S) → fst c ≡ fst (keyS W ψ)
          → ⟨ pr (fst c) (fst yc) ∈ fst (lookup T γ) ⟩ → fst yc ≡ fst (SatW ψ))

さらに三つの仮定は、命題的切り詰めの下でのみ存在を与えます。領域の要素がアリティ符号とペイロードの対として提示されると、指定されたそのアリティの論理式へ単に復号できるだけです。全域性は各領域の鍵にある何らかの表の値を単に与え、表の各要素も、鍵が領域に属す鍵と値の対へ単に分解されます。これらの仮定はいずれも、再利用できる復号関数や値の選択関数を定めません。

    (decode : (c : S) → ⟨ fst c ∈ fst (lookup C γ) ⟩ → (n : ℕ) (z : V ℓ)
            → fst c ≡ pr (# n) z → ∥ Σ[ ψ ∈ Formula Ab n ] (z ≡ cd ψ) ∥₁)
    (tot : (c : S) → ⟨ fst c ∈ fst (lookup C γ) ⟩
         → ∥ Σ[ yc ∈ S ] ⟨ pr (fst c) (fst yc) ∈ fst (lookup T γ) ⟩ ∥₁)
    (onc : (e : S) → ⟨ fst e ∈ fst (lookup T γ) ⟩

最後の仮定は領域条件を完成させます。表に表示された各要素は、指定された符号領域に c が属すような対 (c,yc) として、単に存在するものとして同定されます。したがって全域性は鍵から値への向きを制御し、この条件は表の要素から領域の鍵へ戻る向きを制御します。略記 Tv と Cv は、これらの局所的な主張で使う表と領域の基礎集合を名づけるだけです。

         → ∥ Σ[ c ∈ S ] Σ[ yc ∈ S ] ((fst e ≡ pr (fst c) (fst yc)) × ⟨ fst c ∈ fst (lookup C γ) ⟩) ∥₁)
    where
    private
      Tv = fst (lookup T γ)
      Cv = fst (lookup C γ)

さらに、環境の塔の基礎集合と台を名づけます。枠、節、関係の読み出しは、同じ格納データを三つの尺度で表します。十二個の対象からなる共通の枠、表の最上位の条件、そして構成子ごとの関係です。これらは固定された環境の局所的な見方であり、新しい数学的仮定ではありません。

      Ev = fst (lookup E γ)
      Wv = fst W
      module Fr = Frame T w C E N γ tg
      module Cl = Clause T w C E N
      module R = Rel T w N

Arity ar F は、ある自然数 n が単に存在し、ar が n の数項であり、F が対応する符号化環境の集合 envSet W n であることを述べます。証人 n は命題的切り詰めの内側に留まるので、この型は命題値の証明に必要なアリティ情報を記録するだけで、後の計算に使うアリティを選びません。

      Arity : (ar F : S) → Type (ℓ-suc ℓ)
      Arity ar F = ∥ Σ[ n ∈ ℕ ] ((fst ar ≡ # n) × (fst F ≡ fst (envSet W n))) ∥₁

このアリティの証拠を得るには、環境の塔の要素 q を対 (ar,F) として提示します。すると塔の仕様に、台の等式と零タグの等式を合わせることで、その対から、単に存在する自然数アリティとその正準な環境集合を読み取れます。

      arity : (q ar F : S) → ⟨ fst q ∈ Ev ⟩ → fst q ≡ pr (fst ar) (fst F) → Arity ar F
      module TR = TowerRead E w (N f0) γ W qw (tg f0) hE

対の等式によって、q の所属証明を表示された対 (ar,F) へ運びます。続いて塔の要素に関する定理が、命題的切り詰めの内側にあるまま Arity ar F を返します。この段階で取り出すのは現在の要素に必要な局所的アリティ証拠だけであり、塔の符号化に対する大域的な逆関数は定めません。

      arity q ar F q∈ eq = TR.entry-out ar F (subst (λ u → ⟨ u ∈ Ev ⟩) eq q∈)

表に対する第一の最上位条件は、指定された論理式符号の領域上での全域性です。仮定 tot はすでにその意味内容を正確に与えており、各値は単に存在するだけです。そこで枠の補題は、この仮定を対象言語の全域性の節が充足されることへ直接変換します。

      total : ⟨ γ ⊨ Cl.total ⟩
      total = Fr.total-in tot

第二の最上位条件は、表に表示された各要素が、指定された領域の鍵の上にあることを述べます。仮定 onc は基礎集合の水準でまさにこの条件を表すので、枠の補題によって対応する対象言語の節の充足へ変換できます。

      onC : ⟨ γ ⊨ Cl.onC ⟩
      onC = Fr.onC-in onc

各構成子の節は、同じ十二対象の配置について検証されます。最初のフィールド群はそれらの対象を記録します。すなわち、塔の要素とそのアリティおよび環境集合、論理式符号の領域の要素とその構成子ペイロード、表の要素とその値、そして対象言語の論理式が必要とする補助的な証人です。

      record Args (k : Fin ) : Type (ℓ-suc ℓ) where
        field
          q ar F s c p s1 r s2 e yc s3 : S
          q∈ : ⟨ fst q ∈ Ev ⟩
          eq : fst q ≡ pr (fst ar) (fst F)

残りのフィールドは、それらの対象を一つの整合した枠にする関係を述べます。塔の要素がアリティと環境集合の対であること、論理式の符号が領域に属してアリティ、タグ、ペイロードへ分かれること、そして表の要素が表に属してその符号と候補値へ分かれることです。これらは局所的な表示の等式であり、一意性や大域的な復号を主張しません。

          c∈ : ⟨ fst c ∈ Cv ⟩
          ec : fst c ≡ pr (fst ar) (fst p)
          ep : fst p ≡ pr (# (toℕ k)) (fst r)
          e∈ : ⟨ fst e ∈ Tv ⟩
          ee : fst e ≡ pr (fst c) (fst yc)

一つのタグと、整合した十二対象の枠を固定すると、問題は一つの構成子の節を検証することに絞られます。この範囲で後に行う議論はすべて同じ対象と等式を使うので、そのタグのペイロードが必要な外延事実をどのように定めるかに集中できます。

      module Fill (k : Fin ) (A : Args k) where
        open Args A

枠は、節の論理式が要求する正確な座標順に、十二個の対象 yc、s3、e、r、s2、p、s1、c、F、ar、s、q を元の環境 γ の前へ加えます。したがって、候補値、表項目、構成子のペイロード、論理式符号、環境集合、アリティ、塔の項目は四つの補助的な証人を間に挟みながら、節が用いる添字に正確に置かれます。

        frame : S ^ ( + m)
        frame = yc ∷ s3 ∷ e ∷ r ∷ s2 ∷ p ∷ s1 ∷ c ∷ F ∷ ar ∷ s ∷ q ∷ γ

この固定された枠では、タグに対応する関係の定理を、その意味論的な外延条件と対象言語の関係の節との間で双方向に使えます。充足を組み立てる証明が使うのは構成する向きです。復号されたペイロードとあらかじめ定められた子の値から正しい外延事実が得られれば、そのタグの関係の節が従います。

        module RR = RelRead T w N frame

それぞれの充填の場合の目標は、十二の枠のフレームで、与えられたタグに対する関係の条項の充足です。

        Goal : Type (ℓ-suc ℓ)
        Goal = ⟨ frame ⊨ R.relN (toℕ k) ⟩

この目標は命題値です。この構造における任意の論理式の充足が h-命題だからです。これが後で使う命題的切り詰めの正確な消去境界になります。単に復号されたアリティ、論理式、構成子の形は、この目標を証明するためには使えますが、再利用可能な計算データとして取り出すことはできません。

        isPropGoal : isProp Goal
        isPropGoal = snd (frame ⊨ R.relN (toℕ k))

移行の補題が重要なステップです。アリティの等式、環境集合の等式、論理式符号の等式 fst p ≡ cd ψ、そして ψ の充足関係集合についての外延事実が与えられると、枠にある表の値について対応する外延事実を作ります。この三つの等式は、枠のアリティ、環境集合、論理式符号の対象を、再帰的な充足関係集合が用いるデータにそろえます。

        transfer : (n : ℕ) (ψ : Formula Ab n) → fst ar ≡ # n → fst F ≡ fst (envSet W n)
                 → fst p ≡ cd ψ → {j : ℕ} (env : S ^ j) (φ : Formula S ( + j))
                 → ExtFact (fst (SatW ψ)) (fst (envSet W n)) (λ z → ⟨ (z ∷ env) ⊨ φ ⟩)
                 → RR.Ext env φ
        transfer n ψ qa qF qp env φ ext =

まず枠の等式から、c が復号された論理式の正準な鍵であり、与えられた表の要素が c と yc の対であることを示します。すると値の一致の仮定により、yc の基礎集合が再帰的な充足集合と同定されます。最後に、その値の等式を逆向きに用い、さらに F を正準な環境集合と同定する等式に沿って運ぶことで、橋の外延事実を枠が要求する外延事実へ変換します。

          subst2 (λ Y F' → ExtFact Y F' (λ z → ⟨ (z ∷ env) ⊨ φ ⟩))
            (sym (val≡ ψ c yc (ec ∙ cong₂ pr qa qp) (subst (λ u → ⟨ u ∈ Tv ⟩) ee e∈))) (sym qF) ext

下位の値の補題は、同じアリティの子の項目に、値の一致の仮定を適用します。子の表の項目から充足集合を復元するのです。

        subVal : (n : ℕ) (a : Formula Ab n) (c₁ ya e₁ : S) → fst ar ≡ # n
               → ⟨ fst e₁ ∈ Tv ⟩ → fst e₁ ≡ pr (fst c₁) (fst ya) → fst c₁ ≡ pr (fst ar) (cd a)
               → fst ya ≡ fst (SatW a)
        subVal n a c₁ ya e₁ qa e₁∈ ee₁ e₁' =
          val≡ a c₁ ya (e₁' ∙ cong (λ v → pr v (cd a)) qa) (subst (λ u → ⟨ u ∈ Tv ⟩) ee₁ e₁∈)

量化子の本体では、子の鍵は後続アリティにあります。追加の等式は、そのアリティ成分 ar' を親のアリティ成分のフォン・ノイマン後続と同定します。これを ar = # n と合成すると suc n の数項が得られます。したがって値の一致の仮定により、子の表の値を本体の再帰的な充足集合と同定できます。これはアリティの計算であり、構成可能階層の段階についての主張ではありません。

        subValS : (n : ℕ) (a : Formula Ab (suc n)) (c₁ ya e₁ ar' : S) → fst ar ≡ # n
                → ⟨ fst e₁ ∈ Tv ⟩ → fst e₁ ≡ pr (fst c₁) (fst ya) → fst c₁ ≡ pr (fst ar') (cd a) → fst ar' ≡ sucV (fst ar)
                → fst ya ≡ fst (SatW a)
        subValS n a c₁ ya e₁ ar' qa e₁∈ ee₁ e₁' es =
          val≡ a c₁ ya (e₁' ∙ cong (λ v → pr v (cd a)) (es ∙ cong sucV qa)) (subst (λ u → ⟨ u ∈ Tv ⟩) ee₁ e₁∈)

データの型は、復号されたアリティ、環境の集合、論理式、そしてタグの照合を集めます。構成子の場合を振り分けるために必要なすべてです。

        Data : Type (ℓ-suc ℓ)
        Data = Σ[ n ∈ ℕ ] ((fst ar ≡ # n) × ((fst F ≡ fst (envSet W n))
                 × (Σ[ ψ ∈ Formula Ab n ] ((fst p ≡ cd ψ) × MatchN (toℕ k) ψ (fst r)))))

data' の証拠は、全体を通して命題的切り詰めの内側に留まります。まず塔の要素が、あるアリティとその環境集合を単に与えます。その各証人に対して、decode はそのアリティのある論理式を単に与え、PT.map が matchAt から得た構成子の形の証明を付け加えます。外側の消去先も再び切り詰められた型なので、アリティや論理式が大域的に選ばれることはありません。

        data' : ∥ Data ∥₁
        data' = PT.rec squash₁
          (λ { (n , (qa , qF)) → PT.map
            (λ { (ψ , qp) → n , (qa , qF , ψ , (qp , matchAt ψ (toℕ k) (fst r) (sym qp ∙ ep))) })
            (decode c c∈ n (fst p) (ec ∙ cong (λ v → pr v (fst p)) qa)) })

外側の命題的切り詰めの消去に渡す最後の引数は、提示された塔の要素から読み取った局所的な Arity ar F の証拠です。これは上の入れ子になった切り詰め付き復号を開始しますが、隠された自然数の証人をそれだけで外へ取り出すことはありません。

          (arity q ar F q∈ eq)

任意の二項構成子について、まず二つの子論理式の表の値を、それぞれの再帰的な充足集合と同定します。次に二項の橋は、二つの子充足集合への所属を対応する対象言語の結合子で組み合わせることにより、複合論理式の再帰的な充足集合を特徴づけます。この共通の議論を、連言、選言、含意にそれぞれ用います。

        module BinFill (op : ∀ {j} → Formula S j → Formula S j → Formula S j)
          (opA : ∀ {j} → Formula Ab j → Formula Ab j → Formula Ab j)
          (bridge : ∀ {n} (a b : Formula Ab n) {j : ℕ} (env : S ^ j) (ya yb : Fin j)
                  → fst (lookup ya env) ≡ fst (SatW a) → fst (lookup yb env) ≡ fst (SatW b)
                  → ExtFact (fst (SatW (opA a b))) (fst (envSet W n))

橋の外延の事実は、二つの下位の充足集合の上の所属の原子に、二項の結合子を適用する論理式の上で述べられます。

                      (λ z → ⟨ (z ∷ env) ⊨ op (var i0 ∈̇ var (suc ya)) (var i0 ∈̇ var (suc yb)) ⟩)) where

ペイロードの等式は、枠のペイロードが二つの子論理式の符号の対であることを述べます。対の単射性から二つの成分の等式を別々に取り出し、subVal はそれらを使って、表された各子の値の底集合を再帰的に定義された値 SatW の底集合と同定します。

          go : (n : ℕ) (a b ψ : Formula Ab n) → fst ar ≡ # n → fst F ≡ fst (envSet W n)
             → fst p ≡ cd ψ → ψ ≡ opA a b → fst r ≡ pr (cd a) (cd b) → ⟨ frame ⊨ R.binRel op ⟩
          go n a b ψ qa qF qp qψ qr = RR.bin-in op (λ a' b' s' c₁ ya s₁ e₁ c₂ yb s₂ e₂ er e₁∈ ee₁ e₁' e₂∈ ee₂ e₂' →
            let q' = pr-inj (sym er ∙ qr)
                ya≡ = subVal n a c₁ ya e₁ qa e₁∈ ee₁ (e₁' ∙ cong (pr (fst ar)) (q' .fst))

この二つの子の値の等式は、対応する表の項目と同じ拡張環境に置かれます。結合子の橋渡しは二項の節によって SatW (opA a b) を特徴づけ、transfer はその正準な値と環境集合を、枠にすでにある候補値と環境集合へ置き換えます。

                yb≡ = subVal n b c₂ yb e₂ qa e₂∈ ee₂ (e₂' ∙ cong (pr (fst ar)) (q' .snd))
                env = yb ∷ c₂ ∷ s₂ ∷ e₂ ∷ ya ∷ c₁ ∷ s₁ ∷ e₁ ∷ b' ∷ a' ∷ s' ∷ frame
            in transfer n (opA a b) qa qF (qp ∙ cong cd qψ) env (R.binBody op)
                 (bridge a b env i4 i0 ya≡ yb≡))

非有界量化された論理式では、再帰的な子論理式のアリティは後続になりますが、その意味論的な量化は台 W 上を動きます。そこで抽象的な構成子 q' は後で ∃[]-syntax または ∀[]-syntax に具体化され、qA はアルファベット上の対応する非有界構成子を表し、橋渡しはその再帰的な充足集合を台で有界化した節に結び付けます。

        module QuFill (q' : ∀ {j} → Term S j → Formula S (suc j) → Formula S j)
          (qA : ∀ {j} → Formula Ab (suc j) → Formula Ab j)
          (bridge : ∀ {n} (a : Formula Ab (suc n)) {j : ℕ} (env : S ^ j) (wi yai : Fin j)
                  → fst (lookup wi env) ≡ Wv → fst (lookup yai env) ≡ fst (SatW a)
                  → ExtFact (fst (SatW (qA a))) (fst (envSet W n))

この節は、候補となる符号化環境 z を判定します。外側の構成子は後で ∃[]-syntax または ∀[]-syntax に具体化され、台 W 上を量化します。その各要素について、内側の ∃[]-syntax は、その要素を z に付け加えて得られる符号化環境が、子論理式を表す充足集合の要素として存在することを要求します。これは一回の量化を対象言語で記述したものであり、復号器でも、再利用可能な証人の選択でもありません。