参数抽象

可以直接阅读本章，也可以通过阅读指南和依赖地图选择其他路线。

阅读指南 · 依赖地图

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

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

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

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

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

module FOL.Manipulation.ParameterAbstraction where

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

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

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

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

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

  ( 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 个是新的参数位。输出是空字母表 ⊥* 上的词项，因为没有常元存活下来。

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 个位中的同一位，由补位定律，它在拼接环境中仍取原值。

        → (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 个位。这样每个子词项看到的都是作用于自身出现位的安置，两个翻译后的子词项以原来的联结词重新组合。

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 复合。假值 ⊥̇ 没有任何出现，翻译为自身。没有哪条子句需要第二次遍历或改名引理：在递归之前先复合安置，使整个翻译保持为一次结构性遍历。

                   ⇒̇ 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 安置在前段。无界量词 ∃̇ 与 ∀̇ 只带移位。这些子句合起来覆盖了全部十个公式构造子。

                        (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)。全部序号算术都已折入遍历之中，抽象本身没有任何情形需要处理。由于预算恰等于计数，安置实际上给出了出现位与参数位之间的双射，不过代码从不需要把这一点说出来。

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 的环境的类型。

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

  open ZFStructure 𝒮

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

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

  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 复合、再施加 ι，便得到递归调用所需的左前提。

    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 必须被确切告知要跨过多少个位。

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

      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，这恰是命题，只是等式的方向相反。

    ⟦⟧-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，即较宽语境中的同一位，补位定律表明在 γ ++ σ 中查出即可恢复原值。常元与变量两个情形解决后，其余构造子要么是由拆分不变量处理的二元节点，要么是约束子，公式层面的归纳遵循同一模式。

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

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

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

    ⊨-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 的处理完全相同，只是以结构的相等 ≈ˢ 代替属于；随后的命题联结词只需把词项引理换成公式层归纳。

      (⟦⟧-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 ℓ 中的命题，并且只使用同余，不假定它具有对的表示，也不将其拆解。

      (⟦⟧-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₂ 所施加的逻辑运算上不同；包括拆分后的假设在内，其余完全一致。

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

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

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

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

      (⊨-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。这个抵消是定义性的，因此证明中不出现任何移位引理。

    ⊨-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 是唯一指名该运算之处，其下的归纳毫无二致。

      (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 φ 之间拆分。存在型有界量词 ∃̇∈ 以 ⊓ 代替 ⇒ 与之互为镜像。至此，语言的每个构造子都由同一不变量覆盖。

      (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 φ)：按次序排列的被记录常元，逐一经解释。所得定理说：原公式在 γ 处的满足，就是抽象在「γ 被这些经解释常元扩张之后」的满足。

    ⊨-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 便给出定理。数学上说：一条无参公式加上一个有限的有序参数向量，与原带常元公式具有相同的外延。

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

何谓可定义子集

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

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

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

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

小结

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