---
title: "参数抽象"
module: FOL.Manipulation.ParameterAbstraction
lang: zh
site: "Bedrock"
description: "参数抽象"
stage: "一阶逻辑"
reading_order: 18
canonical: https://bedrock.institute/zh/FOL.Manipulation.ParameterAbstraction.html
html: FOL.Manipulation.ParameterAbstraction.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/FOL/Manipulation/ParameterAbstraction.lagda.md
prerequisites: [Base.Prelude, FOL.ZFStructure, FOL.Syntax, FOL.Semantics, FOL.Manipulation.ConstantOccurrences]
routes: [fol-operations]
translations: [https://bedrock.institute/en/FOL.Manipulation.ParameterAbstraction.md, https://bedrock.institute/ja/FOL.Manipulation.ParameterAbstraction.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
# 参数抽象

带常元的公式可通过将每次常元出现替换为新变量，并把这些常元记录在向量中，转成无参公式。通过环境供给该向量会保持满足关系，从而使带参数公式可用于后续符号化论证。

本章构造这个替换本身。FOL.Manipulation.ConstantOccurrences 中的出现计数决定了需要多少个新变量，而安置决定每次出现获得哪个变量位。替换只做一次结构遍历；章末的充分性定理识别替换前后的满足关系，这正是后续对公式符号化时所依赖的事实。

公式的章首引言常常需要常元：要说集合 $a$ 可由参数定义，人们会写下提到 $a$ 的公式。但对编码论证而言，只使用无参公式会更方便。参数抽象正是使这成为可能的翻译：把每次常元出现换成新变量，并把诸常元记录在一个向量中，交给环境供给。

这个替换按出现逐一进行，而不是按常元本身。若常元 $c$ 出现两次，它就被记录两次、获得两个变量。按出现记录意味着翻译无须判断两个名字是否相等，因此字母表 `K` 不需要可判定相等；常元出现一章的位置计数完成了全部簿记。

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

module FOL.Manipulation.ParameterAbstraction where

open import Base.Prelude
open import FOL.ZFStructure using ( ZFStructure )
```

具体地，这个翻译消耗「逐次出现地处理常元」一章准备好的两份数据：常元出现的数目，它决定需要多少个新变量；以及记录下来的常元向量，它决定这些变量在解释之后代表什么。替换本身由一个安置描述，即一个函数，决定每次出现获得哪个变量位。

整个构造是对公式的一次结构性遍历。章末证明的充分性定理把原公式在常元解释下的满足，与抽象在扩张环境下的满足等同起来；后续编码论证所依赖的正是这一等同。

```agda
open import FOL.Syntax using
  ( Term; con; var
  ; Formula; _∈̇_; _≐_; _∧̇_; _∨̇_; _⇒̇_; ⊥̇; ∃̇_; ∀̇_; ∀̇∈; ∃̇∈ )
import FOL.Semantics
open import FOL.Manipulation.ConstantOccurrences using
```

由于每次常元出现都成为变量，翻译后的公式完全不含常元：它定义在一个没有成员的字母表上。代码以空类型 `⊥*` 充当这个字母表。永远不会向它索要解释，因为无可解释之物；这个类型只需存在，使翻译后的语法有一个良构的载体。

```agda
  ( countTm; countFo; constantsTm; constantsFo; padRight; padLeft
  ; lookup-padRight; lookup-padLeft; lookup-map )
open import Cubical.Data.Nat using ( _+_ )
open import Cubical.Data.Vec using ( _++_; map )
import Cubical.Data.Empty as Empty
```

## 抽象

安置为每次常元出现指派较大语境中的一个变量。`placeFo` 按结构执行替换，而 `absFo` 选择原自由变量之后的连续区块，其长度正是出现次数。

遍历针对任意安置 `θ` 陈述，这种泛型是递归强加的：子公式处使用的安置就在遍历内部产生，归纳假设因此必须对所有安置成立。让 `θ` 保持抽象也使充分性证明保持模块化。本节先对词项、再对公式构造这两个遍历。

替换的一般形式是一个遍历，除公式外还接受一个安置 `θ : Fin (countTm t) → Fin (n + k)`：它按计数章枚举的次序读取 `t` 的诸出现位，并为每一次出现指名 `n + k` 个可用位中的一个，其中 `n` 个是原自由变量，`k` 个是新的参数位。输出是空字母表 `⊥*` 上的词项，因为没有常元存活下来。

```agda
placeTm : ∀ {ℓz ℓc} {K : Type ℓc} {n k} (t : Term K n)
        → (Fin (countTm t) → Fin (n + k)) → Term (⊥* {ℓz}) (n + k)
placeTm         (con c) θ = var (θ zero)
placeTm {k = k} (var i) θ = var (padRight k i)

placeFo : ∀ {ℓz ℓc} {K : Type ℓc} {n k} (φ : Formula K n)
```

词项的两个情形展示了两种手法。常元 `con c` 恰有一次出现，即第零位，安置指出由哪个变量取代它：`var (θ zero)`。变量 `var i` 不贡献出现，故安置不被使用，但语境已从 `n` 增长为 `n + k`，旧序号必须重新嵌入：`padRight k` 把 `i` 送到前 `n` 个位中的同一位，由补位定律，它在拼接环境中仍取原值。

```agda
        → (Fin (countFo φ) → Fin (n + k)) → Formula (⊥* {ℓz}) (n + k)
placeFo (t ∈̇ u)  θ = placeTm t (λ i → θ (padRight (countTm u) i))
                   ∈̇ placeTm u (λ j → θ (padLeft (countTm t) j))
placeFo (t ≐ u)  θ = placeTm t (λ i → θ (padRight (countTm u) i))
                   ≐ placeTm u (λ j → θ (padLeft (countTm t) j))
```

在二元节点处出现表发生分裂，安置算术由此登场。考虑原子 `t ∈̇ u`，取 `t = con c`、`u = con d`：出现表是 `c ∷ d ∷ []`，`c` 在序号 0，`d` 在序号 1。于是左词项须经 `padRight` 读取安置，跳过属于 `u` 的 `countTm u` 个位；右词项须经 `padLeft` 读取，跨过属于 `t` 的 `countTm t` 个位。这样每个子词项看到的都是作用于自身出现位的安置，两个翻译后的子词项以原来的联结词重新组合。

```agda
placeFo (φ ∧̇ ψ)  θ = placeFo φ (λ i → θ (padRight (countFo ψ) i))
                   ∧̇ placeFo ψ (λ j → θ (padLeft (countFo φ) j))
placeFo (φ ∨̇ ψ)  θ = placeFo φ (λ i → θ (padRight (countFo ψ) i))
                   ∨̇ placeFo ψ (λ j → θ (padLeft (countFo φ) j))
placeFo (φ ⇒̇ ψ)  θ = placeFo φ (λ i → θ (padRight (countFo ψ) i))
```

公式遍历以结构递归推广了这个例子。每个由两部分构成的构造子，无论原子还是命题联结词，都恰以这种方式分裂其出现表：第一个因子的出现在前，第二个的在后，故左支的遍历把 `θ` 与越过右侧计数的 `padRight` 复合，右支则与越过左侧计数的 `padLeft` 复合。假值 `⊥̇` 没有任何出现，翻译为自身。没有哪条子句需要第二次遍历或改名引理：在递归之前先复合安置，使整个翻译保持为一次结构性遍历。

```agda
                   ⇒̇ placeFo ψ (λ j → θ (padLeft (countFo φ) j))
placeFo ⊥̇        θ = ⊥̇
placeFo (∃̇ φ)    θ = ∃̇ placeFo φ (λ j → suc (θ j))
placeFo (∀̇ φ)    θ = ∀̇ placeFo φ (λ j → suc (θ j))
placeFo (∀̇∈ t φ) θ = ∀̇∈ (placeTm t (λ i → θ (padRight (countFo φ) i)))
```

在约束子之下语境增一，这是第二种反复出现的手法。在 `∃̇∈ t φ` 中，语义求值公式体时会把界定变量前置到环境左侧，故每个参数位都上移一：公式体在安置 `suc ∘ θ` 之下遍历，再经 `padLeft` 越过词项的出现而调整；词项本身则以越过公式体出现的 `padRight` 安置在前段。无界量词 `∃̇` 与 `∀̇` 只带移位。这些子句合起来覆盖了全部十个公式构造子。

```agda
                        (placeFo φ (λ j → suc (θ (padLeft (countTm t) j))))
placeFo (∃̇∈ t φ) θ = ∃̇∈ (placeTm t (λ i → θ (padRight (countFo φ) i)))
                        (placeFo φ (λ j → suc (θ (padLeft (countTm t) j))))
```

本书余下部分使用的实例取如下参数：参数位的数目恰好等于出现次数，安置则取紧随原变量之后的那一段。这就是所需的抽象，其类型可以概括为：`K` 上带 `n` 个自由变量的公式，变为带 `n + countFo φ` 个自由变量的无参公式。

`padLeft n` 恰是把出现 `j` 送到第 `n + j` 位的那个安置，于是每个被记录的常元、按 `constantsFo φ` 列出它们的次序，分别获得原变量之后第一个空闲位。除此之外无须再做任何选择。

定义只是一次调用：`absFo φ = placeFo φ (padLeft n)`。全部序号算术都已折入遍历之中，抽象本身没有任何情形需要处理。由于预算恰等于计数，安置实际上给出了出现位与参数位之间的双射，不过代码从不需要把这一点说出来。

```agda
absFo : ∀ {ℓz ℓc} {K : Type ℓc} {n} (φ : Formula K n) → Formula (⊥* {ℓz}) (n + countFo φ)
absFo {n = n} φ = placeFo φ (padLeft n)
```

## 充分性

充分性比较常元解释下的原公式与扩展变量环境下的抽象公式。只要安置后的每个变量都带有其所记录常元的解释，词项释义与公式满足关系便依结构归纳相符。

这一比较在载体为 `S` 的结构 `𝒮` 内、在原常元的一个解释 `ι : K → S` 之下陈述。两种语义读法并排建立：`_⊨_` 与 `⟦_⟧` 对应 `K` 上、`ι` 之下的公式与词项；其更名副本 `_⊨₀_`、`⟦_⟧₀` 对应抽象的常元域 `⊥*`。无参一侧不需要真正的解释，因为 `⊥*` 为空，但语义模块要求这份资料，`Empty.rec*` 空虚地供给了它。

充分性是说抽象不改变意义。它比较同一公式的两种求值：`K` 上的原语法、其常元由映射 `ι : K → S` 解释；对空字母表上的翻译语法，在拼接环境 `γ ++ σ` 中求值，其中 `γ` 存放原自由变量的值，`σ` 存放所记录常元的解释。这里 `S` 是命题值结构 `𝒮` 的载体，`S ^ n` 是长度为 `n` 的环境的类型。

```agda
module _ {ℓ} (𝒮 : ZFStructure ℓ) where

  open ZFStructure 𝒮

  private module Sem = FOL.Semantics 𝒮
  open Sem using ( _^_ )
```

这一比较只依赖一条连接两侧的假设：对每次出现，安置所指名的变量持有该处所记录常元的解释，即 `lookup (θ j) (γ ++ σ) ≡ ι (lookup j (constantsFo φ))`。以下的一切都是在此假设之下对语法的结构归纳。由于翻译后的语法定义在空字母表上，其读法 `_⊨₀_` 与 `⟦_⟧₀` 不需要真正的常元解释，尽管语义模块要求这份资料；空类型的消去空虚地供给了它。

```agda
  module _ {ℓz ℓc} {K : Type ℓc} (ι : K → S) where

    open Sem.At K ι using ( _⊨_; ⟦_⟧ )
    open Sem.At (⊥* {ℓz}) Empty.rec* using ()
      renaming ( _⊨_ to _⊨₀_ ; ⟦_⟧ to ⟦_⟧₀ )
```

这一陈述对安置是泛型的，也必须如此，因为递归中的诸安置是在递归调用处产生的。它陈述在**变元**环境 `γ` 与**变元**参数环境 `σ` 处，受一条假设约束：在每次出现处，安置所指名的那个位置存放着在该处记录的诸常元的解释。这条假设就是「常元由环境供给」的全部内容；把它取作假设、而不是代入一个具体环境，正是让每条子句都不必归一化一个向量的原因。

对由两部分构成的构造子，唯一要做的处理就是拆分这条假设，拆出的每一半各与补位定律复合一次。

归纳的不变量是关于完整出现向量的假设 `h`，唯一的新工作是在二元构造子把该向量分成左半 `p` 与右半 `q` 时拆分它。设 `h` 说在 `γ ++ σ` 中，位 `θ j` 存放 `p ++ q` 第 `j` 个条目的解释。左运算项只需要 `j` 小于 `p` 长度的那些序号，而经越过 `q` 的 `padRight` 读取这样的序号恰恢复 `p` 的对应条目：`lookup-padRight` 正是这条定律。把它与 `h` 复合、再施加 `ι`，便得到递归调用所需的左前提。

```agda
    private
      leftHalf : ∀ {n k a b} (θ : Fin (a + b) → Fin (n + k))
                 (γ : S ^ n) (σ : S ^ k) (p : Vec K a) (q : Vec K b)
               → (∀ j → lookup (θ j) (γ ++ σ) ≡ ι (lookup j (p ++ q)))
               → (∀ i → lookup (θ (padRight b i)) (γ ++ σ) ≡ ι (lookup i p))
```

右半是其镜像：`q` 的序号经 `padLeft` 读取，它恰跨过 `p` 的 `a` 个位，而 `lookup-padLeft` 把在拼接中读到的条目等同于 `q` 的对应条目。注意 `a` 在 `rightHalf` 中是显式参数，而在 `leftHalf` 中是隐式的：安置的定义域 `Fin (a + b)` 本身不足以确定 `a`，而 `padLeft` 必须被确切告知要跨过多少个位。

```agda
      leftHalf θ γ σ p q h i = h (padRight _ i) ∙ cong ι (lookup-padRight p q i)

      rightHalf : ∀ {n k} a {b} (θ : Fin (a + b) → Fin (n + k))
                  (γ : S ^ n) (σ : S ^ k) (p : Vec K a) (q : Vec K b)
                → (∀ j → lookup (θ j) (γ ++ σ) ≡ ι (lookup j (p ++ q)))
                → (∀ j → lookup (θ (padLeft a j)) (γ ++ σ) ≡ ι (lookup j q))
```

有了 `leftHalf` 与 `rightHalf`，拆分的不变量便一劳永逸地建立起来。下面归纳的每条二元子句都经这两个引理之一限制合并的假设，此后再没有子句需要查看拼接环境的内部。

```agda
      rightHalf a θ γ σ p q h j = h (padLeft a j) ∙ cong ι (lookup-padLeft a p q j)
```

先看词项，两个情形都立即成立。常元的取值正是假设所述那个位置上的解释；变量的取值不变，补位定律保证它在扩张后的环境中仍取原值。

归纳从词项开始，这里不变量已经完成了全部工作。命题是：只要 `h` 正确填好诸安置位，`t` 在解释 `ι` 之下于 `γ` 中的取值，就等于翻译后的词项在空字母表上于 `γ ++ σ` 中的取值。对常元 `con c`，翻译是 `var (θ zero)`，它在 `γ ++ σ` 中的取值是 `lookup (θ zero) (γ ++ σ)`；假设 `h zero` 把它等同于 `ι c`，这恰是命题，只是等式的方向相反。

```agda
    ⟦⟧-place : ∀ {n k} (t : Term K n) (θ : Fin (countTm t) → Fin (n + k))
               (γ : S ^ n) (σ : S ^ k)
             → (∀ j → lookup (θ j) (γ ++ σ) ≡ ι (lookup j (constantsTm t)))
             → ⟦ t ⟧ γ ≡ ⟦ placeTm t θ ⟧₀ (γ ++ σ)
    ⟦⟧-place (con c) θ γ σ h = sym (h zero)
```

对变量 `var i`，没有任何东西被替换，只是重新编号：翻译把它移到 `padRight k i`，即较宽语境中的同一位，补位定律表明在 `γ ++ σ` 中查出即可恢复原值。常元与变量两个情形解决后，其余构造子要么是由拆分不变量处理的二元节点，要么是约束子，公式层面的归纳遵循同一模式。

```agda
    ⟦⟧-place (var i) θ γ σ h = sym (lookup-padRight γ σ i)
```

然后是归纳的十二个情形：十个公式情形在此处理，两个词项情形刚刚证毕。命题的每条原语子句都是同余，因为语义为每个构造子指派的恰是相应的逻辑运算，中间无须任何转换。四条约束子句向环境添加一个取值，并在扩张后的环境处援引归纳假设，而关于诸参数位的那条假设**原样**适用：左侧的前置与安置的 `suc` 移位由计算相互抵消，于是约束子不需要自己的引理。两条有界子句照它们的构造子那样一分为二，词项在左，公式体在右。

公式层面的陈述 `⊨-place` 与词项引理形状相同，只是以满足关系取代取值：在关于诸安置位的假设 `h` 之下，`(γ ⊨ φ)` 等于 `((γ ++ σ) ⊨₀ placeFo φ θ)`。代表性的原子是属于关系 `t ∈̇ u`：原子的满足是两个词项取值沿结构所属关系的同余，故该子句在遍历实际使用的安置处对两个运算项各施词项引理。

```agda
    ⊨-place : ∀ {n k} (φ : Formula K n) (θ : Fin (countFo φ) → Fin (n + k))
              (γ : S ^ n) (σ : S ^ k)
            → (∀ j → lookup (θ j) (γ ++ σ) ≡ ι (lookup j (constantsFo φ)))
            → (γ ⊨ φ) ≡ ((γ ++ σ) ⊨₀ placeFo φ θ)
    ⊨-place (t ∈̇ u) θ γ σ h = cong₂ _∈ˢ_
```

每个运算项的假设恰由拆分不变量供给：针对 `constantsTm t ++ constantsTm u` 的合并假设 `h`，左侧经 `padRight` 限制，右侧经 `padLeft` 限制。相等原子 `t ≐ u` 的处理完全相同，只是以结构的相等 `≈ˢ` 代替属于；随后的命题联结词只需把词项引理换成公式层归纳。

```agda
      (⟦⟧-place t (λ i → θ (padRight (countTm u) i)) γ σ
        (leftHalf θ γ σ (constantsTm t) (constantsTm u) h))
      (⟦⟧-place u (λ j → θ (padLeft (countTm t) j)) γ σ
        (rightHalf (countTm t) θ γ σ (constantsTm t) (constantsTm u) h))
    ⊨-place (t ≐ u) θ γ σ h = cong₂ _≈ˢ_
```

合取是第一条纯命题子句。语义把 `φ ∧̇ ψ` 的满足定义为将命题合取 `_⊓_` 施于两个满足值，故该子句是在两条归纳假设之下的 `cong₂ _⊓_`，其中 `h` 在 `constantsFo φ` 与 `constantsFo ψ` 之间拆分。证明只把 `(γ ⊨ φ) ⊓ (γ ⊨ ψ)` 当作 `hProp ℓ` 中的命题，并且只使用同余，不假定它具有对的表示，也不将其拆解。

```agda
      (⟦⟧-place t (λ i → θ (padRight (countTm u) i)) γ σ
        (leftHalf θ γ σ (constantsTm t) (constantsTm u) h))
      (⟦⟧-place u (λ j → θ (padLeft (countTm t) j)) γ σ
        (rightHalf (countTm t) θ γ σ (constantsTm t) (constantsTm u) h))
    ⊨-place (φ ∧̇ ψ) θ γ σ h = cong₂ _⊓_
```

析取以命题析取 `⊔` 重复同一模式，蕴涵则使用其蕴涵运算 `⇒`。三条命题子句只在 `cong₂` 所施加的逻辑运算上不同；包括拆分后的假设在内，其余完全一致。

```agda
      (⊨-place φ (λ i → θ (padRight (countFo ψ) i)) γ σ
        (leftHalf θ γ σ (constantsFo φ) (constantsFo ψ) h))
      (⊨-place ψ (λ j → θ (padLeft (countFo φ) j)) γ σ
        (rightHalf (countFo φ) θ γ σ (constantsFo φ) (constantsFo ψ) h))
    ⊨-place (φ ∨̇ ψ) θ γ σ h = cong₂ _⊔_
```

至此值得把这个模式一次性说清：余下的每条子句，要么在其构造子所对应的逻辑运算处施加同余，要么向环境添加一个取值后递归。没有哪条子句需要新的想法。

```agda
      (⊨-place φ (λ i → θ (padRight (countFo ψ) i)) γ σ
        (leftHalf θ γ σ (constantsFo φ) (constantsFo ψ) h))
      (⊨-place ψ (λ j → θ (padLeft (countFo φ) j)) γ σ
        (rightHalf (countFo φ) θ γ σ (constantsFo φ) (constantsFo ψ) h))
    ⊨-place (φ ⇒̇ ψ) θ γ σ h = cong₂ _⇒_
```

假值印证了这一点。无论环境或安置如何，等式两边都是假命题 `⊥`，故该子句就是 `refl`。它也是唯一一个翻译后根本不提及参数块的构造子。

```agda
      (⊨-place φ (λ i → θ (padRight (countFo ψ) i)) γ σ
        (leftHalf θ γ σ (constantsFo φ) (constantsFo ψ) h))
      (⊨-place ψ (λ j → θ (padLeft (countFo φ) j)) γ σ
        (rightHalf (countFo φ) θ γ σ (constantsFo φ) (constantsFo ψ) h))
    ⊨-place ⊥̇       θ γ σ h = refl
```

无界量词 `∃̇ φ` 是约束子情形，其内容是移位相互抵消。遍历把公式体置于 `suc ∘ θ` 之下，因为把界定值前置到左侧使每个参数位上移一；语义则对 `x ∷ γ` 量化。于是递归命题在 `x ∷ γ` 处被援引，在那里 `lookup (suc (θ j)) (x ∷ γ ++ σ)` 由计算化归为 `lookup (θ j) (γ ++ σ)`，恰是 `h`。这个抵消是定义性的，因此证明中不出现任何移位引理。

```agda
    ⊨-place (∃̇ φ)   θ γ σ h = cong (λ P → ∃[ x ∶ S ] P x) (funExt (λ x →
      ⊨-place φ (λ j → suc (θ j)) (x ∷ γ) σ h))
    ⊨-place (∀̇ φ)   θ γ σ h = cong (λ P → ∀[ x ∶ S ] P x) (funExt (λ x →
      ⊨-place φ (λ j → suc (θ j)) (x ∷ γ) σ h))
    ⊨-place (∀̇∈ t φ) θ γ σ h = cong (λ P → ∀[ x ∶ S ] P x) (funExt (λ x → cong₂ _⇒_
```

全称量词 `∀̇` 的论证相同，只是以代数的全称量化运算 `∀[ x ] P x` 代替存在量化运算 `∃[ x ] P x`；外层的 `cong` 是唯一指名该运算之处，其下的归纳毫无二致。

```agda
      (cong (x ∈ˢ_) (⟦⟧-place t (λ i → θ (padRight (countFo φ) i)) γ σ
        (leftHalf θ γ σ (constantsTm t) (constantsFo φ) h)))
      (⊨-place φ (λ j → suc (θ (padLeft (countTm t) j))) (x ∷ γ) σ
        (rightHalf (countTm t) θ γ σ (constantsTm t) (constantsFo φ) h))))
    ⊨-place (∃̇∈ t φ) θ γ σ h = cong (λ P → ∃[ x ∶ S ] P x) (funExt (λ x → cong₂ _⊓_
```

有界量词把两种手法合起来。对 `∀̇∈ t φ`，遍历把词项 `t` 在语境前段抽象，经越过公式体出现的 `padRight`；并把公式体的安置经 `padLeft` 越过词项出现后再移位 `suc`。相应地，该子句是二者的 `cong₂ _⇒_`：一侧经词项引理得到 `x` 属于抽象后界定项，另一侧经移位后的归纳得到在 `x ∷ γ` 处的递归命题；`leftHalf` 与 `rightHalf` 把 `h` 在 `constantsTm t` 与 `constantsFo φ` 之间拆分。存在型有界量词 `∃̇∈` 以 `⊓` 代替 `⇒` 与之互为镜像。至此，语言的每个构造子都由同一不变量覆盖。

```agda
      (cong (x ∈ˢ_) (⟦⟧-place t (λ i → θ (padRight (countFo φ) i)) γ σ
        (leftHalf θ γ σ (constantsTm t) (constantsFo φ) h)))
      (⊨-place φ (λ j → suc (θ (padLeft (countTm t) j))) (x ∷ γ) σ
        (rightHalf (countTm t) θ γ σ (constantsTm t) (constantsFo φ) h))))
```

名副其实的充分性随之而来：安置取抽象所取的那一个，参数环境取收集所规定的那一个，即诸常元自身经解释之后的样子。它的假设正是两条补位定律的延续，而定理的内容也一如所述：原公式在 `γ` 处的满足，就是抽象在「`γ` 被收集来的诸常元扩张之后」的满足。

主定理把归纳实例化一次。由于 `absFo φ` 是在安置 `padLeft n` 处的遍历产生的，就该在那个安置处应用 `⊨-place`，而参数环境取为 `map ι (constantsFo φ)`：按次序排列的被记录常元，逐一经解释。所得定理说：原公式在 `γ` 处的满足，就是抽象在「`γ` 被这些经解释常元扩张之后」的满足。

```agda
    ⊨-abs : ∀ {n} (φ : Formula K n) (γ : S ^ n)
          → (γ ⊨ φ) ≡ ((γ ++ map ι (constantsFo φ)) ⊨₀ absFo φ)
    ⊨-abs {n} φ γ = ⊨-place φ (padLeft n) γ (map ι (constantsFo φ)) hyp
      where
      hyp : ∀ j → lookup (padLeft n j) (γ ++ map ι (constantsFo φ))
```

剩下的只是看到这一 `σ` 的选择如何清偿假设。安置 `padLeft n` 把出现 `j` 送到条目 `n + j`，它落在拼接的后半段；`lookup-padLeft` 把该条目等同于 `lookup j (map ι (constantsFo φ))`，`lookup-map` 再让解释穿过，恰得 `ι (lookup j (constantsFo φ))`。两条定律复合即为假设，有了它 `⊨-place` 便给出定理。数学上说：一条无参公式加上一个有限的有序参数向量，与原带常元公式具有相同的外延。

```agda
                ≡ ι (lookup j (constantsFo φ))
      hyp j = lookup-padLeft n γ (map ι (constantsFo φ)) j
            ∙ lookup-map ι (constantsFo φ) j
```

## 何谓可定义子集

参数抽象把可定义子集背后的数据拆开列出：一条无参公式、一个有限参数向量，以及用于检验成员关系的变量。充分性表明，这种呈现与原带常元公式具有完全相同的外延。

还有一处形状，也是元数一的情形值得单写的理由：在元数一处，扩张后的环境是 `x ∷ map ι p`，一个成员后接诸参数，而那正是本书别处每一个单条目环境的形状。

对一元可定义子集，这条推论把环境固定为 `x ∷ []`：元数为一的公式在唯一成员 `x` 处检验，定理给出抽象在 `x` 后接诸经解释参数处的检验。由于该陈述是命题之间的路径，两种对成员关系的读法可以互换；后续为可定义子集编码的章节可以直接使用无参公式加参数向量 `map ι (constantsFo φ)`，既无须重标常元，也无须改动公式。

```agda
    ⊨-abs₁ : (φ : Formula K 1) (x : S)
           → ((x ∷ []) ⊨ φ) ≡ ((x ∷ map ι (constantsFo φ)) ⊨₀ absFo φ)
    ⊨-abs₁ φ x = ⊨-abs φ (x ∷ [])
```

## 小结

`absFo` 为每次常元出现增加一个变量以消去常元，`⊨-abs` 则在把记录的常元附加到环境后识别满足关系。这就是公式本身需要符号化时所用的有限参数呈现。