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

対話型目次 · 依存グラフ

一つの宇宙レベルと、この古典論理の実例を固定する。本章では、同じ真理条件の二つの記述を比較する。符号化された側では、環境が再帰的に定義された集合 Sat B φ に属する。意味論の側では、対応する割当てが、B の要素を論域とする構造で φ を充足する。二つの記述が同じ制限構造で定数を解釈できるように、定数も B の要素を名指すものに限る。

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

再帰的構成 Sat は各論理式に符号化された環境の集合を割り当てるが、その再帰方程式が意図した意味をもつためには、それらの符号を B の要素からなる構造の実際の割当てと比較しなければならない。ここで重要なのは、この制限構造の内側の意味論を使うことである。量化変数はすでに B 上を動き、有界量化子はさらに、限界項の値への所属という別の条件を課す。

明示的な仮定は、レベル ℓ-suc ℓ における排中律だけである。以下の論理式に関する帰納法そのものは命題について場合分けをしない。この仮定は、すでに構成された環境集合と充足集合を通して入る。それらの分出は lem をパラメータとしているからである。

open import Cubical.Foundations.Prelude using ( funExt⁻ )

証明は論理式の構文に沿って進む。論理式には二つの原子構成子、三つの命題結合子、偽、二つの非有界量化子、そして項で限界づけられた二つの有界量化子がある。したがって意味論の比較には十の場合がある。項と論理式の定数アルファベットは、それぞれ mapTm と mapFo によって取り替えられ、mapFo-comp は二度続けた取り替えが合成写像による取り替えと一致することを述べる。こうして B の要素を定数とする論理式を、その構文を変えずに周囲の定数アルファベットへ移せる。

定数の改名は意味論的に正確である。写像 f に沿って定数を取り替えたとき、解釈 ι のもとで mapFo f φ を評価した真理値は、合成された解釈 ι ∘ f のもとで φ を評価した真理値と一致する。これが ⊨-map である。本章では、小さな要素添字、制限構造の要素、構成可能集合の間を移るときに、この等式を用いる。周囲の階層とその順序対演算は、符号化された環境を作る集合を供給する。

先行する三つの構成が、この橋で使う数学的データを供給する。集合 B に対して、DefOf は B への所属に制限した構造と、その構造で定義可能な部分集合を与える。環境の符号化は有限の割当てを値のグラフで表し、一つの値を先頭に加えることで拡張を表す。最後に、環境集合の構成は、固定されたアリティをもつそのようなグラフをすべて集める。ここで使う推移性はクラス L の推移性である。構成可能集合の要素を再び構成可能とみなすために用いられ、B 自身が推移的であることは主張しない。

符号化された側と意味論の側には、すでに相補的なインターフェースがある。添字族は正準なグラフ envS を与え、envSet-in と envSet-out は正準なグラフと envSet の任意の要素を結ぶ。集合 Sat B φ はさらに、再帰的条件 cond B φ を充足するグラフを envSet B n から分出して得られる。論理式 tmIs は項の値の関係を表し、その変数の場合を読む補題を伴う。原子論理式と非有界量化子に関する読み出しは、対応する節を両方向に翻訳する。これらの主張が説明するのは cond であり、envSet に属するという追加条件は Sat-mem の別の成分として残る。

残る読み出しは二つの有界量化子を扱う。先のインターフェースと合わせると、cond の命題結合子以外の各節を両方向に展開できる。有界な節では二つの制限を区別する。新しい値は台 B に属さなければならず、同時に限界項の値にも属さなければならない。後の帰納法では、これらを制限構造の論域と、内側の意味論に現れる限界とにそれぞれ対応させる。

証明は命題値の主張をパスによって比較する。⇔toPath は命題の間の二方向の含意をそのようなパスへ変え、その後は合同性によって比較を論理構成子の内部へ運べる。所属の原子の場合には、二つの候補となる項の値をそれぞれ意味論的な値と同定した後、subst2 が二つの等式に沿って所属関係を輸送する。存在の節と環境の回復には命題的切り詰めを用いる。切り詰めは目標が再び命題である場合にだけ除去されるので、選ばれた証人が取り出されることはない。

階層の集合には、その要素の小さな表示が備わっている。a ∈ B の証明から、同値 ∈-asFiber は ⟪ B ⟫ の添字と、その添字が表示する要素から a へのパスを返す。小さな表示での所属と通常の階層での所属の二方向の変換により、証明は二つの見方の間を移れる。この表示が重要なのは、内側の割当てが各項目の B への所属証明をすでに含み、そこから添字族を直接得られるからである。

open import Cubical.HITs.CumulativeHierarchy.Base using ( V; _∈_ )
open import Cubical.HITs.CumulativeHierarchy.Properties
  using ( ⟪_⟫; ⟪_⟫↪; ∈-asFiber; ∈∈ₛ; ∈ₛ⟪_⟫↪_ )
open import Cubical.HITs.CumulativeHierarchy.Constructions
  using ( module InfinitySet )

有限環境は von Neumann 数項をキーとして用いる。したがって位置 i : Fin n は、そのグラフでは集合 # (toℕ i) によって記録される。ここで数項の構成子を導入することで、項の変数が使う有限添字と、符号化された環境が使う集合論的なキーとが結ばれる。

open InfinitySet using ( #_ )

構成可能宇宙を hProp 値の構造として開くと、構成可能性の証明を備えた集合からなる周囲の台 S が定まる。同時に、命題値の所属を表す _∈ˢ_ と、その基礎の証明型を取り出す括弧 ⟨_⟩ も得られる。したがって以下の等式が比較するのは真理値そのものである。階層の集合の等式でも、追加のデータを運ぶ切り詰められていない同値でもない。

open hPropView 𝒮ʟ

先に導入した対象言語の条件は、すべての構成可能集合が担う構造で解釈される。一般の絶対性の構成をクラス isL に具体化すると、この周囲の充足関係 _⊨_ が得られる。その変数は構成可能集合を動く。Sat の所属の等式を開いた後、この周囲の意味論が cond B φ のような符号化された論理式を読む。これは符号化された側の中間層であり、論域が一つの特定の集合 B の要素だけからなる、さらに小さな構造とは区別しなければならない。

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

台上の制限構造

ここで B : S を固定する。その基礎となる階層の集合に DefOf を適用すると、制限された論域 DB.SM が得られる。その要素は、集合と、それが B に属することの証明との対である。構造 DB.𝒮M は、この論域の上で所属と等号を解釈する。そこで定数の恒等解釈を用いて通常の一階意味論を開くと、_⊨ᴮ_ と ⟦_⟧ᴮ が得られる。これらは DB.defSet の定義に使われる内側の充足と項の評価そのものなので、橋の意味論的な終点と定義可能部分集合は同じ制限構造を共有する。

module _ (B : S) where

module DB = DefOf (B .fst)
module SemB = FOL.Semantics DB.𝒮M
open SemB.At DB.SM id using () renaming ( _⊨_ to _⊨ᴮ_ ; ⟦_⟧ to ⟦_⟧ᴮ )

要素 x : DB.SM は、基礎の集合 x .fst と、それが B に属することの証明 x .snd からすでに成る。B が構成可能であり、クラス L が推移的なので、x .fst も構成可能である。写像 intoL は基礎の集合を保ったまま、この新しい証明書だけを補い、周囲の台 S の要素を作る。ここでは B が所属について閉じているとは仮定しない。

intoL : DB.SM → S
intoL x = x .fst , isL-trans {x = B .fst} {y = x .fst} (x .snd) (B .snd)

さらにもう一つ、定数アルファベットを結ぶ必要がある。添字 m : ⟪ B .fst ⟫ は B の一つの要素を表示する。DB.ι m はその要素と所属証明を組にして DB.SM の要素を作り、intoL は同じ基礎集合を S の要素とみなす。その合成 asConst は、小さな表示で添字づけられた論理式を周囲の意味論で読むときの定数写像である。表示写像 DB.ι と包含 intoL は異なる役割をもつが、その合成は名指された集合を変えない。

asConst : ⟪ B .fst ⟫ → S
asConst m = intoL (DB.ι m)

内側の割当てを環境として符号化する

内側の環境 δ : Vec DB.SM n は、各位置に集合とその B への所属証明をともに保存する。符号化された環境が必要とするのは集合だけである。そこで values δ は各項目を第一成分へ射影する。この基礎の値族を明示的に保つのは、項の評価と環境の拡張を、どちらもその有限グラフと比較するためである。

values : ∀ {n} → Vec DB.SM n → Fin n → V ℓ
values δ i = (lookup i δ) .fst

集合 graph δ は、この値族の有限グラフである。位置 i には、i の数項をキーとし、values δ i を値とする順序対が記録される。したがって内側のベクトルと階層の集合は、同じ割当てを二つの形で保持する。以下の補題は、この二つの間を移るために必要な正確な等式を与える。

graph : ∀ {n} → Vec DB.SM n → V ℓ
graph δ = env (values δ)

変数を束縛することは、割当ての先頭に新しい値を加えることである。基礎の値族ではこれは cons (x .fst) (values δ) であり、内側のベクトルでは x ∷ δ である。補題 cons-values は両者を各点で同定する。新しい先頭ではどちらも x .fst を与え、後ろへずれた各位置ではどちらも以前の値を与える。この一つの整合性の等式が、四つの量化子の場合すべてで再利用される。

private
  cons-values : ∀ {n} (x : DB.SM) (δ : Vec DB.SM n)
              → cons (x .fst) (values δ) ≡ values (x ∷ δ)
  cons-values x δ = funExt (λ { zero → refl ; (suc i) → refl })

ベクトルそのものが、B の小さな表示における添字族を定める。位置 i では、lookup i δ の第二成分が、その基礎の値が B に属することを証明する。この証明に ∈-asFiber を適用して、添字 index δ i を得る。この構成はベクトルにすでに保存された所属の証拠を直接使うため、命題的切り詰めも、符号化されたグラフから回復した代表の選択も含まない。

  index : ∀ {n} (δ : Vec DB.SM n) → Ix B n
  index δ i = ∈-asFiber {a = values δ i} {b = B .fst} ((lookup i δ) .snd) .fst

ファイバーの同値が返すのは添字だけではない。その添字が表示する要素と、もとの基礎の値との同一視も返す。index-eq δ i は各位置でこのパスを記録する。したがって index δ が表示する値族と values δ は各点で一致し、有限グラフを比較するための正確な入力が得られる。

  index-eq : ∀ {n} (δ : Vec DB.SM n) (i : Fin n)
           → ⟪ B .fst ⟫↪ (index δ i) ≡ values δ i
  index-eq δ i = ∈-asFiber {a = values δ i} {b = B .fst} ((lookup i δ) .snd) .snd

この添字族を正準な環境の構成子に渡すと、構成可能な周囲の構造の要素 envFor δ が得られる。これは具体的なベクトル δ に対応する、階層における正準な符号である。続く二つの事実が、その基礎のグラフを同定し、さらに環境集合への所属を証明する。任意の環境の代表を選んではいない。

envFor : ∀ {n} → Vec DB.SM n → S
envFor δ = envS B (index δ)

envFor δ の基礎となる階層の集合は、ちょうど graph δ である。関数外延性が各点のパス index-eq δ i を値族の等式にまとめ、env の合同性がそれを envFor-graph に変える。後で使うインターフェースは、この基礎集合のパスである。特に、δ を x ∷ δ へ拡張すると新しい正準な環境が得られ、切り詰めの中に隠れた証人を比較せずに、同じ定理を再び適用できる。

envFor-graph : ∀ {n} (δ : Vec DB.SM n) → (envFor δ) .fst ≡ graph δ
envFor-graph δ = cong env (funExt (index-eq δ))

最初の帰結は、既知のベクトルから環境集合への所属へ進む。z : S の基礎集合が graph δ であるとする。正準な環境 envFor δ は envSet-in によって envSet B n に属し、envFor-graph と仮定したパスに沿ってその所属を z へ輸送すれば、graph-envSet が得られる。後の所属の等式が Sat B φ から共通の環境条件を取り除くときに必要とするのは、まさにこの向きである。逆向きは論理的な強さが異なる。envSet-out が回復する添字族は命題的切り詰めの中にあり、後の構成がそれをベクトルへ変換するときも切り詰めを保つ。この回復は論理式に関する帰納法の外に置かれる。

graph-envSet : ∀ {n} (δ : Vec DB.SM n) (z : S)
             → z .fst ≡ graph δ → ⟨ z ∈ˢ envSet B n ⟩
graph-envSet {n} δ z q = subst (λ w → ⟨ w ∈ (envSet B n) .fst ⟩)
  (envFor-graph δ ∙ sym q) (envSet-in B (index δ))

グラフの等式により、所属の等式から共通の環境条件を取り除ける。Sat-mem は、z が Sat B φ に属すことを、envSet B n への所属と cond B φ の充足との論理積として表す。z .fst ≡ graph δ が与えられれば、直前の補題から前者が得られるので、後者は論理積全体と論理的に同値である。⇔toPath はその二方向の含意を真理値の間のパスにする。したがって Sat-cond はまだ論理式の意味を説明せず、次の帰納法で解釈すべき再帰条件だけを取り出す。

Sat-cond : ∀ {n} (φ : Formula S n) (δ : Vec DB.SM n) (z : S)
         → z .fst ≡ graph δ
         → (z ∈ˢ Sat B φ) ≡ ((z ∷ []) ⊨ cond B φ)
Sat-cond φ δ z q =
  Sat-mem B φ z ∙ ⇔toPath (λ p → p .snd) (λ h → graph-envSet δ z q , h)

項と環境拡張を読み取る

最初の読み補題は、対象言語の項述語と実際の項評価を比較する。周囲の環境 γ では、スロット ei が符号化された割当てを、スロット viが候補の値を収める。前者の基礎集合が graph δ なら、tmIs (mapTm intoL t) vi ei の充足から、後者の基礎集合が(⟦ t ⟧ᴮ δ) .fst に等しいことが従う。定数の場合、この述語はすでに求める等式である。intoL による定数の改名は台の包装だけを変え、基礎集合はその定数の値のままである。

tmIs-out : ∀ {n k} (t : Term DB.SM n) (δ : Vec DB.SM n) (γ : Vec S k) (vi ei : Fin k)
         → (lookup ei γ) .fst ≡ graph δ
         → ⟨ γ ⊨ tmIs (mapTm intoL t) vi ei ⟩
         → (lookup vi γ) .fst ≡ (⟦ t ⟧ᴮ δ) .fst
tmIs-out (con c) δ γ vi ei qe h = h

変数の場合、tmIs-var-out は充足関係をグラフへの所属として読む。添字の数項と候補の値との対が、ei に収められたグラフに属すという所属である。その存在証人は命題的に切り詰められているが、目標の所属は命題なので、ここでの除去によって必要な情報は失われない。qe に沿って輸送するとグラフは graph δ になり、lookup-spec はキー i での所属を、候補の値が δ の第 i項に等しいことと同一視する。符号化グラフのこの関数性が、項評価の変数の場合にほかならない。

tmIs-out (var i) δ γ vi ei qe h =
  subst ⟨_⟩ (lookup-spec (values δ) i ((lookup vi γ) .fst))
    (subst (λ w → ⟨ pr (# (toℕ i)) ((lookup vi γ) .fst) ∈ w ⟩) qe
      (tmIs-var-out i γ vi ei h))

逆向きの補題は、意味論的な値の等式から項述語の充足を構成する。定数の場合も直ちに従う。定数を改名した後に対象言語の等式が要求するのは、仮定として与えられた等式そのものである。tmIs-out と tmIs-in を合わせると、項の値をどちらの向きにも読める。原子の節ではこの二つの補題で評価済みの二項を比較し、有界量化子の節では限界項の値を読む。

tmIs-in : ∀ {n k} (t : Term DB.SM n) (δ : Vec DB.SM n) (γ : Vec S k) (vi ei : Fin k)
        → (lookup ei γ) .fst ≡ graph δ
        → (lookup vi γ) .fst ≡ (⟦ t ⟧ᴮ δ) .fst
        → ⟨ γ ⊨ tmIs (mapTm intoL t) vi ei ⟩
tmIs-in (con c) δ γ vi ei qe q = q

変数の場合には、先ほどの議論を逆向きにたどる。lookup-spec が仮定された値の等式を、キー付きの対のgraph δ への所属に変える。次にグラフの等式を逆向きに用いて、その所属を ei に収められたグラフへ輸送し、tmIs-var-in が対象言語の述語の充足として包む。したがって二方向が表すのは同じ関数的グラフの事実であり、切り詰めから代表を選ぶことはない。

tmIs-in (var i) δ γ vi ei qe q = tmIs-var-in i γ vi ei
  (subst (λ w → ⟨ pr (# (toℕ i)) ((lookup vi γ) .fst) ∈ w ⟩) (sym qe)
    (subst ⟨_⟩ (sym (lookup-spec (values δ) i ((lookup vi γ) .fst))) q))

第二の一対の読み補題は、割当ての拡張を扱う。consAtL ei mi di では、スロット di が古いグラフを、mi が新しい先頭値を収め、ei が拡張後のグラフの候補になる。最初の二つのスロットがそれぞれ δ と x に対応しているなら、この述語の充足からei の基礎集合が graph (x ∷ δ) であることが従う。量化された論理式が、元の割当てから先頭に一項を加えた割当てへ移るときに必要なのがこの等式である。

consAtL-out : ∀ {n k} (δ : Vec DB.SM n) (x : DB.SM) (γ : Vec S k) (ei mi di : Fin k)
            → (lookup di γ) .fst ≡ graph δ
            → (lookup mi γ) .fst ≡ x .fst
            → ⟨ γ ⊨ consAtL ei mi di ⟩
            → (lookup ei γ) .fst ≡ graph (x ∷ δ)

証明はまず consAtL-adequate を使う。古いグラフについての仮定のもとで、このパスは拡張スロットの候補をenv (cons ((lookup mi γ) .fst) (values δ)) と同一視する。等式 qmがその先頭値を x .fst に置き換え、cons-values が得られた族をx ∷ δ の基礎の値の族と同一視する。最後に env の合同性を使えば、求めるグラフの等式が得られる。ここで妥当性の法則が与えるのは拡張グラフとの等式であって、そのグラフへの所属ではない。

consAtL-out δ x γ ei mi di qd qm h =
    subst ⟨_⟩ (consAtL-adequate ei mi di γ (values δ) qd) h
  ∙ cong env (cong (λ w → cons w (values δ)) qm ∙ cons-values x δ)

内向きの読みは三つの意味論的な等式を仮定する。古いスロットがgraph δ を、新しい値のスロットが x .fst を、拡張スロットの候補がgraph (x ∷ δ) を収めるという等式である。これらから consAtL の充足を構成する。この向きがあるため、各量化子の節は標準環境envFor (x ∷ δ) を証明済みの拡張として直接使える。存在表示から切り詰められていない環境を取り出す必要はない。

consAtL-in : ∀ {n k} (δ : Vec DB.SM n) (x : DB.SM) (γ : Vec S k) (ei mi di : Fin k)
           → (lookup di γ) .fst ≡ graph δ
           → (lookup mi γ) .fst ≡ x .fst
           → (lookup ei γ) .fst ≡ graph (x ∷ δ)
           → ⟨ γ ⊨ consAtL ei mi di ⟩

内向きの証明は、外向きの読みに使ったパスを逆にたどる。graph (x ∷ δ) についての等式から始め、cons-values の逆向きの等式と先頭の値の等式によって、その右辺を mi の値と古い値の族から作ったグラフへ書き換える。続いて妥当性のパスを逆向きに用い、この等式を consAtL の充足へ輸送する。したがって、各スロットを基礎集合の等式で固定すれば、対象言語の拡張述語と割当てを具体的に前置拡張する操作との間を双方向に移れる。

consAtL-in δ x γ ei mi di qd qm q =
  subst ⟨_⟩ (sym (consAtL-adequate ei mi di γ (values δ) qd))
    (q ∙ sym (cong env (cong (λ w → cons w (values δ)) qm ∙ cons-values x δ)))

再帰の値から内側の充足への帰納法

論理式に関する帰納法は、性質 Adequate によって組織される。制限構造の各割当て δ、周囲の各構成可能な要素 z、およびその基礎集合をgraph δ と同一視する各等式に対し、この性質は、定数を改名した論理式の充足関係集合への所属から、元の論理式が δ のもとで充足されることへのパスを与える。すべての z を量化するため、主張はグラフの特定の代表に依存しない。結論は二つの命題を比較し、左辺の mapFo intoL φ は制限された定数から周囲の構成可能な定数への必要な変更を記録する。

Adequate : ∀ {n} → Formula DB.SM n → Type (ℓ-suc (ℓ-suc ℓ))
Adequate {n} φ = (δ : Vec DB.SM n) (z : S) → z .fst ≡ graph δ
               → (z ∈ˢ Sat B (mapFo intoL φ)) ≡ (δ ⊨ᴮ φ)

偽は基底の場合であり、帰納仮定を必要としない。Sat-cond が環境集合についての論理積の項を取り除くと、⊥̇ の再帰条件は偽命題になる。⊥̇ の内側の意味論も同じ偽命題なので、残る比較は定義的に成り立つ。二つの意味論は、同一の充足不能な条件を課している。

step⊥ : ∀ {n} → Adequate {n} ⊥̇
step⊥ δ z q = Sat-cond ⊥̇ δ z q

論理積の場合、Sat-cond は二つの再帰的な部分条件の論理積を露わにする。二つの帰納仮定は、同じ割当てと同じグラフの代表のもとで、各部分条件から対応する内側の充足命題へのパスを与える。真理値の論理積_⊓_ の合同性を二つのパスに施せば、a ∧̇ b に必要なパスが得られる。再帰の節と内側の意味論が同じ命題結合子を使うため、証人を扱う必要はない。

step∧ : ∀ {n} (a b : Formula DB.SM n)
      → Adequate a → Adequate b → Adequate (a ∧̇ b)
step∧ a b ia ib δ z q = Sat-cond (mapFo intoL (a ∧̇ b)) δ z q
  ∙ cong₂ _⊓_ (ia δ z q) (ib δ z q)

論理和も同じ構造をもつ。その再帰条件は真理値の論理和 _⊔_ で二つの部分条件を結び、合同性が二つの帰納パスをこの結合子のもとへ運ぶ。ここでの演算は命題に作用する。証明が比較するのは二つの部分論理式の真理と、その論理和の真理であり、二つの充足関係集合の和集合を作るのではない。

step∨ : ∀ {n} (a b : Formula DB.SM n)
      → Adequate a → Adequate b → Adequate (a ∨̇ b)
step∨ a b ia ib δ z q = Sat-cond (mapFo intoL (a ∨̇ b)) δ z q
  ∙ cong₂ _⊔_ (ia δ z q) (ib δ z q)

含意で命題の場合がすべてそろう。再帰の節は真理値の含意 _⇒_ を使うため、二つの帰納パスに合同性を施すだけで、ここでも比較が得られる。したがって、偽と三つの二項結合子には特別な意味論的変換が要らない。環境の成分を取り除いた後では、それらの再帰条件がすでに内側の意味論と同じ論理的な形をしているからである。

step⇒ : ∀ {n} (a b : Formula DB.SM n)
      → Adequate a → Adequate b → Adequate (a ⇒̇ b)
step⇒ a b ia ib δ z q = Sat-cond (mapFo intoL (a ⇒̇ b)) δ z q
  ∙ cong₂ _⇒_ (ia δ z q) (ib δ z q)

原子論理式の再帰条件は項の値の候補を量化するため、先ほどの項の読み補題が必要である。所属の場合、その条件は命題的切り詰めのもとで、値 v と w、それらがそれぞれ t と u の評価を表すという証明、および v .fst からw .fst への所属を与える。内側の意味論は、実際の評価 T と U の間の所属を直接述べる。この二つの評価に局所的な名前を付けることで、論理的同値の両方向を明示できる。

step∈ : ∀ {n} (t u : Term DB.SM n) → Adequate (t ∈̇ u)
step∈ t u δ z q = Sat-cond (mapFo intoL (t ∈̇ u)) δ z q ∙ ⇔toPath fwd bwd
  where
  T = ⟦ t ⟧ᴮ δ
  U = ⟦ u ⟧ᴮ δ

順方向では、cond∈-out が切り詰められた候補を展開する。目標 T .fst ∈ U .fst は命題なので、rec₁ によって各候補の包みを調べられる。環境 w ∷ v ∷ z ∷ [] で tmIs-out を二度使うと、v は T と、w は U とそれぞれ同一視される。二変数の輸送subst2 が、記録された関係 v .fst ∈ w .fst を T .fst ∈ U .fst へ運ぶ。これがこの原子の内側の解釈そのものである。

  fwd : ⟨ (z ∷ []) ⊨ cond B (mapFo intoL (t ∈̇ u)) ⟩ → ⟨ T .fst ∈ U .fst ⟩
  fwd h = rec₁ ((T .fst ∈ U .fst) .snd)
    (λ { (v , (w , (ht , (hu , r)))) → subst2 (λ p s → ⟨ p ∈ s ⟩)
      (tmIs-out t δ (w ∷ v ∷ z ∷ []) (suc zero) (suc (suc zero)) q ht)
      (tmIs-out u δ (w ∷ v ∷ z ∷ []) zero (suc (suc zero)) q hu)

逆向きの含意では、意味論的な項の値そのものが候補になる。写像intoL は基礎集合を変えずに T と U を周囲の構成可能な要素として包むので、intoL T と intoL U を cond∈-in が要求する二つの証人として入れられる。これは与えられた評価からの直接の構成であり、選択原理を使ったり、命題的切り詰めから証人を取り出したりはしない。

      r })
    (cond∈-out B (mapTm intoL t) (mapTm intoL u) z h)
  bwd : ⟨ T .fst ∈ U .fst ⟩ → ⟨ (z ∷ []) ⊨ cond B (mapFo intoL (t ∈̇ u)) ⟩
  bwd r = cond∈-in B (mapTm intoL t) (mapTm intoL u) z
    ∣ intoL T , (intoL U

この二つの証人を定めると、tmIs-in の二つの呼び出しにはどちらもrefl を渡せる。intoL T の基礎集合は定義によって T .fst であり、U についても同様だからである。したがって、仮定された評価間の所属が、候補間に必要な関係になっている。この一式を命題的切り詰めへ入れると、逆向きの含意が閉じ、所属の原子についての妥当性が完成する。

    , ( tmIs-in t δ (intoL U ∷ intoL T ∷ z ∷ []) (suc zero) (suc (suc zero)) q refl
      , ( tmIs-in u δ (intoL U ∷ intoL T ∷ z ∷ []) zero (suc (suc zero)) q refl
        , r ))) ∣₁

等号の原子も同じ方針に従い、候補間の関係だけを等号に替える。再帰条件は命題的切り詰めのもとで、二つの項の値の候補、二つの項の読み、およびそれらの基礎集合の間のパスを与える。内側の意味論が直接要求するのはT .fst ≡ U .fst というパスである。所属の場合と同じく、⇔toPath は妥当性を、候補から評価へ輸送する順方向と、評価を候補として使う逆方向とに分ける。

step≐ : ∀ {n} (t u : Term DB.SM n) → Adequate (t ≐ u)
step≐ t u δ z q = Sat-cond (mapFo intoL (t ≐ u)) δ z q ∙ ⇔toPath fwd bwd
  where
  T = ⟦ t ⟧ᴮ δ
  U = ⟦ u ⟧ᴮ δ

累積階層の等号は命題なので、順方向の写像は切り詰めを除去できる。項の読みが ht : v .fst ≡ T .fst と hu : w .fst ≡ U .fst を与え、候補間の関係が r : v .fst ≡ w .fst であるとき、求めるパスの向きは正確にsym ht ∙ r ∙ hu である。すなわち、まず t の実際の評価からその候補へ逆向きに進み、記録された候補間の等号を渡り、最後に u の実際の評価へ順向きに進む。

  fwd : ⟨ (z ∷ []) ⊨ cond B (mapFo intoL (t ≐ u)) ⟩ → T .fst ≡ U .fst
  fwd h = rec₁ ((intoL T ≈ˢ intoL U) .snd)
    (λ { (v , (w , (ht , (hu , r)))) →
        sym (tmIs-out t δ (w ∷ v ∷ z ∷ []) (suc zero) (suc (suc zero)) q ht)
      ∙ r

逆向きの写像でも、intoL T と intoL U を周囲の証人として使う。内向きの項の読みによって二つの項述語が充足され、仮定されたパスT .fst ≡ U .fst が cond≐-in の要求する候補間の等号をそのまま与える。したがって、所属の原子と等号の原子との違いは、同じ二つの評価済み項の間にどの関係を運ぶかだけである。候補の値と切り詰めの扱いは一致する。

      ∙ tmIs-out u δ (w ∷ v ∷ z ∷ []) zero (suc (suc zero)) q hu })
    (cond≐-out B (mapTm intoL t) (mapTm intoL u) z h)
  bwd : T .fst ≡ U .fst → ⟨ (z ∷ []) ⊨ cond B (mapFo intoL (t ≐ u)) ⟩
  bwd r = cond≐-in B (mapTm intoL t) (mapTm intoL u) z
    ∣ intoL T , (intoL U

tmIs-in に渡す二つの値の等式は、ここでも refl である。証人として選んだのが、intoL で包んだ項の評価そのものだからである。仮定された等号が、切り詰められた条件へ入れる組を完成させる。これで論理式文法の二つの原子の葉について妥当性が得られた。残るのは量化子の場合であり、そこでの中心的な課題は、対象言語の拡張の証人を、内側の割当ての先頭に一つの要素を加える操作と対応させることである。

    , ( tmIs-in t δ (intoL U ∷ intoL T ∷ z ∷ []) (suc zero) (suc (suc zero)) q refl
      , ( tmIs-in u δ (intoL U ∷ intoL T ∷ z ∷ []) zero (suc (suc zero)) q refl
        , r ))) ∣₁

非有界の存在量化子について、対象言語の条件は命題的に切り詰められた一式のデータを含む。周囲の要素 x と、その基礎集合が B に属すという証明、拡張環境の候補 e、拡張述語の充足、および e の部分論理式の充足関係集合への所属である。内側の存在量化子は DB.SM 上を動き、その要素は集合とそのB への所属証明をすでに組にしている。この存在量化子自身も命題的に切り詰められている。したがって順方向では、特定の代表を保持せずに、外側の一式を内側の存在証人へ写せる。

step∃ : ∀ {n} (a : Formula DB.SM (suc n)) → Adequate a → Adequate (∃̇ a)
step∃ a ia δ z q = Sat-cond (mapFo intoL (∃̇ a)) δ z q ∙ ⇔toPath fwd bwd
  where
  fwd : ⟨ (z ∷ []) ⊨ cond B (mapFo intoL (∃̇ a)) ⟩ → ⟨ δ ⊨ᴮ (∃̇ a) ⟩
  fwd h = rec₁ squash₁

切り詰めの内側で、周囲の証人とその証明 x∈B を組にすると、制限された台の要素 (x .fst , x∈B) が得られる。非有界の量化変数に課される論域の制限はこれだけであり、限界項の値への所属という追加条件は有界量化子で初めて現れる。続いて consAtL-out は e を、具体的に拡張した割当て (x .fst , x∈B) ∷ δ のグラフと同一視する。帰納仮定が、記録された部分論理式の所属をこの割当てでの内側の充足へ輸送し、その値と証明の組が内側の存在量化の命題的切り詰めへ入れられる。

    (λ { (x , (x∈B , (e , (hc , he)))) → ∣ (x .fst , x∈B)
       , subst ⟨_⟩ (ia ((x .fst , x∈B) ∷ δ) e
           (consAtL-out δ (x .fst , x∈B) (e ∷ x ∷ z ∷ [])
             zero (suc zero) (suc (suc zero)) q refl hc)) he ∣₁ })
    (cond∃-out B (mapFo intoL a) z h)

存在量化の場合の逆向きの含意では、意味論的な証人は ∃[] の内部でのみ与えられる。そこで、この命題的切り詰めの上で構成を写す。証人 x はすでに制限された台の要素なので、第一成分が周囲の集合を与え、第二成分が B への所属を証明する。条件の側では intoL x を新しい値とし、拡張された割当て x ∷ δ の正準な環境 envFor (x ∷ δ) を環境の証人とする。

  bwd : ⟨ δ ⊨ᴮ (∃̇ a) ⟩ → ⟨ (z ∷ []) ⊨ cond B (mapFo intoL (∃̇ a)) ⟩
  bwd h = cond∃-in B (mapFo intoL a) z (map₁
    (λ { (x , ha) → intoL x , (x .snd , (envFor (x ∷ δ)
       , ( consAtL-in δ x (envFor (x ∷ δ) ∷ intoL x ∷ z ∷ [])
             zero (suc zero) (suc (suc zero)) q refl (envFor-graph (x ∷ δ))

consAtL の内向きの読みは、三つの等式からこの環境の拡張を証明する。古い環境は δ のグラフをもち、intoL x の基礎の値は x の基礎の値であり、新しい正準な環境は x ∷ δ のグラフをもつ。続いて帰納法の仮定を逆向きに読み、x ∷ δ での部分論理式の意味論的充足を、正準な環境が再帰的な部分の値に属することへ移す。証人の構成はすべて ∃[] の内部にとどまり、意味論的な証人を命題的切り詰めの外へ選び出すことはない。

         , subst ⟨_⟩ (sym (ia (x ∷ δ) (envFor (x ∷ δ))
             (envFor-graph (x ∷ δ)))) ha ))) })
    h)

全称量化の場合は証明の形が異なる。内側の ∀[] は、制限された台の任意の x に対して、部分論理式が x ∷ δ で成り立つことを示す関数であり、命題的切り詰めを含まない。Sat-cond が再帰的な条件を展開した後、正向きの含意は任意の x を取り、必要な証明を直接構成する。

step∀ : ∀ {n} (a : Formula DB.SM (suc n)) → Adequate a → Adequate (∀̇ a)
step∀ a ia δ z q = Sat-cond (mapFo intoL (∀̇ a)) δ z q ∙ ⇔toPath fwd bwd
  where
  fwd : ⟨ (z ∷ []) ⊨ cond B (mapFo intoL (∀̇ a)) ⟩ → ⟨ δ ⊨ᴮ (∀̇ a) ⟩
  fwd h x = subst ⟨_⟩ (ia (x ∷ δ) (envFor (x ∷ δ)) (envFor-graph (x ∷ δ)))

条件の全称の節を使うために、周囲での表示 intoL x、台への所属証明 x .snd、そして正準な拡張環境を与える。consAtL の内向きの読みは、この環境が実際に x の値を古いグラフの先頭に加えたものであることを示す。すると節から再帰的な部分の値への所属が得られ、帰納法の仮定がそれを内側の充足へ運ぶ。この非有界変数に課される唯一の制限は B への所属であり、その証明はすでに x : DB.SM の組に含まれている。

    (cond∀-out B (mapFo intoL a) z h (intoL x) (envFor (x ∷ δ)) (x .snd)
      (consAtL-in δ x (envFor (x ∷ δ) ∷ intoL x ∷ z ∷ [])
        zero (suc zero) (suc (suc zero)) q refl (envFor-graph (x ∷ δ))))
  bwd : ⟨ δ ⊨ᴮ (∀̇ a) ⟩ → ⟨ (z ∷ []) ⊨ cond B (mapFo intoL (∀̇ a)) ⟩
  bwd k = cond∀-in B (mapFo intoL a) z

逆に条件が要求するのは、B に属すると分かっている周囲の任意の x と、z の拡張であると証明された任意の環境に対する、部分の値への所属である。証明は (x .fst , x∈B) を制限された台の要素として組にし、与えられた内側の全称関数を適用する。consAtL の外向きの読みは、証明された環境を拡張された割当てのグラフと同定する。その等式に沿って帰納法の仮定を逆向きに読めば、必要な部分の値への所属が得られる。この向きは終始点ごとの議論であり、命題的切り詰めを使わない。

    (λ x e x∈B hc → subst ⟨_⟩
      (sym (ia ((x .fst , x∈B) ∷ δ) e
        (consAtL-out δ (x .fst , x∈B) (e ∷ x ∷ z ∷ [])
          zero (suc zero) (suc (suc zero)) q refl hc)))
      (k (x .fst , x∈B)))

有界存在量化では、非有界の場合の議論に限界項の評価が加わる。T = ⟦ t ⟧ᴮ δ を、制限された構造におけるその項の真の値とする。内側の意味論は ∃[] の下で x : DB.SM を探し、x の基礎集合が T の基礎集合に属することと、部分論理式が x ∷ δ で充足されることを同時に要求する。したがって、台への所属と限界への所属は別々の証拠として保たれる。

step∃∈ : ∀ {n} (t : Term DB.SM n) (a : Formula DB.SM (suc n))
       → Adequate a → Adequate (∃̇∈ t a)
step∃∈ t a ia δ z q = Sat-cond (mapFo intoL (∃̇∈ t a)) δ z q ∙ ⇔toPath fwd bwd
  where
  T = ⟦ t ⟧ᴮ δ

正向きの含意では、有界な条件はまず外側の切り詰めの下で、項の値を表す述語を満たす候補 w を与える。第二の切り詰められた組は、周囲の要素 x、x が B と w に属する証明、拡張環境 e、そして e での部分条件を与える。外側の切り詰めは命題値である意味論的な目標へ除去し、内側の切り詰めは意味論的な存在証人 (x .fst , x∈B) へ写す。

  fwd : ⟨ (z ∷ []) ⊨ cond B (mapFo intoL (∃̇∈ t a)) ⟩ → ⟨ δ ⊨ᴮ (∃̇∈ t a) ⟩
  fwd h = rec₁ squash₁
    (λ { (w , (hw , hb)) → map₁
      (λ { (x , ((x∈B , x∈w) , (e , (hc , he)))) → (x .fst , x∈B)
         , ( subst (λ s → ⟨ x .fst ∈ s ⟩)

項の読み tmIs-out は、候補 w の基礎集合を意味論的な値 T の基礎集合と同定する。そのパスに沿って輸送すると、x∈w は内側の意味論が要求する限界への所属、すなわち x .fst ∈ T .fst になる。一方、consAtL-out は e を (x .fst , x∈B) ∷ δ のグラフと同定するので、帰納法の仮定によって e での部分条件を拡張された割当てでの充足へ移せる。この二つの結果が内側の ∃[] の中身になる。

               (tmIs-out t δ (w ∷ z ∷ []) zero (suc zero) q hw) x∈w
           , subst ⟨_⟩ (ia ((x .fst , x∈B) ∷ δ) e
               (consAtL-out δ (x .fst , x∈B) (e ∷ x ∷ w ∷ z ∷ [])
                 zero (suc zero) (suc (suc (suc zero))) q refl hc)) he ) })
      hb })

逆向きの含意では、真の値 T そのものを条件側の限界の候補として用いる。反射的な値の等式とともに tmIs-in を使えば、その項の値を表す述語が得られる。次に意味論的な ∃[] の上で写すと、残る仕事は各意味論的証人 x を組み直すことだけになる。条件の内側の存在は命題的に切り詰められたままである。

    (cond∃∈-out B (mapTm intoL t) (mapFo intoL a) z h)
  bwd : ⟨ δ ⊨ᴮ (∃̇∈ t a) ⟩ → ⟨ (z ∷ []) ⊨ cond B (mapFo intoL (∃̇∈ t a)) ⟩
  bwd h = cond∃∈-in B (mapTm intoL t) (mapFo intoL a) z (map₁
    (λ { (x , (hx , ha)) → intoL T
       , ( tmIs-in t δ (intoL T ∷ z ∷ []) zero (suc zero) q refl

意味論的証人 x : DB.SM は二つの制限を別々に与える。x .snd は台への所属を証明し、hx は限界 T への所属を証明する。選んだ候補は実際に intoL T なので、hx はそのまま使える。拡張環境として envFor (x ∷ δ) を選び、consAtL-in でそれを証明し、帰納法の仮定を逆向きに読んで再帰的な部分の値への所属を得る。

         , ∣ intoL x , ((x .snd , hx) , (envFor (x ∷ δ)
           , ( consAtL-in δ x (envFor (x ∷ δ) ∷ intoL x ∷ intoL T ∷ z ∷ [])
                 zero (suc zero) (suc (suc (suc zero))) q refl
                 (envFor-graph (x ∷ δ))
             , subst ⟨_⟩ (sym (ia (x ∷ δ) (envFor (x ∷ δ))

これで有界存在量化の両方向が完成する。非有界存在量化に加わった数学的な仕事は、限界項の値を名づけることと、符号化された候補と意味論的な値の間で一つの所属証明を輸送することだけである。二つの存在の組はどちらも命題的切り詰めの下にとどまるため、選択原理は導入されない。排中律のパラメータはすでに Sat の構成に現れており、この妥当性の段階で新たな古典的仮定は加わらない。

                 (envFor-graph (x ∷ δ)))) ha ))) ∣₁ ) })
    h)

有界全称量化は最後の構成子の場合である。T = ⟦ t ⟧ᴮ δ とすると、その内側の意味は、任意の x : DB.SM と証明 x .fst ∈ T .fst を受け取り、部分論理式が x ∷ δ で充足されることを返す関数である。非有界全称量化の場合と同じく、どちらの向きにも存在の組はないため、二つの含意は命題的切り詰めを使わず点ごとに構成される。

step∀∈ : ∀ {n} (t : Term DB.SM n) (a : Formula DB.SM (suc n))
       → Adequate a → Adequate (∀̇∈ t a)
step∀∈ t a ia δ z q = Sat-cond (mapFo intoL (∀̇∈ t a)) δ z q ∙ ⇔toPath fwd bwd
  where
  T = ⟦ t ⟧ᴮ δ

正向きの関数を作るには、x とその意味論的な限界への所属証明 hx を取る。条件の全称の節では、真の限界値 intoL T を使い、その項の読みを tmIs-in から得る。変数には周囲での表示 intoL x を使う。二つの制限は異なる所から来る。x .snd が x ∈ B を記録し、hx が x .fst ∈ T .fst を記録する。consAtL-in が正準な拡張を証明し、帰納法の仮定が得られた部分の値への所属を内側の充足へ移す。

  fwd : ⟨ (z ∷ []) ⊨ cond B (mapFo intoL (∀̇∈ t a)) ⟩ → ⟨ δ ⊨ᴮ (∀̇∈ t a) ⟩
  fwd h x hx = subst ⟨_⟩ (ia (x ∷ δ) (envFor (x ∷ δ)) (envFor-graph (x ∷ δ)))
    (cond∀∈-out B (mapTm intoL t) (mapFo intoL a) z h (intoL T)
      (tmIs-in t δ (intoL T ∷ z ∷ []) zero (suc zero) q refl)
      (intoL x) (envFor (x ∷ δ)) (x .snd) hx

逆向きの関数では、条件は任意の限界候補 w、それが項の値として読めることを示す hw、x∈B と x∈w を伴う周囲の要素 x、そして証明された拡張 e のすべてについて量化する。項の外向きの読みは w の基礎集合を T .fst と同定する。このパスに沿って x∈w を輸送すれば、内側の全称関数を (x .fst , x∈B) に適用するための限界への所属証明がちょうど得られる。

      (consAtL-in δ x (envFor (x ∷ δ) ∷ intoL x ∷ intoL T ∷ z ∷ [])
        zero (suc zero) (suc (suc (suc zero))) q refl (envFor-graph (x ∷ δ))))
  bwd : ⟨ δ ⊨ᴮ (∀̇∈ t a) ⟩ → ⟨ (z ∷ []) ⊨ cond B (mapFo intoL (∀̇∈ t a)) ⟩
  bwd k = cond∀∈-in B (mapTm intoL t) (mapFo intoL a) z
    (λ w hw x e x∈B x∈w hc → subst ⟨_⟩

内側の全称関数を適用すると、部分論理式が (x .fst , x∈B) ∷ δ で充足されることが得られる。consAtL の外向きの読みは、証明された環境 e をまさにこの割当てのグラフと同定する。したがって帰納法のパスを逆向きに読めば、意味論的充足を条件が要求する部分の値への所属へ移せる。これで有界全称量化の場合が閉じ、台への制限と限界への制限を区別したまま、四つの量化子の議論がすべて完成する。

      (sym (ia ((x .fst , x∈B) ∷ δ) e
        (consAtL-out δ (x .fst , x∈B) (e ∷ x ∷ w ∷ z ∷ [])
          zero (suc zero) (suc (suc (suc zero))) q refl hc)))
      (k (x .fst , x∈B) (subst (λ s → ⟨ x .fst ∈ s ⟩)
        (tmIs-out t δ (w ∷ z ∷ []) zero (suc zero) q hw) x∈w)))

個々の場合を論理式の構造に沿って再帰させ、Sat-spec にまとめる。その帰納的不変条件は正確である。任意の割当て δ、任意の周囲の要素 z、そして z .fst から graph δ への任意のパスについて、z が Sat B (mapFo intoL φ) に属することと、内側で δ ⊨ᴮ φ が成り立つことは同じ命題である。最初の四つの節は二つの原子の場合を選び、連言と選言について帰納的に得たパスを組み合わせる。

Sat-spec : ∀ {n} (φ : Formula DB.SM n) → Adequate φ
Sat-spec (t ∈̇ u)  = step∈ t u
Sat-spec (t ≐ u)  = step≐ t u
Sat-spec (a ∧̇ b)  = step∧ a b (Sat-spec a) (Sat-spec b)
Sat-spec (a ∨̇ b)  = step∨ a b (Sat-spec a) (Sat-spec b)

再帰は含意と偽へ進み、続いて二つの非有界量化子と有界全称量化を扱う。複合した構成子が受け取るのは、直接の部分論理式に対する妥当性の証明だけであり、偽の場合には帰納法の仮定は要らない。したがって帰納法の仮定は毎回、その構文の枝における再帰的な条件と内側の意味論を比較するためだけに使われる。

Sat-spec (a ⇒̇ b)  = step⇒ a b (Sat-spec a) (Sat-spec b)
Sat-spec ⊥̇        = step⊥
Sat-spec (∃̇ a)    = step∃ a (Sat-spec a)
Sat-spec (∀̇ a)    = step∀ a (Sat-spec a)
Sat-spec (∀̇∈ t a) = step∀∈ t a (Sat-spec a)

有界存在量化の節によって十の場合の再帰が閉じる。したがって Sat-spec は、定数が制限された台に属する任意の論理式について妥当性を証明する。ここで mapFo intoL はそれらの定数を周囲の言語へ移す。この定理は、外側で構成された各値 Sat B φ に意味論的な読みを与えるが、一様な充足関係表を構成することも、候補の表の一意性を証明することもない。SatisfactionGraph が候補となるグラフ関係を記述し、PinnedRecursion が必要なキーごとの一意性を証明する。UniformSatisfaction は存在とこの一意性を組み合わせて一様な表を構成し、その後で Sat-spec を使って各値を解釈する。

Sat-spec (∃̇∈ t a) = step∃∈ t a (Sat-spec a)

環境から割当てを復元する

主定理は、あらかじめ選ばれた割当てから出発する。環境集合の任意の要素を読むには、まずその符号化に使われる小さな添字を、制限された台の要素へ変換する。m : ⟪ B .fst ⟫ に対して、表示写像は基礎集合 ⟪ B .fst ⟫↪ m を与える。表示における所属の二つの読みから、この集合が B .fst に属することが分かる。集合とその証明を組にしたものが inB m : DB.SM である。

private
  inB : (m : ⟪ B .fst ⟫) → ⟨ ⟪ B .fst ⟫↪ m ∈ B .fst ⟩
  inB m = ∈∈ₛ {a = ⟪ B .fst ⟫↪ m} {b = B .fst} .snd (∈ₛ⟪ B .fst ⟫↪ m)

添字族 g : Ix B n は、有限な各位置に小さな要素の添字を一つずつもつ。関数 tab は n に関する再帰によって、これを Vec DB.SM n の割当てへ変える。先頭は g zero が表示する集合に inB (g zero) を添えたものであり、尾はずらした族 λ i → g (suc i) から得られる。したがって各項目の順序は正確に保たれる。

  tab : ∀ {n} → Ix B n → Vec DB.SM n
  tab {0} g = []
  tab {suc n} g = (⟪ B .fst ⟫↪ (g zero) , inB (g zero)) ∷ tab (λ i → g (suc i))

最初の整合性の等式は、tab g から台への所属証明を忘れると、g が表示する集合の族がそのまま得られることを述べる。位置 zero では反射的に成り立ち、後続の位置では、ずらした尾に対する再帰的な等式から従う。関数外延性がこれらの点ごとの等式をまとめ、値の族全体の等式 tab-values を与える。

  tab-values : ∀ {n} (g : Ix B n) → values (tab g) ≡ (λ i → ⟪ B .fst ⟫↪ (g i))
  tab-values {0} g = funExt (λ ())
  tab-values {suc n} g = funExt
    (λ { zero → refl
       ; (suc i) → funExt⁻ (tab-values (λ j → g (suc j))) i })

グラフを作る演算 env を tab-values に施すと、第二の整合性の等式が得られる。これは graph (tab g) を、正準な符号化環境 envS B g の基礎集合と同定する。したがって envSet が使う添字表示と、内側の意味論が使う制限された台の割当ては、項目に異なる補助データを伴いながらも、同じ有限グラフを記述する。

  tab-graph : ∀ {n} (g : Ix B n) → graph (tab g) ≡ (envS B g) .fst
  tab-graph g = cong env (tab-values g)

envSet の外向きの仕様は、要素 z から命題的切り詰めの下で添字族 g と、z .fst から envS B g の基礎集合へのパスを復元する。g を tab g へ写し、そのパスを tab-graph の逆向きと合成すると、z .fst ≡ graph δ を満たす割当て δ が得られる。結果は切り詰めの下にとどまり、大域的に選ばれた復号も一意性の主張も与えない。後の節の意味論で任意の符号化環境を扱うときにも、まさにこの制限されたインターフェースが使われる。

envSet-vectors : ∀ {n} (z : S) → ⟨ z ∈ˢ envSet B n ⟩
               → ∥ Σ[ δ ∶ Vec DB.SM n ] (z .fst ≡ graph δ) ∥₁
envSet-vectors {n} z h = map₁
  (λ { (g , qg) → tab g , qg ∙ sym (tab-graph g) }) (envSet-out B n z h)

Sat-spec は、特定の割当てとグラフの等式から出発する。Sat-out は、充足の値の任意の要素 z に対応する主張を与える。すなわち ∃[] のもとで、グラフが z .fst であり、制限構造でその論理式を充足する割当て δ が存在する。命題的切り詰めは結論そのものの一部なので、この定理は復号する割当てを選び出さず、そのような割当ての一意性も証明しない。主張するのは、Sat への所属から充足する表示の存在へ進む向きだけである。

Sat-out : ∀ {n} (φ : Formula DB.SM n) (z : S)
        → ⟨ z ∈ˢ Sat B (mapFo intoL φ) ⟩
        → ∥ (Σ[ δ ∶ Vec DB.SM n ] ((z .fst ≡ graph δ) × ⟨ δ ⊨ᴮ φ ⟩)) ∥₁
Sat-out {n} φ z h = map₁
  (λ { (g , qg) → tab g , (qg ∙ sym (tab-graph g)

最後の二行は、復元されたデータの論理的な強さを増すことなく、外向きの読みを完成させる。もとの Sat への所属証明から、Sat-mem が取り出すのは z が環境集合に属するという成分だけである。続いて envSet-out は、命題的切り詰めの中で添字族 g とそのグラフ等式を返す。map₁ の内部では、tab g が対応する内側の割当てであり、qg ∙ sym (tab-graph g) が z の基礎集合をその割当てのグラフと同一視する。この等式を固定すると、Sat-spec はもとの所属証明 h を直接、内側の充足へ運ぶ。したがって割当てとその充足証明は同じ切り詰めの中にとどまり、選択も一意性も主張されない。

     , subst ⟨_⟩ (Sat-spec φ (tab g) z (qg ∙ sym (tab-graph g))) h) })
  (envSet-out B n z (subst ⟨_⟩ (Sat-mem B (mapFo intoL φ) z) h .fst))

定義可能部分集合との一致

この再帰を定義可能部分集合と比較するには、定数を三つの領域の間で移す必要がある。論理式 ψ の定数は、初めは小さな提示 ⟪ B .fst ⟫ に属する。DB.ι はそれらを制限された台へ送り、続いて intoL がその台の要素を周囲の台 S へ送る。定義により、この合成が asConst である。したがって mapFo-comp が表す定数の改名の関手性により、二度改名した論理式 mapFo intoL (mapFo DB.ι ψ) は、直接改名した論理式 mapFo asConst ψ と同一視される。これは論理式の等式であり、意味論の橋を、再帰が要求する定数の形で使えるようにする。

private
  mapFo-fuse : ∀ {n} (ψ : Formula ⟪ B .fst ⟫ n)
             → mapFo intoL (mapFo DB.ι ψ) ≡ mapFo asConst ψ
  mapFo-fuse = mapFo-comp DB.ι intoL

第二の正規化は、定義可能部分集合で用いる一項目の割当てに関するものである。正準な環境 envS B (λ _ → m) は、値が常に m である添字族から作られ、その基礎集合はベクトル DB.ι m ∷ [] のグラフである。長さ一の族には添字 zero しかないため、二つのグラフの値の族は一致する。関数外延性がこの添字を確認し、後続の場合は不可能である。さらに合同性がその等式をグラフ演算へ運ぶ。こうして、この具体的な環境は Sat-spec が必要とするグラフの仮定を満たす。

  graph-single : (m : ⟪ B .fst ⟫)
               → (envS B (λ _ → m)) .fst ≡ graph (DB.ι m ∷ [])
  graph-single m = cong env (funExt (λ { zero → refl ; (suc ()) }))

この二つの正規化から、小さな定数アルファベットにおける橋が得られる。z の基礎集合が内側の割当て δ のグラフに等しいとする。このとき、mapFo asConst ψ に対する再帰の値への z の所属は、δ における mapFo DB.ι ψ の内側の充足と等しくなる。右辺の論理式は制限された台に定数を持ち、その構造で恒等写像を解釈として評価される。言い換えれば、もとの小さな論理式の定数を DB.ι で解釈したものである。証明はまず mapFo-fuse を逆向きに使って左辺に二段の定数の改名を現し、次に Sat-spec を適用する。これにより、下で自由変数が一つの場合へ特殊化する前に、任意のアリティに対する小さなアルファベットでの橋が得られる。

Sat-small-spec : ∀ {n} (ψ : Formula ⟪ B .fst ⟫ n) (δ : Vec DB.SM n) (z : S)
               → z .fst ≡ graph δ
               → (z ∈ˢ Sat B (mapFo asConst ψ)) ≡ (δ ⊨ᴮ mapFo DB.ι ψ)
Sat-small-spec ψ δ z q = cong (λ χ → z ∈ˢ Sat B χ) (sym (mapFo-fuse ψ))
  ∙ Sat-spec (mapFo DB.ι ψ) δ z q

ここで自由変数が一つの場合に特殊化する。小さな論理式 ψ と提示の添字 m に対し、defSet-Sat は二つの命題を比較する。m が名指す集合が定義可能部分集合 DB.defSet ψ に属することと、m に対する正準な一項目の環境が mapFo asConst ψ の再帰的な充足関係の値に属することである。証明の最初のパスは DB.defSet-mem である。これは定義可能部分集合の意味を展開し、前者の所属命題を、定数を DB.ι で解釈した ψ の、割当て DB.ι m ∷ [] における内側の充足へ変える。

defSet-Sat : (ψ : Formula ⟪ B .fst ⟫ 1) (m : ⟪ B .fst ⟫)
           → (⟪ B .fst ⟫↪ m ∈ DB.defSet ψ)
           ≡ (envS B (λ _ → m) ∈ˢ Sat B (mapFo asConst ψ))
defSet-Sat ψ m =
    DB.defSet-mem ψ m

さらに三つのパスをつなぐと、主張された再帰の値に到達する。まず ⊨-map を逆向きに使い、定数を DB.ι で解釈した ψ の充足を、恒等解釈のもとで改名された論理式 mapFo DB.ι ψ の充足へ置き換える。次に graph-single を用いて Sat-spec を逆向きにたどり、その内側の充足を Sat B (mapFo intoL (mapFo DB.ι ψ)) への所属へ変える。最後に mapFo-fuse に沿う合同性により、二度改名された論理式を mapFo asConst ψ に置き換える。各段階は真理値の間のパスである。割当てとそのグラフは明示的に与えられているため、割当ての復元も命題的切り詰めも用いない。この結果が、定義可能冪集合の構成から再帰的な充足関係の値を読むための、一変数のインターフェースになる。

  ∙ sym (⊨-map DB.𝒮M DB.ι id ψ (DB.ι m ∷ []))
  ∙ sym (Sat-spec (mapFo DB.ι ψ) (DB.ι m ∷ []) (envS B (λ _ → m))
           (graph-single m))
  ∙ cong (λ χ → envS B (λ _ → m) ∈ˢ Sat B χ) (mapFo-fuse ψ)

まとめ

中心的な結果 Sat-spec は、与えられた各割当てについて、再帰的に構成された値への所属を内側の充足と同定する。z .fst ≡ graph δ ならば、z が Sat B (mapFo intoL φ) に属することと δ ⊨ᴮ φ は同じ命題である。入力が充足の値の任意の符号化された要素である場合、Sat-out は必要なグラフの等式と充足の証明を備えた割当てを ∃[] のもとで与えるだけである。その割当てを選び出すことも、一意性を証明することもない。小さな表示の定数を DB.ι、intoL の順に取り替えると、Sat-small-spec が任意のアリティで橋を与え、defSet-Sat はそれを自由変数が一つの場合に特殊化して、定義可能部分集合への所属を正準な一項目環境の所属と同定する。一様な表の構成と候補表の値の一意性には、後の固定された再帰と一様な充足関係の議論が必要である。