---
title: "充足関係と再帰の値"
module: L.Coding.SatisfactionBridge
lang: ja
site: "Bedrock"
description: "充足関係と再帰の値"
stage: "内部の符号化：表と一様な充足関係"
reading_order: 50
canonical: https://bedrock.institute/ja/L.Coding.SatisfactionBridge.html
html: L.Coding.SatisfactionBridge.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/Coding/SatisfactionBridge.lagda.md
prerequisites: [Base.Prelude, Base.Classical, FOL.ZFStructure, FOL.Syntax, FOL.Manipulation.ConstantMapping, FOL.Manipulation.Relabelling, FOL.Absoluteness, FOL.Semantics, V.Hierarchy, V.Coding, L.Constructible, L.Definability, L.Coding.Environment, L.Coding.Expressions, L.Coding.EnvironmentSet, L.Coding.Satisfaction]
routes: [internal-satisfaction]
translations: [https://bedrock.institute/en/L.Coding.SatisfactionBridge.md, https://bedrock.institute/zh/L.Coding.SatisfactionBridge.md]
agent_guide: https://bedrock.institute/llms.txt
license: "CC-BY-NC-SA-4.0"
---


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

# 充足関係と再帰の値

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

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

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

```agda
open import FOL.ZFStructure using ( module hPropView )
open import FOL.Syntax
  using ( Term; con; var; Formula
        ; _∈̇_; _≐_; _∧̇_; _∨̇_; _⇒̇_; ⊥̇; ∃̇_; ∀̇_; ∀̇∈; ∃̇∈ )
open import FOL.Manipulation.ConstantMapping using ( mapTm; mapFo; mapFo-comp )
open import FOL.Manipulation.Relabelling using ( ⊨-map )
import FOL.Absoluteness
import FOL.Semantics
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ )
open import V.Coding {ℓ} using ( pr )
open import L.Constructible {ℓ} using ( 𝒮ʟ; isL; isL-trans )
open import L.Definability {ℓ} using ( module DefOf )
open import L.Coding.Environment {ℓ} using ( env; cons; lookup-spec )
open import L.Coding.Expressions {ℓ} using ( consAtL; consAtL-adequate )
open import L.Coding.EnvironmentSet {ℓ} lem
  using ( Ix; envS; envSet; envSet-in; envSet-out )
open import L.Coding.Satisfaction {ℓ} lem
  using ( tmIs; tmIs-var-in; tmIs-var-out; cond; Sat; Sat-mem
        ; cond∈-in; cond∈-out; cond≐-in; cond≐-out
        ; cond∃-in; cond∃-out; cond∀-in; cond∀-out
        ; cond∃∈-in; cond∃∈-out; cond∀∈-in; cond∀∈-out )
```

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

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

```agda
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` への所属証明をすでに含み、そこから添字族を直接得られるからである。

```agda
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)` によって記録される。ここで数項の構成子を導入することで、項の変数が使う有限添字と、符号化された環境が使う集合論的なキーとが結ばれる。

```agda
open InfinitySet using ( #_ )
```

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

```agda
open hPropView 𝒮ʟ
```

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

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

## 台上の制限構造

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

<details open class="submodule-fold">
<summary class="submodule-fold-heading">

```agda
module _ (B : S) where
```

</summary>
<div class="submodule-fold-content">

```agda
  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` が所属について閉じているとは仮定しない。

```agda
  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` は異なる役割をもつが、その合成は名指された集合を変えない。

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

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

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

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

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

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

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

```agda
  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` を得る。この構成はベクトルにすでに保存された所属の証拠を直接使うため、命題的切り詰めも、符号化されたグラフから回復した代表の選択も含まない。

```agda
    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 δ` は各点で一致し、有限グラフを比較するための正確な入力が得られる。

```agda
    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 δ` が得られる。これは具体的なベクトル `δ` に対応する、階層における正準な符号である。続く二つの事実が、その基礎のグラフを同定し、さらに環境集合への所属を証明する。任意の環境の代表を選んではいない。

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

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

```agda
  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` が回復する添字族は命題的切り詰めの中にあり、後の構成がそれをベクトルへ変換するときも切り詰めを保つ。この回復は論理式に関する帰納法の外に置かれる。

```agda
  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` はまだ論理式の意味を説明せず、次の帰納法で解釈すべき再帰条件だけを取り出す。

```agda
  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` による定数の改名は台の包装だけを変え、基礎集合はその定数の値のままである。

```agda
  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`項に等しいことと同一視する。符号化グラフのこの関数性が、項評価の変数の場合にほかならない。

```agda
  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` を合わせると、項の値をどちらの向きにも読める。原子の節ではこの二つの補題で評価済みの二項を比較し、有界量化子の節では限界項の値を読む。

```agda
  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` が対象言語の述語の充足として包む。したがって二方向が表すのは同じ関数的グラフの事実であり、切り詰めから代表を選ぶことはない。

```agda
  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 ∷ δ)` であることが従う。量化された論理式が、元の割当てから先頭に一項を加えた割当てへ移るときに必要なのがこの等式である。

```agda
  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` の合同性を使えば、求めるグラフの等式が得られる。ここで妥当性の法則が与えるのは拡張グラフとの等式であって、そのグラフへの所属ではない。

```agda
  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 ∷ δ)` を証明済みの拡張として直接使える。存在表示から切り詰められていない環境を取り出す必要はない。

```agda
  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` の充足へ輸送する。したがって、各スロットを基礎集合の等式で固定すれば、対象言語の拡張述語と割当てを具体的に前置拡張する操作との間を双方向に移れる。

```agda
  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 φ` は制限された定数から周囲の構成可能な定数への必要な変更を記録する。

```agda
  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` が環境集合についての論理積の項を取り除くと、`⊥̇` の再帰条件は偽命題になる。`⊥̇` の内側の意味論も同じ偽命題なので、残る比較は定義的に成り立つ。二つの意味論は、同一の充足不能な条件を課している。

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

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

```agda
  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)
```

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

```agda
  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)
```

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

```agda
  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` の間の所属を直接述べる。この二つの評価に局所的な名前を付けることで、論理的同値の両方向を明示できる。

```agda
  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` へ運ぶ。これがこの原子の内側の解釈そのものである。

```agda
    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` が要求する二つの証人として入れられる。これは与えられた評価からの直接の構成であり、選択原理を使ったり、命題的切り詰めから証人を取り出したりはしない。

```agda
        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` についても同様だからである。したがって、仮定された評価間の所属が、候補間に必要な関係になっている。この一式を命題的切り詰めへ入れると、逆向きの含意が閉じ、所属の原子についての妥当性が完成する。

```agda
      , ( 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` は妥当性を、候補から評価へ輸送する順方向と、評価を候補として使う逆方向とに分ける。

```agda
  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` の実際の評価へ順向きに進む。

```agda
    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` の要求する候補間の等号をそのまま与える。したがって、所属の原子と等号の原子との違いは、同じ二つの評価済み項の間にどの関係を運ぶかだけである。候補の値と切り詰めの扱いは一致する。

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

```agda
      , ( 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` への所属証明をすでに組にしている。この存在量化子自身も命題的に切り詰められている。したがって順方向では、特定の代表を保持せずに、外側の一式を内側の存在証人へ写せる。

```agda
  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) ∷ δ` のグラフと同一視する。帰納仮定が、記録された部分論理式の所属をこの割当てでの内側の充足へ輸送し、その値と証明の組が内側の存在量化の命題的切り詰めへ入れられる。

```agda
      (λ { (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 ∷ δ)` を環境の証人とする。

```agda
    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 ∷ δ` での部分論理式の意味論的充足を、正準な環境が再帰的な部分の値に属することへ移す。証人の構成はすべて `∃[]` の内部にとどまり、意味論的な証人を命題的切り詰めの外へ選び出すことはない。

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

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

```agda
  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` の組に含まれている。

```agda
      (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` の外向きの読みは、証明された環境を拡張された割当てのグラフと同定する。その等式に沿って帰納法の仮定を逆向きに読めば、必要な部分の値への所属が得られる。この向きは終始点ごとの議論であり、命題的切り詰めを使わない。

```agda
      (λ 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 ∷ δ` で充足されることを同時に要求する。したがって、台への所属と限界への所属は別々の証拠として保たれる。

```agda
  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)` へ写す。

```agda
    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` での部分条件を拡張された割当てでの充足へ移せる。この二つの結果が内側の `∃[]` の中身になる。

```agda
                 (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` を組み直すことだけになる。条件の内側の存在は命題的に切り詰められたままである。

```agda
      (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` でそれを証明し、帰納法の仮定を逆向きに読んで再帰的な部分の値への所属を得る。

```agda
           , ∣ 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` の構成に現れており、この妥当性の段階で新たな古典的仮定は加わらない。

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

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

```agda
  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` が正準な拡張を証明し、帰納法の仮定が得られた部分の値への所属を内側の充足へ移す。

```agda
    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)` に適用するための限界への所属証明がちょうど得られる。

```agda
        (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` をまさにこの割当てのグラフと同定する。したがって帰納法のパスを逆向きに読めば、意味論的充足を条件が要求する部分の値への所属へ移せる。これで有界全称量化の場合が閉じ、台への制限と限界への制限を区別したまま、四つの量化子の議論がすべて完成する。

```agda
        (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 φ)` に属することと、内側で `δ ⊨ᴮ φ` が成り立つことは同じ命題である。最初の四つの節は二つの原子の場合を選び、連言と選言について帰納的に得たパスを組み合わせる。

```agda
  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)
```

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

```agda
  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` を使って各値を解釈する。

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

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

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

```agda
  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)` から得られる。したがって各項目の順序は正確に保たれる。

```agda
    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` を与える。

```agda
    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` が使う添字表示と、内側の意味論が使う制限された台の割当ては、項目に異なる補助データを伴いながらも、同じ有限グラフを記述する。

```agda
    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 δ` を満たす割当て `δ` が得られる。結果は切り詰めの下にとどまり、大域的に選ばれた復号も一意性の主張も与えない。後の節の意味論で任意の符号化環境を扱うときにも、まさにこの制限されたインターフェースが使われる。

```agda
  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` への所属から充足する表示の存在へ進む向きだけである。

```agda
  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` を直接、内側の充足へ運ぶ。したがって割当てとその充足証明は同じ切り詰めの中にとどまり、選択も一意性も主張されない。

```agda
       , 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 ψ` と同一視される。これは論理式の等式であり、意味論の橋を、再帰が要求する定数の形で使えるようにする。

```agda
  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` が必要とするグラフの仮定を満たす。

```agda
    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` を適用する。これにより、下で自由変数が一つの場合へ特殊化する前に、任意のアリティに対する小さなアルファベットでの橋が得られる。

```agda
  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 ∷ []` における内側の充足へ変える。

```agda
  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 ψ` に置き換える。各段階は真理値の間のパスである。割当てとそのグラフは明示的に与えられているため、割当ての復元も命題的切り詰めも用いない。この結果が、定義可能冪集合の構成から再帰的な充足関係の値を読むための、一変数のインターフェースになる。

```agda
    ∙ 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 ψ)
```

</div>
</details>

## まとめ

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