---
title: "满足关系与递归取值"
module: L.Coding.SatisfactionBridge
lang: zh
site: "Bedrock"
description: "满足关系与递归取值"
stage: "内部编码：表与统一满足关系"
reading_order: 50
canonical: https://bedrock.institute/zh/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/ja/L.Coding.SatisfactionBridge.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
# 满足关系与递归取值

递归构造 `Sat` 为每条公式指定一个编码环境集，但只有把这些编码同 `B` 的成员结构中的真正赋值比较以后，那些递归方程才取得预期含义。这里的关键选择是采用该限制结构的内层语义：其中的量化变元已经遍历 `B`，而有界量词还另行要求变元属于界项的取值。

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

唯一显式的假设是层级 `ℓ-suc ℓ` 上的排中律。下文的公式归纳本身不对命题作分类讨论；这条假设经由已经构造好的环境集与满足集进入，而这些集合所用的分离运算以 `lem` 为参数。

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

证明沿公式的语法结构进行。公式有两个原子构造子、三个命题联结词、假、两个无界量词，以及两个受词项约束的有界量词，因此语义比较共有十种情形。词项与公式可分别通过 `mapTm` 和 `mapFo` 更换常元字母表，`mapFo-comp` 则说明连续两次更换等同于沿复合映射更换。由此，常元取自 `B` 的成员的公式可进入外围常元字母表，而其语法结构保持不变。

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

常元改名在语义上是精确的。若沿映射 `f` 更换常元，那么在解释 `ι` 下求值 `mapFo f φ`，所得真值与在复合解释 `ι ∘ f` 下求值 `φ` 相同；这正是 `⊨-map`。本章将在小成员索引、限制结构的元素与可构造集合之间转换时使用这条等式。外围层级及其有序对运算则提供构造编码环境所需的集合。

```agda
open import FOL.Manipulation.Relabelling using ( ⊨-map )
import FOL.Absoluteness
import FOL.Semantics
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ )
open import V.Coding {ℓ} using ( pr )
```

先前三项构造提供这座桥所用的数学数据。对集合 `B`，`DefOf` 给出限制到 `B` 中隶属的结构，以及在该结构中可定义的子集。环境编码以取值的图表示有穷赋值，并以在前端加入一个值表示扩张。最后，环境集构造收集固定元数的全部此类图。这里使用的传递性属于类 `L`：它使可构造集合的成员仍可视为可构造。它并不断言 `B` 本身是传递的。

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

编码一侧与语义一侧已经具备互补的接口。索引族给出典范图 `envS`，`envSet-in` 与 `envSet-out` 则把典范图同 `envSet` 的任意成员联系起来。集合 `Sat B φ` 随后从 `envSet B n` 中分离出满足递归条件 `cond B φ` 的那些图。公式 `tmIs` 表达词项取值关系，并带有变元情形的读式；关于原子公式与无界量词的导入读式则在两个方向上翻译相应子句。这些陈述只解释 `cond`；属于 `envSet` 的附加要求仍是 `Sat-mem` 中独立的一项。

```agda
  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` 的每一条非命题子句。有界子句始终区分两重限制：新值必须属于载体 `B`，也必须属于界项的取值。后面的归纳会把它们分别对应到限制结构的论域与内层语义中的界。

```agda
        ; cond∃∈-in; cond∃∈-out; cond∀∈-in; cond∀∈-out )
```

证明以路径比较命题值陈述。`⇔toPath` 把命题之间的双向蕴涵变为这样的路径，随后同余便可把比较带过各逻辑构造子。在隶属原子情形，两个候选词项值都与各自的语义取值相认同后，`subst2` 沿这两条等式运输隶属关系。存在子句与环境恢复使用命题截断：只有当目标仍为命题时才消去截断，因而不会从中抽取被选定的见证。

```agda
open import Cubical.Foundations.Prelude using ( subst2; funExt⁻ )
open import Cubical.Data.FinData using ( toℕ )
open import Cubical.Functions.Logic using ( ⇔toPath )
import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∣_∣₁; ∥_∥₁; squash₁ )
```

层级中的集合带有其成员的小表现。给定 `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 hPropStructure 𝒮ʟ
```

前面导入的对象语言条件在由全部可构造集合承载的结构中解释。把一般绝对性构造实例化于类 `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` 所用的内层满足与词项求值，因此桥的语义终点和可定义子集共享同一个限制结构。

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

元素 `x : DB.SM` 已经由底层集合 `fst x` 及其属于 `B` 的证明 `snd x` 组成。由于 `B` 可构造且类 `L` 具有传递性，`fst x` 也可构造。映射 `intoL` 保留底层集合，只补上这份新的证书，从而得到宿主载体 `S` 的元素。这里没有使用 `B` 对隶属封闭的性质。

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

还需连接一层常元字母表。索引 `m : ⟪ fst B ⟫` 表现 `B` 的一个成员；`DB.ι m` 把该成员及其隶属证明包装为 `DB.SM` 的元素，`intoL` 再把同一底层集合视为 `S` 的元素。故其复合 `asConst` 正是把小表现所索引的公式交给宿主语义读取时所用的常元映射。表现映射 `DB.ι` 与包含 `intoL` 承担不同角色，尽管它们的复合保持被指称的集合不变。

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

## 把内层赋值编码为环境

内层环境 `δ : DB.SM ^ n` 在每个位置同时存放一个集合及其属于 `B` 的证明，而编码环境只需记录这些集合。因此，`values δ` 把每个条目投影到其第一分量。这里显式保留这个底层值族，因为词项求值与环境扩张都将同它的有穷图作比较。

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

集合 `graph δ` 是这个值族的有穷图：在位置 `i`，它记录一个有序对，其键是 `i` 的数码，其值是 `values δ i`。因此，内层向量与层级集合以两种形式携带同一赋值。下面的引理将建立在二者之间转换所需的精确等式。

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

绑定一个变元，就是在赋值前端加入一个新值。对底层值族而言，这是运算 `cons (fst x) (values δ)`；对内层向量而言，则是 `x ∷ δ`。引理 `cons-values` 逐点认同二者：在新的首位，两侧都给出 `fst x`；在每个后移位置，两侧都给出原来的值。这一条相干等式会由四种量词情形共同复用。

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

向量本身决定 `B` 的小表现中的一个索引族。在位置 `i`，`lookup i δ` 的第二分量证明该底层值属于 `B`；把 `∈-asFiber` 施用于这份证明，便得到索引 `index δ i`。这项构造直接使用向量中已有的成员证据，所以既不涉及命题截断，也不需要从编码图中恢复并选择一个代表。

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

纤维等价交付的不只有索引；它还把该索引所表现的成员与原来的底层值认同起来。`index-eq δ i` 在每个位置记录这条路径。因此，由 `index δ` 表现的值族与 `values δ` 逐点相同，这正是比较二者有穷图所需的输入。

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

把这个索引族交给典范环境构造子，便得到 `envFor δ`，它是可构造宿主结构的一个元素，也是与具体向量 `δ` 对应的典范层级编码。接下来的两项事实先认出它的底层图，再证明它属于环境集；其中没有选择任意的环境代表。

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

`envFor δ` 的底层层级集合恰为 `graph δ`。函数外延性把逐点路径 `index-eq δ i` 合成为值族之间的等式，`env` 的同余再把它变为 `envFor-graph`。这条底层集合的路径就是后文所用的接口。特别地，把 `δ` 扩张为 `x ∷ δ` 后会得到一个新的典范环境，同一定理可再次施用，无须比较隐藏在截断中的见证。

```agda
  envFor-graph : ∀ {n} (δ : DB.SM ^ n) → fst (envFor δ) ≡ 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} (δ : DB.SM ^ n) (z : S)
               → fst z ≡ graph δ → ⟨ z ∈ˢ envSet B n ⟩
  graph-envSet {n} δ z q = subst (λ w → ⟨ w ∈ fst (envSet B n) ⟩)
    (envFor-graph δ ∙ sym q) (envSet-in B (index δ))
```

图等式现在可以从成员等式中消去共同的环境要求。`Sat-mem`
说明，`z` 属于 `Sat B φ` 当且仅当它既属于 `envSet B n`，又满足`cond B φ`。给定 `fst z ≡ graph δ`，上一条引理已经提供前一个合取支，所以后一支与整个陈述逻辑等价；`⇔toPath` 再把两个方向的蕴涵变成真值之间的路径。因此，`Sat-cond` 还没有解释公式的语义，它只是分离出接下来要由归纳解释的递归条件。

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

## 读取词项与环境扩张

第一条读引理把对象语言的词项谓词与实际的词项求值比较。在外围环境`γ` 中，槽位 `ei` 存放编码赋值，槽位 `vi` 存放候选取值。若前者的底层集合是 `graph δ`，那么满足 `tmIs (mapTm intoL t) vi ei` 就迫使后者的底层集合等于 `fst (⟦ t ⟧ᴮ δ)`。对常元而言，该谓词本身就是所需的等式：沿 `intoL` 作常元改名只改变载体的包装，底层集合仍是这个常元的取值。

```agda
  tmIs-out : ∀ {n k} (t : Term DB.SM n) (δ : DB.SM ^ n) (γ : S ^ k) (vi ei : Fin k)
           → fst (lookup ei γ) ≡ graph δ
           → ⟨ γ ⊨ tmIs (mapTm intoL t) vi ei ⟩
           → fst (lookup vi γ) ≡ fst (⟦ t ⟧ᴮ δ)
  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 (fst (lookup vi γ)))
      (subst (λ w → ⟨ pr (# (toℕ i)) (fst (lookup vi γ)) ∈ w ⟩) qe
        (tmIs-var-out i γ vi ei h))
```

反向引理从语义取值等式构造词项谓词的满足。常元情形仍然是直接的：常元改名之后，对象语言等式所要求的恰是作为假设给出的等式。`tmIs-out` 与 `tmIs-in` 合在一起，使词项取值可以双向读取。原子子句会用这对引理比较两个已求值词项，有界量词子句则会用它们读取界项的取值。

```agda
  tmIs-in : ∀ {n k} (t : Term DB.SM n) (δ : DB.SM ^ n) (γ : S ^ k) (vi ei : Fin k)
          → fst (lookup ei γ) ≡ graph δ
          → fst (lookup vi γ) ≡ fst (⟦ t ⟧ᴮ δ)
          → ⟨ γ ⊨ 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)) (fst (lookup vi γ)) ∈ w ⟩) (sym qe)
      (subst ⟨_⟩ (sym (lookup-spec (values δ) i (fst (lookup vi γ)))) q))
```

第二对读引理处理赋值的扩张。在 `consAtL ei mi di` 中，槽位 `di` 存放旧图，槽位 `mi` 存放新添的首值，槽位 `ei` 则是候选的扩张图。若前两个槽位分别与 `δ` 和 `x` 相符，那么满足该谓词便推出 `ei` 处的底层集合是`graph (x ∷ δ)`。量化公式从原赋值转到前端增加一个条目的赋值时，需要的正是这条等式。

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

证明先使用 `consAtL-adequate`。在旧图假设下，这条路径把候选扩张槽位等同于 `env (cons (fst (lookup mi γ)) (values δ))`。等式 `qm` 把其首值替换为 `fst x`，`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 δ`，新值槽位存放 `fst x`，候选扩张槽位存放 `graph (x ∷ δ)`；由此构造 `consAtL` 的满足关系。这个方向使每个量词子句都能直接把典范环境 `envFor (x ∷ δ)` 用作经过认证的扩张，而无须从存在表示中提取一个未截断的环境。

```agda
  consAtL-in : ∀ {n k} (δ : DB.SM ^ n) (x : DB.SM) (γ : S ^ k) (ei mi di : Fin k)
             → fst (lookup di γ) ≡ graph δ
             → fst (lookup mi γ) ≡ fst x
             → fst (lookup ei γ) ≡ 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} φ = (δ : DB.SM ^ n) (z : S) → fst z ≡ 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`之求值的证明，以及从 `fst v` 到 `fst w` 的成员关系。内层语义则直接陈述实际求值 `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` 展开经过截断的候选。目标`fst T ∈ fst U` 是命题，所以 `PT.rec` 可以逐个考察候选包。在环境`w ∷ v ∷ z ∷ []` 上，两次使用 `tmIs-out`，分别把 `v` 与 `T`、`w`与 `U` 认同。二元运输 `subst2` 随后把记录的关系 `fst v ∈ fst w`搬到 `fst T ∈ fst U`，这正是该原子的内层解释。

```agda
    fwd : ⟨ (z ∷ []) ⊨ cond B (mapFo intoL (t ∈̇ u)) ⟩ → ⟨ fst T ∈ fst U ⟩
    fwd h = PT.rec (snd (fst T ∈ fst U))
      (λ { (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 : ⟨ fst T ∈ fst U ⟩ → ⟨ (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` 的底层集合按定义就是 `fst T`，`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 ))) ∣₁
```

相等原子沿用同一方案，只把候选之间的关系换成相等。递归条件在命题截断之下给出两个候选词项值、两份词项读式，以及它们底层集合之间的路径；内层语义则直接要求路径 `fst T ≡ fst U`。与成员原子一样，`⇔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 : fst v ≡ fst T` 与 `hu : fst w ≡ fst U`，而候选关系是`r : fst v ≡ fst w`，那么所需路径的方向恰为 `sym ht ∙ r ∙ hu`。也就是先从 `t` 的实际求值逆行到其候选，经过已记录的候选相等，再正向到达 `u`的实际求值。

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

反向映射仍以 `intoL T` 与 `intoL U` 作为外围见证。向内词项读式证明它们满足两条词项谓词，而假设路径 `fst T ≡ fst U` 恰好提供
`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 : fst T ≡ fst U → ⟨ (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 = PT.rec squash₁
```

在截断之内，外围见证及其证明 `x∈B` 组成限制载体元素`(fst x , x∈B)`。这是无界量化变元唯一的论域限制；属于界项取值的附加成员条件只在有界量词中出现。随后，`consAtL-out` 把 `e` 认同为具体扩张赋值 `(fst x , x∈B) ∷ δ` 的图。归纳假设把已记录的子公式成员关系运输为该赋值下的内层满足关系，最后把这个取值连同证明写入内层存在的命题截断。

```agda
      (λ { (x , (x∈B , (e , (hc , he)))) → ∣ (fst x , x∈B)
         , subst ⟨_⟩ (ia ((fst x , x∈B) ∷ δ) e
             (consAtL-out δ (fst x , 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 (PT.map
      (λ { (x , ha) → intoL x , (snd x , (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`、载体成员证明 `snd x`，以及典范扩张环境。`consAtL` 的向内读式验证该环境确由 `x` 的取值扩张旧图。子句随即给出对递归子取值的隶属，归纳假设再把它送到内层满足。这个无界变元唯一的限制是属于 `B`，而该证明已经存放在 `x : DB.SM` 的包装中。

```agda
      (cond∀-out B (mapFo intoL a) z h (intoL x) (envFor (x ∷ δ)) (snd x)
        (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` 之扩张的环境，都给出对子取值的隶属。证明把 `(fst x , x∈B)` 包装成限制载体的元素，再调用已给定的内层全称函数。`consAtL` 的向外读式把经认证的环境认同为扩张赋值的图，随后沿这条等式反向读取归纳假设，得到所需的子取值隶属。整个方向都是逐点的，不使用命题截断。

```agda
      (λ x e x∈B hc → subst ⟨_⟩
        (sym (ia ((fst x , x∈B) ∷ δ) e
          (consAtL-out δ (fst x , x∈B) (e ∷ x ∷ z ∷ [])
            zero (suc zero) (suc (suc zero)) q refl hc)))
        (k (fst x , 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` 处的子条件。外层截断被消去到命题值的语义目标中，内层截断则映射到语义存在见证 `(fst x , x∈B)`。

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

词项读式 `tmIs-out` 把候选 `w` 的底层集合与语义取值 `T` 的底层集合认同起来。沿这条路径运输，`x∈w` 便成为内层语义要求的界项成员证明，即 `fst x ∈ fst T`。另一方面，`consAtL-out` 把 `e` 认同为 `(fst x , x∈B) ∷ δ` 的图，因此归纳假设可把 `e` 处的子条件转成扩张赋值处的满足。这两项结果共同构成内层 `∃[]` 的载荷。

```agda
                 (tmIs-out t δ (w ∷ z ∷ []) zero (suc zero) q hw) x∈w
             , subst ⟨_⟩ (ia ((fst x , x∈B) ∷ δ) e
                 (consAtL-out δ (fst x , 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 (PT.map
      (λ { (x , (hx , ha)) → intoL T
         , ( tmIs-in t δ (intoL T ∷ z ∷ []) zero (suc zero) q refl
```

语义见证 `x : DB.SM` 分别提供两道限制：`snd x` 证明它属于载体，`hx` 证明它属于界 `T`。由于选取的候选正是 `intoL T`，证明可原样保留 `hx`。扩张环境取为 `envFor (x ∷ δ)`，由 `consAtL-in` 加以认证，再反向读取归纳假设，得到对递归子取值的隶属。

```agda
           , ∣ intoL x , ((snd x , 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`，再取证明 `fst x ∈ fst 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 ⟧ᴮ δ
```

构造正向函数时，取 `x` 及其语义界项成员证明 `hx`。条件的全称子句以真正的界值 `intoL T` 实例化，其词项读式由 `tmIs-in` 给出；变元则以外围代表 `intoL x` 实例化。两道限制来自不同来源：`snd x` 记录 `x ∈ B`，`hx` 记录 `fst x ∈ fst T`。`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 ∷ δ)) (snd x) hx
```

构造反向函数时，条件对以下数据作全称量化：任意候选界值 `w`、证明它读作词项取值的 `hw`、带有 `x∈B` 与 `x∈w` 的外围成员 `x`，以及经认证的扩张 `e`。词项的向外读式把 `w` 的底层集合与 `fst T` 认同起来；沿这条路径运输 `x∈w`，便得到把内层全称函数用于 `(fst x , 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 ⟨_⟩
```

应用内层全称函数后，得到子公式在 `(fst x , x∈B) ∷ δ` 处的满足。`consAtL` 的向外读式把经认证的环境 `e` 认同为这个赋值的图。因此，反向读取归纳路径，便把语义满足变成条件所需的子取值隶属。至此有界全称情形闭合，四个量词论证全部完成，并且载体限制与界项限制始终彼此分明。

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

各个情形现在沿公式作结构递归，汇合为 `Sat-spec`。它的归纳不变量十分精确：对每个赋值 `δ`、每个外围元素 `z`，以及每条从 `fst z` 到 `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 : ⟪ fst B ⟫`，表现映射给出底层集合 `⟪ fst B ⟫↪ m`；表现隶属的两种读式证明该集合属于 `fst B`。把集合与这条证明配对，便得到 `inB m : DB.SM`。

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

索引族 `g : Ix B n` 在每个有穷位置都含有一个小成员索引。函数 `tab` 按 `n` 递归，把它变成 `DB.SM ^ n` 中的赋值：首项是 `g zero` 所表现的集合，并配上 `inB (g zero)`；尾部来自移位后的族 `λ i → g (suc i)`。因此，所有条目的次序都得到精确保留。

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

第一条相容等式从 `tab g` 忘去载体成员证明，恰好恢复 `g` 所表现的集合族。在位置零处，这条等式是自反的；在后继位置，它递归地来自移位后的尾部。函数外延性把这些逐点等式合成为 `tab-values`，即完整取值族之间的等式。

```agda
    tab-values : ∀ {n} (g : Ix B n) → values (tab g) ≡ (λ i → ⟪ fst B ⟫↪ (g i))
    tab-values {zero} 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) ≡ fst (envS B g)
    tab-graph g = cong env (tab-values g)
```

`envSet` 的向外规格从成员 `z` 出发，在命题截断下恢复索引族 `g`，以及一条从 `fst z` 到 `envS B g` 底层集合的路径。把 `g` 映射为 `tab g`，再将该路径与 `tab-graph` 的逆向复合，便得到满足 `fst z ≡ graph δ` 的赋值 `δ`。结果仍在命题截断之下，既不提供全局选定的解码，也不声称解码唯一。后续的子句语义论证在处理任意编码环境时，使用的正是这项受限接口。

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

`Sat-spec` 从一项给定赋值和一条图等式出发。`Sat-out` 则陈述满足取值的任意成员 `z` 所对应的结论：在 `∃[]` 下，存在赋值 `δ`，其图就是 `fst z`，并且它在限制结构中满足该公式。命题截断是结论本身的一部分，所以这项定理既不选定解码赋值，也不证明这样的赋值唯一；它只断言从属于 `Sat` 到存在一项满足公式的表示这一方向。

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

最后两行完成外向读式，同时没有增强恢复所得资料的逻辑强度。从原来的 `Sat` 成员证明出发，`Sat-mem` 只取出「`z` 属于环境集」这一分量；`envSet-out` 随即在命题截断下返回索引族 `g` 及其图等式。在 `PT.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))
```

## 与可定义子集相符

为了把这项递归同可定义子集比较，常元需要穿过三个论域。公式 `ψ` 起初取常元于小呈现 `⟪ fst B ⟫`；`DB.ι` 把这些常元送入限制载体，`intoL` 再把所得载体元素送入外围载体 `S`。按定义，这两个映射的复合就是 `asConst`。因此，`mapFo-comp` 所表达的常元改名函子性把两次改名所得的公式 `mapFo intoL (mapFo DB.ι ψ)` 认同为直接改名所得的公式 `mapFo asConst ψ`。这是公式之间的等式，它使语义桥能够采用递归所需的常元形式。

```agda
  private
    mapFo-fuse : ∀ {n} (ψ : Formula ⟪ fst B ⟫ 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 : ⟪ fst B ⟫)
                 → fst (envS B (λ _ → m)) ≡ graph (DB.ι m ∷ [])
    graph-single m = cong env (funExt (λ { zero → refl ; (suc ()) }))
```

这两项归一化给出小常元字母表中的桥。设 `z` 的底层集合等于内层赋值 `δ` 的图，则 `z` 属于 `mapFo asConst ψ` 的递归取值这一命题，等于 `mapFo DB.ι ψ` 在 `δ` 处的内层满足。右侧公式的常元属于限制载体，并在该结构中按恒等解释求值；等价地说，它就是把原小公式的常元按 `DB.ι` 解释。证明先取 `mapFo-fuse` 的对称方向，在左侧显出两次常元改名，再应用 `Sat-spec`。由此先得到适用于任意元数的小字母表版本，再在下文特化到一个自由变元。

```agda
  Sat-small-spec : ∀ {n} (ψ : Formula ⟪ fst B ⟫ n) (δ : DB.SM ^ n) (z : S)
                 → fst z ≡ 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.ι m ∷ []` 处的内层满足，其中常元由 `DB.ι` 解释。

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

再接三条路径，便到达陈述中的递归取值。首先，`⊨-map` 的对称方向把「以 `DB.ι` 解释常元时 `ψ` 的满足」换成「恒等解释下，改名公式 `mapFo DB.ι ψ` 的满足」。其次，`Sat-spec` 的对称方向借助 `graph-single`，把这项内层满足换成 `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 ψ)
```

## 小结

中心结论 `Sat-spec` 对每项给定赋值，把递归构造所得取值中的隶属与内层满足认同起来：若 `fst z ≡ graph δ`，则 `z` 属于 `Sat B (mapFo intoL φ)` 与 `δ ⊨ᴮ φ` 是同一个命题。若输入改为满足取值的任意编码成员，`Sat-out` 也只在 `∃[]` 下给出一项具有所需图等式与满足证明的赋值；它既不选定这项赋值，也不证明其唯一。把小表现中的常元依次经 `DB.ι` 与 `intoL` 改名后，`Sat-small-spec` 给出任意元数的桥，`defSet-Sat` 再把它特化到一个自由变元，将可定义子集中的隶属与典范单条目环境的隶属认同起来。统一表的构造与候选表取值的唯一性仍需后续的钉扎递归和统一满足关系论证。