---
title: "在对子码封闭的定义域上钉扎递归"
module: L.Coding.PinnedRecursion
lang: zh
site: "Bedrock"
description: "固定在对子码封闭的索引集上的递归"
stage: "内部编码：表与统一满足关系"
reading_order: 66
canonical: https://bedrock.institute/zh/L.Coding.PinnedRecursion.html
html: L.Coding.PinnedRecursion.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/Coding/PinnedRecursion.lagda.md
prerequisites: [Base.Prelude, Base.Classical, FOL.ZFStructure, FOL.Syntax, FOL.Absoluteness, FOL.Manipulation.ConstantMapping, V.Hierarchy, V.Coding, L.Constructible, L.Axioms.Numerals, L.Coding.Model, L.Coding.Expressions, L.Coding.Closure, L.Coding.EnvironmentSet, L.Coding.CodeConstructibility, L.Coding.CodeSet, L.Coding.Satisfaction, L.Coding.SatisfactionBridge, L.Coding.SatisfactionTable, L.Coding.Quantification, L.Coding.EnvironmentTower, L.Coding.CodeDomain, L.Coding.CodeAlphabet, L.Coding.SatisfactionClauses, L.Coding.SatisfactionClauseSemantics]
routes: [internal-satisfaction]
translations: [https://bedrock.institute/en/L.Coding.PinnedRecursion.md, https://bedrock.institute/ja/L.Coding.PinnedRecursion.md]
agent_guide: /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 )
```

模块固定宇宙层级并命名经典假设：下文每条定理都准确记录它消耗哪个层级的排中律实例。

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

结构递归沿公式文法的十个构造子进行：隶属与相等原子式、合取、析取、蕴含、假、两个无界量词、`∀[]-syntax` 与 `∃[]-syntax`。常元重标记使同一棵语法树先在某个载体的成员字母表上读取，再在可构造载体上读取，而不改变其构造结构。

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

公式键用集合论有序对把元数与语法码组合起来。这一构造有两个版本：一个直接位于累积层级中，另一个在 `L` 内部并携带可构造性证明。对码、数码与公式码的投影定理将说明两者的底层层级集合相等。

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

封闭条件恰好追随公式满足关系的递归依赖。二元联结词需要两个同元数的公式子式，无界量词需要其后继元数主体，而 `∀[]-syntax` 与 `∃[]-syntax` 只需要各自后继元数的公式主体。后两种构造子携带的词项码在子句内部求值，不要求属于封闭定义域。

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

对公式 `ψ`，`Sat` 给出由递归定义的典范满足环境集合；满足关系表则存放编码后的键值对。定理将比较这种对中已经给出的值与 `Sat ψ`。表的全定义性只在命题截断下供给子公式的值，因此证明可以用这些值建立等式，却不能把它们变成可复用的选择函数。

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

零至九这十个标签选取十条构造子子句。环境塔对每个自然数元数 `n` 记录一对数据：数码 `# n` 与长度为 `n` 的编码环境集合。这两套坐标使子句既能识别语法构造子，也能识别其满足关系集合所处的元数。

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

表规格有三个数学部分：定义域中的每个键都有某个值；每个表项都是键值对，且其键属于定义域；十个构造子各自满足相应的语义子句。子句语义把最后一部分读成外延事实。当候选值与典范递归值在环境集上具有相同外延时，外延性便将它们的底层层级集合等同起来。

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

子句环境是有限向量，延拓框架会使每个原有坐标发生移位；查找与搬运负责保持这些坐标对齐。藏在命题截断下的见证只会被消去到命题值目标：钉扎证明中的底层层级集合等式，以及填充证明中固定对象语言子句的满足关系。这些消去都不会露出可复用的取值、解码结果或框架数据。

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

命题截断保留见证存在这一事实，却忘去具体见证；因此，其消去目标必须取值于命题。层级中的隶属取值于命题，而层级 `V` 是 h-集合，所以其中两个集合之间的等式也是命题，可以作为下文诸次消去的合法目标。

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

构造子标签存为 `Fin 10` 的元素，语法码中使用的则是普通自然数数码。映射 `toℕ` 忘去界限证明，露出编码有序对中数码所表示的自然数；原有界限仍保证只会出现零至九的标签。

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

以 `S` 表示 `L` 上一阶结构的载体。`S` 的元素由一个底层层级集合及其可构造性证明组成。本章多数结论只比较第一投影，因为满足关系所需的数学内容正是被表示集合的相等。

```agda
open hPropStructure 𝒮ʟ using ( S )
```

对象语言子句在 `L` 所承载的一阶结构中解释。因此，记号 `γ ⊨ φ` 表示有限环境 `γ` 在该结构中满足公式 `φ`。后续桥引理将把这种内部满足断言与外部定义集合 `SatW ψ` 中的隶属相比较。

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

## 匹配键、标签与解码公式

先比较通往公式键的两条路线。外部路线把字母表符号嵌入层级并配以外围数码；内部路线把常元重标记为可构造集合、在 `L` 内部编码公式，并配以内部数码。

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

证明先对齐语法码分量：重标常元后取外围公式码，等于投影重标后公式的内部码。接着对齐元数数码，最后投影内部有序对。所得路径连接两个键的第一投影；它不主张二者所附的可构造性证明在定义上相同。

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

匹配模块针对单一载体 `W` 陈述：其字母表供给要匹配形状的项与公式语法。

```agda
module Match (W : S) where
  open Alphabet W
```

`MatchN` 是以标签为索引的形状记录族：标签零与一时，它给出一个原子的两个项及其编码对；标签二至四时，它给出一个二元联结词的两个直接子公式及其编码对。该族以已知公式为索引，因此不是对任意集合的解析器。

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

标签四至八延续同一张形状表。标签四记录蕴含及其两个公式码；标签五记录假，并以零号数码为载荷；标签六与七记录两个无界量词的后继元数主体；标签八记录 `∀[]-syntax` 的当前元数词项码与后继元数主体。

```agda
  MatchN {n} 4 ψ r = Σ[ a ∈ Formula Ab n ] Σ[ b ∈ Formula Ab n ] ((ψ ≡ a ⇒̇ b) × (r ≡ pr (cd a) (cd b)))
  MatchN 5 ψ r = (ψ ≡ ⊥̇) × (r ≡ # 0)
  MatchN {n} 6 ψ r = Σ[ a ∈ Formula Ab (suc n) ] ((ψ ≡ ∃̇ a) × (r ≡ cd a))
  MatchN {n} 7 ψ r = Σ[ a ∈ Formula Ab (suc n) ] ((ψ ≡ ∀̇ a) × (r ≡ cd a))
  MatchN {n} 8 ψ r = Σ[ t ∈ Term Ab n ] Σ[ a ∈ Formula Ab (suc n) ] ((ψ ≡ ∀̇∈ t a) × (r ≡ pr (ct t) (cd a)))
```

标签九为 `∃[]-syntax` 保存相应载荷：当前元数处的词项码与后继元数处的公式码组成的对。这个辅助族在每个不小于十的自然数标签处都是空类型。因此，`MatchN` 恰好描述十种构造子形状；把它定义在所有自然数上，是为了支持沿标签等式作搬运。

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

搬运辅助在标签与载荷之间转换匹配记录。配对单射性把编码对的相等拆为标签分量与载荷分量，数码单射性搬运标签索引；匹配记录随后沿两者替换。

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

标签读取器 `matchAt` 并不解码任意集合。它从一条已给公式出发，陈述该公式的码与某个带标签对相等的等式，并返回匹配记录：对公式的情形分析暴露其自身的标签，而搬运辅助把它改标为给定的标签。

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

余下诸式不进行任何搜索。在每个结构情形中，已知构造子直接给出其典范标签与载荷：蕴含给出两个子公式码，假给出零，两个无界量词各给出主体码，而 `∀[]-syntax` 给出词项码与主体码。随后，同一个搬运辅助把这些典范数据与输入等式所指定的标签和载荷对齐。

```agda
  matchAt (a ⇒̇ b) k r e = at (a ⇒̇ b) 4 k _ refl (a , b , (refl , refl)) r e
  matchAt ⊥̇ k r e = at ⊥̇ 5 k _ refl (refl , refl) r e
  matchAt (∃̇ a) k r e = at (∃̇ a) 6 k _ refl (a , (refl , refl)) r e
  matchAt (∀̇ a) k r e = at (∀̇ a) 7 k _ refl (a , (refl , refl)) r e
  matchAt (∀̇∈ t a) k r e = at (∀̇∈ t a) 8 k _ refl (t , a , (refl , refl)) r e
```

对 `∃[]-syntax`，典范标签为九，载荷是界词项码与后继元数主体码组成的对。这最后一个结构分支使 `matchAt` 覆盖全部公式构造子；其结论仍只描述作为输入已经给定的公式之形状。

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

现设 `c` 属于典范码集，并被表示为元数数码 `# n` 与载荷 `z` 的有序对。`c` 在 `AllCodes W` 中的隶属，经命题截断给出某个元数 `n₁`、该元数上的某条公式 `ψ₁`，以及 `c` 与其键之间的等式。余下任务是把 `n₁` 与题设的 `n` 对齐。

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

有序对编码的单射性分别等同两个元数数码与两个载荷；数码单射性继而给出路径 `n₁ ≡ n`。沿这条依赖路径搬运 `ψ₁`，并用 `cd-subst` 校正其码，便得到一条元数恰为 `n` 且码为 `z` 的公式。结果仍处于命题截断之下，所以既不提供选定的解码器，也不主张解码公式唯一。

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

## 对子码封闭定义域上的唯一性

可靠性论证局限于任意给定的码域 `C`。除候选表 `T` 外，它还假设：所存载体为 `W`，十个标签槽含有正确数码，环境槽为正确的塔，`C` 对所需的直接公式子码封闭，并且 `T` 满足打包后的表规格。这些假设并不声称每个公式键都属于 `C`。

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

以 `Tv`、`Cv` 与 `Ev` 分别表示表槽、码域槽与环境塔槽中所存的底层层级集合。原子公式不需要在 `Cv` 中递归查找：其词项码由原子桥直接解释。只有构造子含有直接公式子式时，证明才会递归调用。

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

令 `Wv` 表示载体 `W` 的底层层级集合。量词桥以该集作为量化范围，原子桥则在同一载体所确定的字母表上解释词项码。证明把值作为层级集合比较，所以钉扎结论是第一投影的等式，而非 `S` 中携带证明之记录的等式。

```agda
    Wv = fst W
```

环境塔给出公式元数所对应的一行；子句框架把这一行与公式键、带标签的公式码及候选表值组合起来。在该框架处读取构造子子句，便会露出按成员刻画候选值的语义关系。

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

打包假设 `hT` 包含全定义性、表项之键位于 `C` 的断言，以及十条构造子子句的合取。钉扎证明用全定义性取得子公式表项，并用构造子子句刻画值。所讨论的候选表项由命题直接给出，因此定义域断言 `hOn` 虽从包中保留下来，却不被这段唯一性论证使用。

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

十条构造子子句存为一个由 `Fin 10` 索引的有限合取。读取器 `bigAnd-out` 把这个包化为子句族 `cl k`，于是每个结构情形可以按其构造子标签准确选取对应子句，而无须改动其余九条。

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

情形模块打包一次归纳步骤的数据：一条公式、其标签、其载荷集合、码与载荷间的等式、其键在码域中的成员资格、一个候选表条目及该条目的隶属。塔读取为该公式的元数供给典范塔条目。

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

公式码起初以典范数码 `# k` 表示；标签等式把这个数码改写为槽 `N k` 中存放的值，所得等式便符合子句的输入形式。随后，框架 `δ12` 在外围环境前添加十二个坐标，其中包括元数行、公式键与公式码、载荷及候选值。

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

把所选子句施于这个具体框架，得到标签所索引关系 `relN k` 的满足关系。随后把关系读取固定在 `δ12` 上；后面的各构造专用读取会延拓同一个框架，并把 `rel` 解包为适用于原子式、二元联结词或量词的外延事实。

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

若子公式的键属于 `Cv`，表的全定义性只给出命题截断后的一个对，其中含有某个值 `ya` 及该键处的表项。因此，`sub` 只证明纯粹存在，而不选定一个值。每个递归情形都把这一见证直接消去到层级集合的等式；h-集合结构保证该目标是命题。

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

中心谓词是条件式的。若 `ψ` 的键在码域中，则在该键处记录的每个表值 `y` 的底层集，都与 `ψ` 的递归满足集合的底层集相同。这种条件式正是诚实的形式：对域外的键不作任何断言。

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

`Pinned` 的证明按给定公式作结构递归。递归调用只施于语法构造子直接给出的公式子式。这里既不在 `C` 的成员上递归，也不在任意码上作良基递归，更不会试图给尚未被识别为公式键的码定义值。

```agda
  private
```

编码公式的载荷集合由码等式经配对投影恢复。

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

三个二元联结词共享同一种递归模式。诸参数依次确定构造子、标签与载荷等式、相应的对象语言关系，以及一条语义桥。该桥假设延拓环境中的两个坐标分别等于两个子公式的典范满足关系集合，并据此为复合公式的典范值给出外延事实。

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

该桥针对一个在指定坐标含有两个子值的环境陈述。另有一条封闭读取把复合键在 `Cv` 中的隶属转化为两个同元数子键的隶属。于是，无论全定义性给出哪些子表项，递归假设都能分别把它们与 `SatW a`、`SatW b` 等同。

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

为证明复合公式被钉扎，证明依次消去经命题截断的左子值、右子值与二元关系见证。每次消去的最终目标都是等式 `fst y ≡ fst (SatW (opA a b))`。由于 `V` 是 h-集合，该等式是命题，所以这些消去不会留下对子值或框架数据的固定选择。

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

二元关系读取器用两个子公式码、键和值以及辅助见证延拓公共子句框架。在这个延拓环境中，子句为候选值 `y` 给出外延事实，而桥为 `SatW (opA a b)` 给出相应的外延事实。定理 `ext-unique` 对这两个事实应用集合外延性，从而等同二者的底层集合。

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

关系读取由子句经标签同一视获得；两个子值由表的全域性获得，先左子值，后右子值。

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

局部模块 `K` 记录复合公式本身、其构造子标签、成对子公式码载荷的一个可构造表示、复合键的定义域成员资格，以及候选表项。这样，整个二元论证只使用一个具体子句框架；递归假设则只涉及两个直接子公式。

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

两个无界量词也共享一个递归情形。其主体具有后继元数，载荷就是该主体的码。语义桥接收固定载体所在的坐标与主体表值所在的坐标；把该表值等同于 `SatW a` 后，桥便在 `envSet W n` 上刻画量化公式的典范满足关系集合。

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

载体坐标仍位于原来的外围环境中，框架延拓后通过索引移位访问；子公式值则是关系见证新露出的坐标。封闭性给出后继元数主体键的成员资格，递归假设把该键处每个表项都等同于主体的典范满足关系集合。于是，桥把对象语言量词与在 `Wv` 上的量化准确对应起来。

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

证明先消去经命题截断的主体值，再消去读取量词关系所得的经命题截断见证。该见证以后继数码、主体键、主体值及辅助坐标延拓公共子句框架。两次消去都以候选值和典范量化满足关系集合之间的等式为目标，因此不会全局选定任何主体值。

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

在延拓环境中，关系子句为候选表值 `y` 给出外延事实。递归假设供给桥所需的等式，桥再利用移位后载体坐标处的等式，为 `SatW (qA a)` 给出相应的外延事实。最后，`ext-unique` 中的集合外延性等同两个底层集合。

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

这里，`K` 实例化于量化公式 `qA a`，而非其主体 `a`。它的载荷表示由主体码构造，但定义域成员资格与候选表项属于量化公式的键。主体则作为唯一递归子式单独出现，并处于后继元数。

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

有界量词的构造子码有两个载荷分量：界定词项的码，以及元数增加一的体公式之码。因此，这个情形引理需要构造子标签与载荷等式、相应的关系子句、用五个槽位固定写出的语义体、该语义体的外延桥，以及随后真正需要的唯一一条封闭蕴涵：复合公式的键属于定义域时，体公式的键也属于定义域。这里不要求定义域对词项码封闭。

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

体等式记录有界量词体在五个平移槽位下的拼写方式，使桥能以固定的公式形状陈述，而不依赖调用点的具体槽位索引。

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

这条桥把有界公式的递归满足集与五槽语义体在编码环境上描述的外延对应起来。这里量词与联结词仍是参数，所以同一陈述同时涵盖有界全称与有界存在两种情形，不能一概读成存在某个成员。随后，证明正是把这条外延事实与从表子句读出的外延事实相比较。

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

假设复合公式的键属于定义域时可以推出体公式的键属于定义域，并且体公式键处的表值已经被钉扎，那么复合公式键处任何给定表值也会被钉扎。全定义性只给出经过命题截断的体公式表值，有界量词子句的读式也只在命题截断下给出其见证。这里可以消去这两层命题截断，因为结论是层级中底层集合的等式，因而是命题。复合公式的表值则由结论的前提直接给定，并非由全定义性取得，也没有藏在命题截断之下。

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

读出子句见证后，证明组成一个扩展环境，其中包含后继元数、体公式的表值与键、体公式码，以及界定词项码。在这同一个环境上，`ext-unique` 比较两条外延事实：一条来自子句，刻画候选表值；另一条来自桥，刻画递归定义的满足集。沿体公式等式作运输后，两条事实中的谓词便完全一致。

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

封闭性先给出体公式键的定义域成员关系，归纳假设再把由全定义性取得的体公式表值认同为递归满足集。这个认同与载体等式、词项码等式及两条标签等式一起满足桥的全部前提。有界量词子句的向外读式则给出四个辅助对象和一条外延事实，它们只用于这里的局部比较。

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

三个被命名的分量支撑该情形：呈现为载体元素的载荷、携带词项码的第一投影，以及提供十二槽框架与复合键处表条目的情形模块。

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

原子公式没有公式子式，因此这个情形不需要封闭蕴涵，也不需要递归假设。其构造子载荷是两个词项码组成的对。其余前提识别相应的原子关系子句，并提供一条桥：由载体等式、两条词项码等式和两条标签等式，得到原子公式递归满足集的外延事实。

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

桥参数陈述原子公式的外延事实：满足关系集合恰包含其词项取值满足对象语言关系的那些环境。结论说：只要该原子公式的键属于定义域且给定一个表项，该公式就被钉扎。

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

原子子句只在命题截断下给出一个辅助集合，以及刻画候选表值的外延事实。在由该集合与两个词项码组成的环境中，原子桥给出另一条外延事实，刻画递归满足值。累积层级中的等式是命题，因此可以消去命题截断下的子句见证，再由 `ext-unique` 认同两个底层集合。

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

桥在扩展环境处以两条标签等式与载体等式被应用，产出原子体的外延事实。原子关系的向外读法供给中间集合。

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

三个被命名的分量支撑原子情形：作为载体元素的载荷、其第一与第二投影处的两个词项码，以及提供十二槽框架的情形模块。

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

对这个隶属原子而言，在所示环境中的满足关系依定义就是两个底层集合之间的隶属命题。因此，`memAgree` 中的两个方向都是恒等映射。这只是原子桥在此处需要的局部相合，并未对其他关系符号作出陈述。

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

相等相合对相等原子说同样的话：对象语言的相等就是底层集合的等同。

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

二元联结词的闭包引理从形状满足读取向下闭包：若复合键在域中，则两个分量键都在域中。证明是二元闭包消去的一次应用。

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

下面的二元封闭引理先固定两个子公式，再接收形状证明。其结论并未改变：若某个键的载荷是这两个公式码组成的对，则该键属于定义域便推出两个子公式的键都属于定义域。这样的参数次序使结构递归的每个分支都能把共同的封闭事实专门用于自己的两个子公式。

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

对无界量词而言，封闭性只沿构造子载荷中唯一的公式分量向下。因此，若元数为 `n` 的量化公式之键属于定义域，则其后继元数处的体公式之键也属于定义域。这个陈述只针对当前给出的构造子码，并不解码任意定义域成员。

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

有界量词的载荷以词项码为第一分量，以体公式码为第二分量。封闭条件只沿第二分量向下：复合公式的键属于定义域，便推出后继元数处的体公式之键属于定义域。它有意不对界定词项码给出任何定义域成员关系。

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

两个被命名的分量支撑有界量词闭包：呈现为载体元素的载荷，及其携带词项码的第一投影。

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

钉扎谓词由公式的结构递归证明。隶属原子以隶属关系的恒等相合应用原子情形，不消耗任何子公式假设。

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

相等原子以相等的恒等相合应用原子情形。合取情形以合取桥与标签二处的二元闭包应用二元情形，消耗两个子公式的已钉扎假设。

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

析取与蕴涵在各自标签处遵循同一二元模式。假无子公式：其唯一性由假子句的向外读法与假桥直接证明，二者共同产出空外延。

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

两个无界量词分支分别使用存在桥与全称桥。封闭性把量化公式键的定义域成员关系传到后继元数处的体公式键，递归假设再钉扎桥所需的体公式值。有界全称分支遵循同样的局部模式，但它的构造子码还含有一个词项码；它以全称 `∀[]-syntax` 桥调用有界情形，而封闭性仍然只沿体公式向下。

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

有界存在分支以存在 `∃[]-syntax` 桥调用有界情形。相应的封闭合取项只给出后继元数处体公式键的定义域成员关系，递归假设随后钉扎该体公式的表值。界定词项由桥求值，不会成为另一个递归子问题。

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

## 填充全部满足关系子句

下面证明反向论证。这里不是从子句推出递归值，而是假设已经表示出的表值与递归定义的满足集相合，再用这种相合验证每一条子句。工作集 `W` 固定整个论证使用的字母表、满足关系桥与构造子码匹配。

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

在同一个环境中固定表、载体、公式码定义域与环境塔的槽位，并给出十个数码标签和环境塔规格。关键假设 `val≡` 是条件性的：对一个已知公式键以及该键处给定的表条目，它把条目的底层值认同为该公式递归定义的满足集。它既不声称每个键都有表示，也不选择任何表条目。

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

另外三个假设只在命题截断下提供存在性。若一个定义域成员被表示为元数码与载荷之对，则仅能得到同一元数的某个公式解码；全定义性仅给出每个定义域键处某个表值的存在；每个表成员也仅能在命题截断下分解为键值对，并证明其中的键属于定义域。这些假设都没有定义可复用的解码函数或表值选择函数。

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

最后一个假设补全定义域条件：每个已经表示在表中的成员，都只在命题截断下被识别为某个对 `(c,yc)`，并且 `c` 属于给定的公式码定义域。因此，全定义性控制从键到表值的方向，这条条件则控制从表成员回到定义域键的方向。缩写 `Tv` 与 `Cv` 只命名这些局部陈述所用的底层表集合与定义域集合。

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

这里还命名环境塔的底层集合与载体。随后，框架、子句与关系的读式在三个尺度上表达同一批已存数据：十二对象组成的共同框架、表的顶层条件，以及依构造子而定的关系。它们只是对固定环境的局部读法，并没有增加新的数学假设。

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

`Arity ar F` 表示：只在命题截断下，存在自然数 `n`，使 `ar` 是 `n` 的数码，并且 `F` 是相应的编码环境集 `envSet W n`。见证 `n` 始终留在命题截断之下，因此这个类型只记录命题值证明所需的元数信息，并不为后续计算选择一个元数。

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

要取得这样的元数证据，先把环境塔中的成员 `q` 表示为对 `(ar,F)`。于是，环境塔规格连同载体等式与零标签等式，足以把该对读成只在命题截断下存在的自然数元数及其典范环境集。

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

对等式先把 `q` 的成员关系证明运输到所展示的对 `(ar,F)` 上，环境塔条目定理随后给出仍处于命题截断之下的 `Arity ar F`。这一步只抽取当前条目所需的局部元数证据，并没有定义环境塔编码的全局逆函数。

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

表的第一条顶层条件是在给定公式码定义域上的全定义性。假设 `tot` 已经给出这条条件的确切语义内容，其中每个表值只在命题截断下存在；框架引理因此可直接把它化为对象语言全定义性子句的满足证明。

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

第二条顶层条件说，每个已经表示在表中的成员都位于给定定义域的某个键之上。假设 `onc` 正是在底层集合层面陈述这一条件，因此框架引理把它化为相应对象语言子句的满足证明。

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

每条构造子子句都在同一种十二对象配置上检验。前面的字段记录这些对象：一个环境塔条目及其元数与环境集，一个公式码定义域成员及其构造子载荷，一个表条目及其取值，以及对象语言公式所需的辅助见证。

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

其余字段陈述把这些对象连成一个一致框架的关系：环境塔成员是元数与环境集组成的对；公式码属于定义域，并分解为元数、标签与载荷；表成员属于表，并分解为该公式码与其候选值。这些只是局部表示等式，并不声称唯一性，也不声称存在全局解码。

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

固定一个标签及一组一致的十二对象框架，就把问题缩小为验证单独一条构造子子句。此后这一范围内的所有论证都使用同一批对象与等式，证明因而可以专注于该标签的载荷如何决定所需的外延事实。

```agda
      module Fill (k : Fin 10) (A : Args k) where
        open Args A
```

框架依子句公式所需的精确坐标次序，把十二个对象 `yc`、`s3`、`e`、`r`、`s2`、`p`、`s1`、`c`、`F`、`ar`、`s`、`q` 添加在原环境 `γ` 之前。因此，候选取值、表项、构造子载荷、公式码、环境集、元数与环境塔条目同四个辅助见证交错排列，并且恰好落在子句所使用的索引处。

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

在这个固定框架上，标签对应的关系定理可在其语义外延条件与对象语言关系子句之间双向转换。填充证明使用构造方向：一旦解码出的载荷与给定的子公式值产生正确的外延事实，相应标签的关系子句便随之成立。

```agda
        module RR = RelRead T w N frame
```

每个填充情形的目标是在十二槽框架处、对给定标签的关系子句的满足。

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

这个目标取值于命题，因为该结构中任意公式的满足关系都是 h-命题。这正是后面使用命题截断消去的边界：只在命题截断下得到的元数、公式与构造子形状可以被用于证明此目标，却不能被抽取成可复用的计算数据。

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

转移引理是关键步骤：给定元数等式、环境集等式、公式码等式 `fst p ≡ cd ψ`，以及 `ψ` 的满足关系集合之外延事实，它便产出框架处表取值的相应外延事实。这三条等式分别把框架中的元数、环境集与公式码对象同递归满足关系集合所用的数据对齐。

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

框架中的等式先证明 `c` 是解码公式的典范键，并证明给定表成员是 `c` 与 `yc` 组成的对。取值相合假设随即把 `yc` 的底层集合认同为递归满足集。最后，证明沿这条取值等式的逆向以及 `F` 与典范环境集的等式作运输，把桥给出的外延事实化为框架所需的外延事实。

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

子取值引理把取值一致假设施于同元数的子条目，从子表条目恢复满足集。

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

对量词体而言，子公式键位于后继元数。新增的等式把其元数分量 `ar'` 认同为父公式元数分量的冯·诺伊曼后继；再与 `ar = # n` 复合，就得到 `suc n` 的数码。因此，取值相合假设可把子公式表值认同为体公式的递归满足集。这只是元数计算，并非关于可构造层级阶段的陈述。

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

数据类型收集解码出的元数、环境集、公式与标签匹配：分派构造子情形所需的一切。

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

`data'` 中的证据始终留在命题截断之下。环境塔条目先只给出某个元数及其环境集；对每个这样的见证，`decode` 又只在命题截断下给出该元数处的某个公式，`PT.map` 再用 `matchAt` 得到的构造子形状证明扩充这份数据。外层消去的目标仍是命题截断后的类型，所以整个过程没有在全局选择任何元数或公式。

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

外层命题截断消去器的最后一个实参，是从当前环境塔条目读出的局部 `Arity ar F` 证据。它启动上面的嵌套命题截断解码，却不会单独暴露其中隐藏的自然数见证。

```agda
          (arity q ar F q∈ eq)
```

对任意二元构造子，证明先把两个子公式的表值分别认同为其递归满足集。随后，二元桥用相应的对象语言联结词组合「属于这两个子满足集」的命题，从而刻画复合公式的递归满足集。这一共同论证将分别用于合取、析取与蕴涵。

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

桥的外延事实在「把二元联结词施于两个子满足集上的隶属原子」的公式处陈述。

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

载荷等式表明，框架中的载荷是两个子公式码的配对。配对的单射性分别恢复两个分量等式，`subVal` 再利用它们，把两个被表示的子公式取值分别认同为其递归定义值 `SatW` 的底层集合。

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

这两条子公式取值等式与相应的表条目一同放入扩展环境。联结词桥接据此用二元子句刻画 `SatW (opA a b)`，而 `transfer` 再把这个典范取值及环境集换成框架中已有的候选取值与环境集。

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

对于无界量化公式，递归子公式具有后继元数，而其语义量化仍在载体 `W` 上进行。因此，抽象构造子 `q'` 随后会实例化为 `∃[]-syntax` 或 `∀[]-syntax`；`qA` 表示字母表上的相应无界构造子，桥接则把它的递归满足关系集与这个由载体限定的子句联系起来。

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

该子句检验一个候选编码环境 `z`。其外层构造子随后会实例化为 `∃[]-syntax` 或 `∀[]-syntax`，并在载体 `W` 上量化；对每个这样的元素，内层的 `∃[]-syntax` 要求子公式所表示的满足关系集中存在一个成员，它正是把该元素添到 `z` 所得的编码环境。这是对象语言对一步量化的描述，并不构成解码器，也不提供可复用的见证选择。

```agda
                      (λ z → ⟨ (z ∷ env) ⊨ q' (var (suc wi)) (∃̇∈ (var (suc (suc yai))) (consAtL i0 i1 i2)) ⟩)) where
```

解码所得公式的元数是 `n`，而其量化主体的元数是 `suc n`。关系读式给出的后继等式使 `subValS` 能把主体的键改写到该元数，并把其被表示的取值认同为 `SatW a`；量词桥接由此取得该子句所需的递归子公式取值。

```agda
          go : (n : ℕ) (a : Formula Ab (suc n)) (ψ : Formula Ab n) → fst ar ≡ # n → fst F ≡ fst (envSet W n)
             → fst p ≡ cd ψ → ψ ≡ qA a → fst r ≡ cd a → ⟨ frame ⊨ R.quRel q' ⟩
          go n a ψ qa qF qp qψ qr = RR.qu-in q' (λ c₁ ya ar' s' s'' e' e'∈ ee₁ e₁' es →
            let ya≡ = subValS n a c₁ ya e' ar' qa e'∈ ee₁ (e₁' ∙ cong (pr (fst ar')) qr) es
                env = ar' ∷ s'' ∷ ya ∷ c₁ ∷ s' ∷ e' ∷ frame
```

桥接先给出典范取值 `SatW (qA a)` 的外延事实。随后，元数、环境集与公式码的等式使 `transfer` 能把该事实化为当前框架中候选表取值所需的外延陈述，从而完成无界量词子句。

```agda
            in transfer n (qA a) qa qF (qp ∙ cong cd qψ) env (R.quBody q')
                 (bridge a env (sh 18 w) i2 qw ya≡))
```

有界量化公式只有一个递归公式子项：界限词项在语义桥接内部求值。这里的抽象数据分别给出有界量词、组合各条件的联结词、字母表层的构造子以及准确的对象语言子句主体，因而同一论证既适用于全称形式，也适用于存在形式，同时不会把词项码当作子公式。

```agda
        module BqFill (q' : ∀ {j} → Term S j → Formula S (suc j) → Formula S j)
          (c' : ∀ {j} → Formula S j → Formula S j → Formula S j)
          (qA : ∀ {j} → Term Ab j → Formula Ab (suc j) → Formula Ab j)
          (body : ∀ {j} → Fin j → Fin j → Fin j → Fin j → Fin j → Formula S (1 + j))
          (bodyIs : ∀ {j} (wi ti yai N0i N1i : Fin j)
```

等式 `bodyIs` 把一般子句主体认同为三层有界结构。最外层在 `W` 中量化界限词项的候选取值，`tmIs` 验证该候选；下一层量化既属于该取值又属于 `W` 的元素；最内层用 `∃[]-syntax` 要求编码后的扩展环境属于子公式的满足关系集。这个等式描述的是语义子句主体，而不是原公式主体本身。

```agda
                  → body wi ti yai N0i N1i
                  ≡ q' (var (suc wi)) (c' (tmIs (suc (suc ti)) i1 i0 (suc (suc N0i)) (suc (suc N1i)))
                      (q' (var (suc (suc wi))) (c' (var i0 ∈̇ var i1) (∃̇∈ (var (suc (suc (suc yai)))) (consAtL i0 i1 i3))))))
          (bridge : ∀ {n} (t : Term Ab n) (a : Formula Ab (suc n)) {j : ℕ} (env : S ^ j) (wi ti yai N0i N1i : Fin j)
                  → fst (lookup wi env) ≡ Wv → fst (lookup ti env) ≡ ct t → fst (lookup yai env) ≡ fst (SatW a)
```

桥接假设五条等式，用以在同一环境中定位载体、界限词项码、公式子项的递归取值以及数码标签 `0` 与 `1`。它从这些前提证明有界公式的外延事实。因此，外延事实是桥接的结论，而唯一的递归输入是公式子项的取值。

```agda
                  → fst (lookup N0i env) ≡ # 0 → fst (lookup N1i env) ≡ # 1
                  → ExtFact (fst (SatW (qA t a))) (fst (envSet W n)) (λ z → ⟨ (z ∷ env) ⊨ body wi ti yai N0i N1i ⟩)) where
```

配对的单射性把有界量词的载荷分成词项码分量与公式码分量。第一条等式交给桥接中的词项部分；第二条等式与后继元数等式一起，使 `subValS` 能认同唯一公式子项的被表示取值。词项码不需要递归查询表。

```agda
          go : (n : ℕ) (t : Term Ab n) (a : Formula Ab (suc n)) (ψ : Formula Ab n) → fst ar ≡ # n → fst F ≡ fst (envSet W n)
             → fst p ≡ cd ψ → ψ ≡ qA t a → fst r ≡ pr (ct t) (cd a) → ⟨ frame ⊨ R.bqRel q' c' ⟩
          go n t a ψ qa qF qp qψ qr = RR.bq-in q' c' (λ t' a' s' c₁ ya ar' s₁ s'' e' er e'∈ ee₁ e₁' es →
            let q'' = pr-inj (sym er ∙ qr)
                ya≡ = subValS n a c₁ ya e' ar' qa e'∈ ee₁ (e₁' ∙ cong (pr (fst ar')) (q'' .snd)) es
```

具体桥接先在典范的有界量词主体中证明外延事实。沿 `bodyIs` 改写后，该事实落入一般关系主体；随后 `transfer` 把典范满足关系值换成表条目所表示的候选取值。

```agda
                env = ar' ∷ s'' ∷ ya ∷ c₁ ∷ s₁ ∷ e' ∷ a' ∷ t' ∷ s' ∷ frame
            in transfer n (qA t a) qa qF (qp ∙ cong cd qψ) env (R.bqBody q' c')
                   (subst (λ φ → ExtFact (fst (SatW (qA t a))) (fst (envSet W n)) (λ z → ⟨ (z ∷ env) ⊨ φ ⟩))
                     (bodyIs (sh 21 w) i7 i2 (sh 21 (N f0)) (sh 21 (N f1)))
                     (bridge t a env (sh 21 w) i7 i2 (sh 21 (N f0)) (sh 21 (N f1)) qw (q'' .fst) ya≡ (tg f0) (tg f1))))
```

原子公式含有两个词项码，却没有递归公式子项。因此，它的一般桥接由二元原子构造子以及扩展环境中的关系公式作索引；桥接直接求值两个词项，并证明相应的外延事实。

```agda
        module AtomFill (opA : ∀ {j} → Term Ab j → Term Ab j → Formula Ab j) (rel : Formula S (18 + m))
          (bridge : ∀ {n} (t u : Term Ab n) (env : S ^ (15 + m)) (wi ti ui N0i N1i : Fin (15 + m))
                  → fst (lookup wi env) ≡ Wv → fst (lookup ti env) ≡ ct t → fst (lookup ui env) ≡ ct u
                  → fst (lookup N0i env) ≡ # 0 → fst (lookup N1i env) ≡ # 1
                  → ExtFact (fst (SatW (opA t u))) (fst (envSet W n)) (λ z → ⟨ (z ∷ env) ⊨ atomEx wi ti ui N0i N1i rel ⟩)) where
```

这里的载荷等式同样是配对等式，此次分离的是两个词项的码。这两条等式把词项码放入原子主体所需的环境。真正的词项取值仍由该主体内部的两条 `tmIs` 子句量化并验证，并非通过递归查询表取得。

```agda
          go : (n : ℕ) (t u : Term Ab n) (ψ : Formula Ab n) → fst ar ≡ # n → fst F ≡ fst (envSet W n)
             → fst p ≡ cd ψ → ψ ≡ opA t u → fst r ≡ pr (ct t) (ct u) → ⟨ frame ⊨ R.atomRel rel ⟩
          go n t u ψ qa qF qp qψ qr = RR.atom-in rel (λ t' u' s' er →
            let q' = pr-inj (sym er ∙ qr)
                env = u' ∷ t' ∷ s' ∷ frame
```

加在框架前面的三个条目是载荷中的两个词项码及其配对容纳集合。两个分量等式确立后，原子桥接便用所选关系刻画典范满足关系集，`transfer` 再把该刻画搬到候选表取值上。

```agda
            in transfer n (opA t u) qa qF (qp ∙ cong cd qψ) env (R.atomBody rel)
                   (bridge t u env (sh 15 w) i1 i0 (sh 15 (N f0)) (sh 15 (N f1)) qw (q' .fst) (q' .snd) (tg f0) (tg f1)))
```

假命题既没有词项数据，也没有公式子项。相应桥接直接说明，其递归满足关系集在 `envSet W n` 上具有空外延；`transfer` 把这一事实改写到候选表取值，关系构造再把它封装为假命题子句。

```agda
        botGo : (n : ℕ) (ψ : Formula Ab n) → fst ar ≡ # n → fst F ≡ fst (envSet W n)
              → fst p ≡ cd ψ → ψ ≡ ⊥̇ → ⟨ frame ⊨ R.botRel ⟩
        botGo n ψ qa qF qp qψ = extB-in i0 i8 ⊥̇ frame
          (transfer n ⊥̇ qa qF (qp ∙ cong cd qψ) frame ⊥̇ (botBridge n frame))
```

标签 `0` 对应隶属原子。这里的关系公式在可构造结构中本来就表示通常的隶属关系，因此相符证明的两个方向，以及连接原子意义与隶属关系的两个方向，都是恒等映射。原子论证仍会先验证两个词项码及其取值，再施用该关系。

```agda
      fill : (k : Fin 10) (A : Args k) → Fill.Data k A → Fill.Goal k A
      fill f0 A (n , (qa , qF , ψ , (qp , (t , u , (qψ , qr))))) =
        Fill.AtomFill.go f0 A _∈̇_ (var i1 ∈̇ var i0)
          (λ t u env wi ti ui N0i N1i qw' qt qu q0 q1 →
            AtomBridge.atomBridge t u env wi ti ui N0i N1i qw' qt qu q0 q1 _∈̇_ (λ v x → ⟨ v ∈ x ⟩)
```

标签 `1` 对相等原子采用同一论证。对象语言的相等由层级中底层集合的相等来解释，因此相符映射与语义转换映射同样无需恒等映射以外的搬运。

```agda
              (var i1 ∈̇ var i0) (λ z v x → (λ h → h) , (λ h → h)) (λ δ h → h) (λ δ h → h))
          n t u ψ qa qF qp qψ qr
      fill f1 A (n , (qa , qF , ψ , (qp , (t , u , (qψ , qr))))) =
        Fill.AtomFill.go f1 A _≐_ (var i1 ≐ var i0)
          (λ t u env wi ti ui N0i N1i qw' qt qu q0 q1 →
```

标签 `2`、`3`、`4` 分别以合取、析取、蕴涵的桥接使用共同的二元论证；标签 `5` 则是不含子公式的假命题情形。因此，这一段分派准确遵循构造子编码，而全部递归信息只限于二元联结词所需的两个子公式取值。

```agda
            AtomBridge.atomBridge t u env wi ti ui N0i N1i qw' qt qu q0 q1 _≐_ (λ v x → v ≡ x)
              (var i1 ≐ var i0) (λ z v x → (λ h → h) , (λ h → h)) (λ δ h → h) (λ δ h → h))
          n t u ψ qa qF qp qψ qr
      fill f2 A (n , (qa , qF , ψ , (qp , (a , b , (qψ , qr))))) = Fill.BinFill.go f2 A _∧̇_ _∧̇_ andBridge n a b ψ qa qF qp qψ qr
      fill f3 A (n , (qa , qF , ψ , (qp , (a , b , (qψ , qr))))) = Fill.BinFill.go f3 A _∨̇_ _∨̇_ orBridge n a b ψ qa qF qp qψ qr
```

标签 `6` 与 `7` 表示无界存在公式和无界全称公式。相应语义子句用 `∃[]-syntax` 与 `∀[]-syntax` 在载体 `W` 上量化，并使用后继元数处的递归主体取值。余下两个标签开始处理有界情形；其中同样的有界构造子再与合取或蕴涵结合，以同时表达词项给出的界。

```agda
      fill f4 A (n , (qa , qF , ψ , (qp , (a , b , (qψ , qr))))) = Fill.BinFill.go f4 A _⇒̇_ _⇒̇_ impBridge n a b ψ qa qF qp qψ qr
      fill f5 A (n , (qa , qF , ψ , (qp , (qψ , qr)))) = Fill.botGo f5 A n ψ qa qF qp qψ
      fill f6 A (n , (qa , qF , ψ , (qp , (a , (qψ , qr))))) = Fill.QuFill.go f6 A ∃̇∈ ∃̇_ exBridge n a ψ qa qF qp qψ qr
      fill f7 A (n , (qa , qF , ψ , (qp , (a , (qψ , qr))))) = Fill.QuFill.go f7 A ∀̇∈ ∀̇_ allBridge n a ψ qa qF qp qψ qr
      fill f8 A (n , (qa , qF , ψ , (qp , (t , a , (qψ , qr))))) =
```

对于有界全称公式，典范主体已经具有 `BqFill` 所要求的抽象形状，所以 `bodyIs` 就是自反等式。嵌套的 `∀[]-syntax` 表达：界限词项的每个经验证取值，以及属于该取值的每个载体元素，都必须导向递归子公式集合中的一个编码环境。

```agda
        Fill.BqFill.go f8 A ∀̇∈ _⇒̇_ ∀̇∈ bqAll (λ _ _ _ _ _ → refl)
          (λ t a env wi ti yai N0i N1i qw' qt qa' q0 q1 → BqBridge.allInBridge t a env wi ti yai N0i N1i qw' qt qa' q0 q1)
          n t a ψ qa qF qp qψ qr
      fill f9 A (n , (qa , qF , ψ , (qp , (t , a , (qψ , qr))))) =
        Fill.BqFill.go f9 A ∃̇∈ _∧̇_ ∃̇∈ bqEx (λ _ _ _ _ _ → refl)
```

有界存在公式使用与之平行的三层主体，其中以 `∃[]-syntax` 量化，并用合取连接词项取值条件、元素属于该取值，以及扩展环境属于子公式集合这三项条件。它的主体同样由自反等式匹配，标签 `9` 至此完成十种构造子情形。

```agda
          (λ t a env wi ti yai N0i N1i qw' qt qa' q0 q1 → BqBridge.exInBridge t a env wi ti yai N0i N1i qw' qt qa' q0 q1)
          n t a ψ qa qF qp qψ qr
```

为证明一条构造子子句，先把十二个对象及其隶属与配对等式汇集为 `Args k`，从而固定一个匹配框架。解码出的元数、公式与构造子形状仍留在 `Fill.data'` 的命题截断之内，因为原有前提并未选择其中任何一项。

```agda
      clause : (k : Fin 10) → ⟨ γ ⊨ Cl.clause k ⟩
      clause k = Fr.clause-in k (λ q ar F s c p s1 r s2 e yc s3 q∈ eq c∈ ec ep e∈ ee →
        let A : Args k
            A = record { q = q ; ar = ar ; F = F ; s = s ; c = c ; p = p ; s1 = s1 ; r = r ; s2 = s2 ; e = e ; yc = yc ; s3 = s3
                       ; q∈ = q∈ ; eq = eq ; c∈ = c∈ ; ec = ec ; ep = ep ; e∈ = e∈ ; ee = ee }
```

公式的满足是命题，所以 `Fill.Goal k A` 可以作为消去命题截断数据的目标。对于其中每份被隐藏的见证，`fill` 都证明同一个子句目标；目标的命题性保证结果不依赖哪一个元数、公式或分解见证了解码。此次消去不会产生可重复使用的解码器，也不会给出表取值的选择。

```agda
        in PT.rec (Fill.isPropGoal k A) (fill k A) (Fill.data' k A))
```

十条构造子子句被连成一个有穷合取。这个合取是完整表规格中的 `ten` 分量；全定义性与定义域约束将在下一步另行加入。

```agda
      ten : ⟨ γ ⊨ Cl.ten ⟩
      ten = bigAnd-in γ 9 Cl.clause clause
```

这三部分现在恰好组成 `tableAt` 的定义：`total` 对 `C` 中每个码给出经过命题截断的表取值存在性，`onC` 说明每个表成员的键都属于 `C`，`ten` 则给出全部构造子子句。三者共同证明给定关系满足表规格，但不宣称它是全局选定的函数，也不在此证明其取值唯一。

```agda
    holds : ⟨ γ ⊨ tableAt T w C E N ⟩
    holds = total , (onC , ten)
```

## 专门用于单个公式的槽位

固定 `W` 后便得到两个相互联系的视角。`Alphabet W` 给出常元命名 `W` 中元素的公式及其编码，`Bridge W` 则在可构造载体中解释这些常元，并比较递归满足关系与对象语言子句。下面的特化会把这两个视角同时用于一条公式生成的槽位。

```agda
module _ (W : S) where
  open Alphabet W
  open Bridge W
```

若 `x` 属于 `ψ` 生成的槽位，那么在命题截断下，存在元数 `m` 与公式 `χ : Formula Ab m`，使 `x` 等于 `keyS W χ` 的底层集合。该结论保留这样一个公式键的存在性，却不选择具体公式，也不保留 `χ` 是 `ψ` 的子公式的显式证明。

```agda
  slotAb : ∀ {n} (ψ : Formula Ab n) (x : V ℓ)
         → ⟨ x ∈ fst (slot W (toS ψ)) ⟩
         → ∥ Σ[ m ∈ ℕ ] Σ[ χ ∈ Formula Ab m ] (x ≡ fst (keyS W χ)) ∥₁
  slotAb ψ x h = PT.map
    (λ { (m , χ , e , _) → m , χ , (e ∙ sym (keyBridge W χ)) })
```

局部等式 `mapped ψ` 先把具体槽位改写为收集 `keyʟ (toS χ)` 的一般树。随后施用 `tree-inv`，在命题截断下得到贡献该成员的公式 `χ` 及其与这个内部键的等式。映射保留该等式，再用 `keyBridge` 把内部键换成 `keyS W χ`；所得结论有意舍弃了相伴的子树包含证明。

```agda
    (tree-inv key key ψ x (subst (λ y → ⟨ x ∈ fst y ⟩) (mapped ψ) h))
    where
    key : ∀ {n} → Formula Ab n → S
    key χ = keyʟ (toS χ)
```

等式 `mapped` 由结构递归证明，因为 `toS` 只改变常元，并保留每个公式构造子。隶属原子、相等原子与假命题的两种表示按定义相同。对于二元联结词，槽位由含有公式自身键的单元素集合与两棵子树的并组成，所以两条递归等式在相同的并运算下组合起来。

```agda
    mapped : ∀ {n} (χ : Formula Ab n) → slot W (toS χ) ≡ tree key χ
    mapped (t ∈̇ u) = refl
    mapped (t ≐ u) = refl
    mapped ⊥̇ = refl
    mapped χ@(a ∧̇ b) = cong (cupʟ (sglʟ (key χ))) (cong₂ cupʟ (mapped a) (mapped b))
```

合取、析取与蕴涵具有相同的二叉树形状，因此都使用两条递归等式。每个无界量词只有一个公式主体，所以其根部单元素集合只与一棵经递归匹配的子树取并。约束子下的元数变化会改变该子公式的类型，却不改变这种取并模式。

```agda
    mapped χ@(a ∨̇ b) = cong (cupʟ (sglʟ (key χ))) (cong₂ cupʟ (mapped a) (mapped b))
    mapped χ@(a ⇒̇ b) = cong (cupʟ (sglʟ (key χ))) (cong₂ cupʟ (mapped a) (mapped b))
    mapped χ@(∃̇ a) = cong (cupʟ (sglʟ (key χ))) (mapped a)
    mapped χ@(∀̇ a) = cong (cupʟ (sglʟ (key χ))) (mapped a)
    mapped χ@(∀̇∈ t a) = cong (cupʟ (sglʟ (key χ))) (mapped a)
```

有界全称与有界存在情形同样只把公式主体作为子树加入。它们的界限词项属于构造子的载荷，并不是 `slot` 所收集的公式子树。最后两条递归等式完成具体槽位与一般键树之间的比较。

```agda
    mapped χ@(∃̇∈ t a) = cong (cupʟ (sglʟ (key χ))) (mapped a)
```

`SlotHolds` 在一个环境中工作，其中 `T`、`w`、`C`、`E` 分别是表、载体、码定义域与环境塔的位置，另有十个标签位置 `N`。它假设载体、标签与环境塔的事实，再固定基公式 `ψ0`；等式 `qT` 与 `qC` 只把 `T`、`C` 处存放的底层集合分别认同为 `ψ0` 生成的典范表与槽位。

```agda
  module SlotHolds {m : ℕ} (T w C E : Fin m) (N : Fin 10 → Fin m) (γ : S ^ m)
    (qw : fst (lookup w γ) ≡ fst W) (tg : Tags γ N)
    (hE : ⟨ γ ⊨ towerAt E w (N f0) ⟩) {n0 : ℕ} (ψ0 : Formula Ab n0)
    (qT : fst (lookup T γ) ≡ fst (satTable W (toS ψ0)))
    (qC : fst (lookup C γ) ≡ fst (slot W (toS ψ0))) where
```

这里仅缩写两个底层集合：`Tv` 是表位置 `T` 所存放的关系，`Cv` 是码定义域位置 `C` 所存放的集合。随后四项构造将准确建立这两个集合所需的取值相符、解码、全定义性与定义域约束前提。

```agda
    private
      Tv = fst (lookup T γ)
      Cv = fst (lookup C γ)
```

设 `c` 的底层集合等于公式 `ψ` 的键，且 `(c,yc)` 在 `Tv` 中被表示。沿 `keyBridge` 与 `qT` 改写后，它成为 `ψ0` 生成的典范表中的一个条目；`entry-out` 因而证明 `fst yc ≡ fst (SatW ψ)`。该结论固定了真实公式键处一个已经给出的取值，却不宣称这样的条目必然存在。

```agda
      val≡ : ∀ {n} (ψ : Formula Ab n) (c yc : S) → fst c ≡ fst (keyS W ψ)
           → ⟨ pr (fst c) (fst yc) ∈ Tv ⟩ → fst yc ≡ fst (SatW ψ)
      val≡ ψ c yc qc h = entry-out W (toS ψ0) (toS ψ) (fst yc)
        (subst2 (λ u v → ⟨ pr u (fst yc) ∈ v ⟩) (qc ∙ keyBridge W ψ) qT h)
```

解码同时从成员关系 `c ∈ Cv` 与指定的元数表示 `fst c ≡ pr (# n) z` 出发。沿 `qC` 搬运成员关系后，`slotAb` 在命题截断下给出某个元数处的一条公式，其键为 `c`。余下工作必须证明这个被隐藏的元数恰为 `n`，且该公式码恰为 `z`。

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

关于 `c` 的两条等式给出一条配对等式。配对的单射性分别比较数码分量与公式码分量，数码的单射性再推出两个元数相等。由于公式以元数为索引，必须沿这条等式搬运被隐藏的公式；`cd-subst` 随后说明其编码在这次依赖搬运下如何变化，最终得到 `Formula Ab n` 中公式码为 `z` 的公式。

```agda
              nq = #-inj′ (q .fst)
          in subst (Formula Ab) nq ψ₁ , (sym (q .snd) ∙ sym (cd-subst nq ψ₁)) })
        (slotAb ψ0 (fst c) (subst (λ u → ⟨ fst c ∈ u ⟩) qC c∈))
```

对每个 `c ∈ Cv`，沿 `qC` 搬运可把 `c` 放入典范槽位；`slotTotal` 随即在命题截断下给出取值 `y`，使它与 `c` 的配对属于典范表。再沿 `qT` 搬运，便把该条目送回 `Tv`。所得结论只以存在性证明全定义性，并未在 `Cv` 上选择取值函数。

```agda
      tot : (c : S) → ⟨ fst c ∈ Cv ⟩ → ∥ Σ[ yc ∈ S ] ⟨ pr (fst c) (fst yc) ∈ Tv ⟩ ∥₁
      tot c c∈ = PT.map
        (λ { (y , h) → y , subst (λ u → ⟨ pr (fst c) (fst y) ∈ u ⟩) (sym qT) h })
        (slotTotal W (toS ψ0) (fst c) (subst (λ u → ⟨ fst c ∈ u ⟩) qC c∈))
```

对于 `Tv` 的成员 `e`，等式 `qT` 先把其成员关系搬到典范满足关系表。求逆引理 `ent-slot` 随后在命题截断下给出元数 `m`、公式 `χ`，以及 `fst e` 与 `χ` 所贡献典范条目的底层集合之间的等式。再把这条等式与 `prʟ-fst` 复合，便得到 `fst e ≡ pr (fst (keyʟ χ)) (fst (Sat W χ))`。

```agda
      onc : (e : S) → ⟨ fst e ∈ Tv ⟩
          → ∥ Σ[ c ∈ S ] Σ[ yc ∈ S ] ((fst e ≡ pr (fst c) (fst yc)) × ⟨ fst c ∈ Cv ⟩) ∥₁
      onc e e∈ = PT.map
        (λ { (m , χ , (q , _)) →
          let ee = q ∙ prʟ-fst (keyʟ χ) (Sat W χ)
```

在这份命题截断的见证内部，取 `c = keyʟ χ`、`yc = Sat W χ`。刚得到的等式给出 `e` 所需的分解；把 `e` 的成员关系搬入典范表后，`inSlot` 推出该键属于典范槽位，`qC` 再把这一事实送入 `Cv`。由此在同一命题截断下建立定义域约束，而没有全局选择分解，也没有证明单值性。

```agda
          in keyʟ χ , Sat W χ , (ee , subst (λ u → ⟨ fst (keyʟ χ) ∈ u ⟩) (sym qC)
               (inSlot W (toS ψ0) (fst (keyʟ χ)) (fst (Sat W χ))
                 (subst2 (λ u v → ⟨ u ∈ v ⟩) ee qT e∈))) })
        (ent-slot W (toS ψ0) (fst e) (subst (λ u → ⟨ fst e ∈ u ⟩) qT e∈))
```

现在把共同的载体、标签、环境塔前提与刚证明的四项事实合在一起：取值相符、解码、全定义性与定义域分解。这恰是 `SatHoldsC` 的七项前提。这个方向不需要封闭性，因为重建某条构造子子句时，关系子句以全称方式给出每个相符的子公式表条目，而 `val≡` 直接钉扎其中已经给出的子公式取值。解码器处理当前的定义域码，`tot` 与 `onc` 则建立另外两项顶层表条件；此处没有任何一步需要从父公式键的成员关系推出子公式键的成员关系。

```agda
      module SH = SatHoldsC W T w C E N γ qw tg hE val≡ decode tot onc
```

因此，由 `qC` 与 `qT` 认同为 `ψ0` 所生成槽位和满足关系表的对象满足 `tableAt T w C E N`。这个结论仅是具体的表规格：它既不证明槽位封闭，也不把每张满足该规格的表都认同为典范表。后续章节在需要被表示键处的唯一性时，另行加入 `slotClosed` 并施用 `SatSoundC.pinned`。

```agda
    holds : ⟨ γ ⊨ tableAt T w C E N ⟩
    holds = SH.holds
```

## 回顾

钉住递归把外部给定的表规格转化为关于典范满足关系表的定理，也反过来证明典范表满足这份规格。证明中的数学职责彼此分明：解码负责认出公式码，全定义性仅给出取值的存在性，定义域约束说明表中每个条目的来源，而封闭性只在必须由已经表示的父公式键追回子公式键的方向出现。