---
title: "码化递归所用的公式表达式"
module: L.Coding.Expressions
lang: zh
site: "Bedrock"
description: "码化递归所用的公式表达式"
stage: "内部编码：表达式与定义域"
reading_order: 43
canonical: https://bedrock.institute/zh/L.Coding.Expressions.html
html: L.Coding.Expressions.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/Coding/Expressions.lagda.md
prerequisites: [Base.Prelude, FOL.ZFStructure, FOL.Syntax, FOL.Absoluteness, V.Hierarchy, V.Coding, L.Constructible, FOL.Manipulation.ConstantBounding, L.Absoluteness, L.Coding.Environment, L.Axioms.Numerals, L.Coding.Model]
routes: [internal-satisfaction]
translations: [https://bedrock.institute/en/L.Coding.Expressions.md, https://bedrock.institute/ja/L.Coding.Expressions.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
# 码化递归所用的公式表达式

码化的满足关系递归要在 `L` 内部判定形如「环境 `γ` 是否满足码 `c` 所示公式」的问题。要用有界公式识别 Kuratowski 对这样的复合取值，其见证本身必须是模型元素。对分量 `u`、`v` 的配对 `q`，需要一个可构造集合 `s`，使 `s` 属于 `q`，而 `u`、`v` 属于 `s`；读式一次性绑定这三者，并在「`v, u, s` 接原赋值」的扩展赋值中求取两个分量条件，原槽位在移位下保持不变。

本章把这件事一次做好：在由赋值槽位、可构造字面常元、数码与 Kuratowski 对组成的小表达式语言上建立一条结构读式，并证明其双向充分性。向外方向从满足判断出发，把三层截断存在消去到取值为命题的路径中，再将配对等式与递归的分量路径串联。向内方向为两个子表达式选定显式的内部元素，并取得它们共同的可构造容器，而不从任何截断中抽取选择。

同一读式随后沿几个方向特化。表达式取值属于词项所指的隶属关系使用 `L` 的传递性：该周遭取值属于词项的可构造解释这一事实证明了取值可构造，故它能充当模型元素；这是一次真正的构造，与「截断只能消去到取值为命题的目标」这一限制不同。外延集合描述是一对普通的全称蕴含，外层没有截断；它刻画一个候选集合，而不构造它。元数标签识别器读取两层嵌套的配对：元数与「标签加载荷」之对。最后，后继公式与环境扩展公式经有界绝对性抬升，其转换立足于既有的传递模型设置，以及查值在投影下的相容性。本章以环境扩展公式收尾。

要让复合集合取值的一阶描述留在有界片段中，固定部件由常元命名，每个见证都受集合界定。这里的一切都固定在一个层 `ℓ` 上：周遭层级是 `V ℓ`，有界量词所遍历其元素的模型，是栖身于其中的可构造模型。由于满足判断比较的是真值，这些公式所断言的事实便是`hProp (ℓ-suc ℓ)` 中的命题。

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

open import Base.Prelude

module L.Coding.Expressions {ℓ : Level} where

open import FOL.ZFStructure using ( module hPropStructure )
```

一条区分的两面贯穿全章。在层级之外，结构 `𝒮ᵥ` 在 `V ℓ` 上解释一阶语言，那里的 Kuratowski 配对正是运算 `pr`。在模型之内，同一语言被重新解释于可构造集合之上。因此，识别复合取值的一条子句必须能同时在两处读出；而下面的每条充分性陈述说的恰是这件事：内部公式在模型中读出的真值，作为一条路径，被等同于关于 `pr` 与投影赋值的相应周遭陈述。

```agda
open import FOL.Syntax
  using ( Term; Formula; var; con; _∈̇_; _≐_; _∧̇_; _⇒̇_; ∀̇_; ∃̇∈ )
import FOL.Absoluteness
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ )
open import V.Coding {ℓ} using ( pr )
```

可构造模型的一个元素是「周遭集合连同它可构造的证明」。`L` 的传递性使有界见证能在两侧之间移动：由 `isL-trans`，可构造集合的成员本身可构造，因而自己就能充当模型元素。有界绝对性则为公式做相应的工作：一条关于层级、且所有常元都命名可构造集合的 Δ₀ 公式，在 `L` 内意义不变；`BoundedFo` 数据记录的常元有界性正是这一转换所需的前提。后继公式与环境扩展公式已在层级一侧证得，把它们抬入模型只需施用这一转换。

```agda
open import L.Constructible {ℓ} using ( 𝒮ʟ; isL; isL-trans )
open import FOL.Manipulation.ConstantBounding using ( BoundedFo )
open import L.Absoluteness {ℓ} using ( InL; liftFo; transferFo )
open import L.Coding.Environment {ℓ}
  using ( sucAt; Δ₀-sucAt; sucAt-adequate; consAt; Δ₀-consAt; consAt-adequate
```

数码需要一条相容性事实。内部数码 `numeralL k` 在模型内实现冯·诺伊曼自然数 `k`，而 `numeralL-fst` 把它的投影与周遭的 `# k` 等同起来；数码子句的两个方向都依赖于此。由于若干子句要同时对有穷多个槽位量化，环境沿槽位的重标定而移动。一种逻辑形式贯穿全章：充分性陈述是由命题等价的两个蕴含得到的真值路径，而对象语言的有界量词被读作截断存在。

```agda
        ; env; cons; shiftPairAt; sgl0At; pair0At; tag0At )
open import L.Axioms.Numerals {ℓ} using ( numeralL; numeralL-fst )

open import Cubical.Data.Vec using ( map )
open import Cubical.Data.Nat using ( _+_ )
open import Cubical.Functions.Logic using ( ⇔toPath; ∃[∶]-syntax )
```

周遭层级 `V ℓ` 是一个 h-集合，故其中两个集合的相等是命题，可以放进真值之内；这正是下文打包等式得以成立的原因。自然数以集合身份进入：`# k` 是层级中的冯·诺伊曼数码，`sucV` 是其后继运算，它既不同于任何宇宙层级，也不同于码所带的元数指标。命题截断给出单纯存在，其消去只在取值为命题的目标中合法；配对读式的向外证明将显式遵守这一限制。

```agda
import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∣_∣₁ )
open import Cubical.HITs.CumulativeHierarchy.Base using ( V; setIsSet; _∈_ )
open import Cubical.HITs.CumulativeHierarchy.Constructions using ( module InfinitySet )
open InfinitySet using ( #_; sucV )
```

这里使用的真值是层 `ℓ-suc ℓ` 的 `hProp` 命题，每个都连同「它是命题」的证明打包，联结词与量词直接作用在这些命题上。模型的载体 `S` 由「周遭集合配可构造性证书」的对组成。绝对性机制针对这一情形一次性设立：被相对化的结构是层级 `𝒮ᵥ`，挑选子模型的类是 `isL`，传递性使 Δ₀ 公式保持绝对；满足记作 `⊨`，词项解释记作 `⟦_⟧`，环境是模型元素的向量。

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

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

open import L.Coding.Model {ℓ}
```

模型词典中有一件东西对主要构造至关重要：配对形状的事实。模型的配对 `prʟ` 经 `prʟ-fst` 投影为周遭配对，其有界读式是 `prAtL`；记录 `Container` 连同 `container` 为等于某个对的取值造出一个容纳两个分量的可构造集合。用有界公式读取一个对，需要的恰是这样的中间集合；而 `lookup-fst` 与 `envOverAt` 则是同一词典中稍后用到的投影与环境事实。

```agda
  using ( lookup-fst; prʟ; prʟ-fst; prAtL; prAtL-adequate; envOverAt
        ; Container; container )
```

模型中的有界量词遍历 `S` 的元素，因此公式要识别的任何复合取值，都必须能由本身是模型元素的有界见证来匹配。本节建立一般工具：一个归纳语言 `Expr`，其取值由赋值槽位、可构造字面常元、数码与 Kuratowski 对组装而成；连同一条把表达式变成公式的结构读式，以及一个双向的充分性定理，它把公式的含义与表达式所指的值等同起来。本章其余的一切都是这一读式的特例。

本节以两件小准备开篇。`PairIs a p` 把「周遭取值 `a` 等于 `p`」这一陈述打包成真值：由于层级是 h-集合，该相等类型是命题，与 `setIsSet` 配对后便是 `hProp (ℓ-suc ℓ)` 的元素。此后充分性陈述都将沿路径把满足判断与这些打包的等式相比较。表达式语言本身以自然数 `n` 为指标，确定可用的自由变元槽位数；某个槽位完全可以不被使用。

```agda
private
  PairIs : V ℓ → V ℓ → hProp (ℓ-suc ℓ)
  PairIs a p = (a ≡ p) , setIsSet a p

module PairExpression where
  data Expr (n : ℕ) : Type (ℓ-suc ℓ) where
```

表达式语言由四个构造子确定，每个构造子对应复合取值向公式呈现自身的一种方式。`slot` `i` 引用周遭赋值的第 `i` 项，相当于变元；`literal` `a` 一次性命名模型的一个完整元素，连同其可构造性证书，故其行为如对象语言常元；`numeral` `k` 命名冯·诺伊曼自然数 `k`；`pair` 把两个子表达式合成一个 Kuratowski 对。表达式是取值的有穷描述，本身不是集合，因此它容许两种独立的读法，而目标正是证明二者一致。

```agda
    slot : Fin n → Expr n
    literal : S → Expr n
    numeral : ℕ → Expr n
    pair : Expr n → Expr n → Expr n

  value : ∀ {n} → Expr n → (Fin n → V ℓ) → V ℓ
```

第一种读法是周遭的。给定把层级集合指派给各槽位，`value` 计算表达式所指的集合：槽位按查值，字面常元经 `fst` 投影掉其证书，数码变为 `# k`，配对则是两个所指集合的 Kuratowski 对 `pr`。充分性定理将在右侧恢复的正是这种读法：一条有界公式的意义，就在于从模型内部识别出一个天然描述于外的取值。

```agda
  value (slot i) γ = γ i
  value (literal a) γ = fst a
  value (numeral k) γ = # k
  value (pair a b) γ = pr (value a γ) (value b γ)

  element : ∀ {n} → Expr n → (Fin n → S) → S
```

第二种读法停留在模型内部。给定把 `S` 的元素指派给各槽位，`element` 计算出一个 `S` 的元素：字面常元本就是带证书的模型元素，数码用内部数码 `numeralL`，配对由模型自己的配对 `prʟ` 生成。两种读法逐条款平行，而这种平行性正是二者之间的桥梁可证的原因：比较它们时只需逐情形对应地比。

```agda
  element (slot i) γ = γ i
  element (literal a) γ = a
  element (numeral k) γ = numeralL k
  element (pair a b) γ = prʟ (element a γ) (element b γ)

  element-fst : ∀ {n} (e : Expr n) (γ : Fin n → S)
```

桥梁是 `element-fst`：投影一个内部元素，作为一条路径，恰好等于在投影后赋值处的周遭取值。对槽位与字面常元，两种读法逐字重合，故证明即 `refl`。数码是第一个实质情形：其内部形式经 `numeralL-fst` 投影为周遭形式，这正是数码一章给出的内部数码与周遭数码之间的相容性事实。注意方向，它将贯穿全章：路径从内部取值的投影出发，指向周遭取值。

```agda
              → fst (element e γ) ≡ value e (λ i → fst (γ i))
  element-fst (slot i) γ = refl
  element-fst (literal a) γ = refl
  element-fst (numeral k) γ = numeralL-fst k
  element-fst (pair a b) γ = prʟ-fst (element a γ) (element b γ)
```

配对情形把两条独立的相容性串联起来：模型的配对经 `prʟ-fst` 投影为周遭配对，而每个分量的投影律正是递归的事实。在 `pr` 之下的同余把两条分量路径合成一条，嵌套表达式的投影律便由归纳成立。在语法一侧，`lift3` 是配对读式所需的重标定：它把每个旧槽位上移三位，即 `lift3 ρ i = suc (suc (suc (ρ i)))`，既保留每个槽位所指的旧条目，又为三个新变元腾出位置。

```agda
    ∙ cong₂ pr (element-fst a γ) (element-fst b γ)

  lift3 : ∀ {n m} → (Fin n → Fin m) → Fin n → Fin (3 + m)
  lift3 ρ i = suc (suc (suc (ρ i)))

  read : ∀ {n m} → Expr n → (Fin n → Fin m) → Fin m → Formula S m
  read (slot i) ρ q = var q ≐ var (ρ i)
```

读式 `read` 把槽位 `q` 处的表达式变成一条有界公式。槽位要求与相应的重标定变元相等，字面常元要求与其常元相等，数码要求与命名其内部数码的常元相等。配对情形才有数学内容：它用三条有界存在绑定 `q` 处集合中的集合 `s`，以及 `s` 中的元素 `u`、`v`，使 `s` 属于 `q` 处的条目，而 `u`、`v` 属于 `s`；再借模型的配对读式 `prAtL` 断言 `q` 处的条目等于对 `pr u v`。随后在移位槽位处递归读出两个分量条件，这正是 `lift3` 所提供的。于是，一个复合取值是从模型内部、经由一个容纳两个 Kuratowski 分量的可构造中间集合来识别的。

```agda
  read (literal a) ρ q = var q ≐ con a
  read (numeral k) ρ q = var q ≐ con (numeralL k)
  read (pair a b) ρ q = ∃̇∈ (var q) (∃̇∈ (var zero) (∃̇∈ (var (suc zero))
    (prAtL (suc (suc (suc q))) (suc zero) zero
      ∧̇ (read a (lift3 ρ) (suc zero) ∧̇ read b (lift3 ρ) zero))))
```

充分性分为两个方向，`out` 是可靠性证明所用的方向：从满足判断的一个证明出发，产出「槽位 `q` 处的条目投影后等于所指的值」这条路径。槽位与字面常元按定义本就是这样的路径，数码情形则把前提与 `numeralL-fst` 复合，方向与 `element-fst` 相同。实质工作在配对情形，它占了接下来的两步。

```agda
  out : ∀ {n m} (e : Expr n) (ρ : Fin n → Fin m) (q : Fin m) (γ : S ^ m)
       → ⟨ γ ⊨ read e ρ q ⟩ → fst (lookup q γ) ≡ value e (λ i → fst (lookup (ρ i) γ))
  out (slot i) ρ q γ h = h
  out (literal a) ρ q γ h = h
  out (numeral k) ρ q γ h = h ∙ numeralL-fst k
```

配对情形的前提是一个具有三层的截断有界存在，故证明逐层消去它们，而每次消去都需要取值为命题的目标。这正是 `setIsSet` 进入之处：结论是层级 (一个 h-集合) 中的一条路径，因此目标是命题，消去合法。截断给了什么、没给什么，值得直说：见证 `s`、`u`、`v` 作为元素到达，数学可以继续使用它们，但前提断言的只是它们的单纯存在：没有唯一性，也没有被选出的代表。

```agda
  out (pair a b) ρ q γ = PT.rec (setIsSet _ _) (λ { (s , s∈ , hs) →
    PT.rec (setIsSet _ _) (λ { (u , u∈ , hu) →
      PT.rec (setIsSet _ _) (λ { (v , v∈ , p , ha , hb) →
        subst ⟨_⟩ (prAtL-adequate (suc (suc (suc q))) (suc zero) zero (v ∷ u ∷ s ∷ γ)) p
        ∙ cong₂ pr (out a (lift3 ρ) (suc zero) (v ∷ u ∷ s ∷ γ) ha)
```

拿到三个见证后，最内层公式由配对读式自身的充分性展开：把 `p` 沿 `prAtL-adequate` 传输，配对断言便变成等式 `fst (lookup q γ) ≡ pr (fst u) (fst v)`。两个递归前提随即给出分量在一号与零号槽位处的投影，即 `fst u ≡ value a` 与 `fst v ≡ value b`；再经 `pr` 之下的同余，右侧被改写为 `pr (value a) (value b)`，恰是该配对表达式的取值。内层证明因此是一次传输加一次同余。

```agda
                   (out b (lift3 ρ) zero (v ∷ u ∷ s ∷ γ) hb) }) hu }) hs })

  into : ∀ {n m} (e : Expr n) (ρ : Fin n → Fin m) (q : Fin m) (γ : S ^ m)
        → fst (lookup q γ) ≡ value e (λ i → fst (lookup (ρ i) γ)) → ⟨ γ ⊨ read e ρ q ⟩
  into (slot i) ρ q γ h = h
  into (literal a) ρ q γ h = h
```

逆向的 `into` 从裸等式出发构造满足判断的一个证明。槽位与字面常元直接可得；数码情形与 `numeralL-fst` 的对称复合，调转了前述相容性的方向。配对情形须一次性给出全部三个截断层，而此处并非从截断中抽取任何东西：见证是直接构造的。内部元素 `u` 与 `v` 取为重标定赋值下的 `element a` 与 `element b`，而 `Container` 与 `container` 用调整后的路径 `e` 造出一个同时容纳两者的可构造集合 `s`，连同全部隶属证书。这是对 `L` 传递性的一次独立运用，与上文使消去得以合法的「取值为命题」是两回事：那里消去的是截断，这里产出的是具体的元素。

```agda
  into (numeral k) ρ q γ h = h ∙ sym (numeralL-fst k)
  into {n} {m} (pair a b) ρ q γ h = ∣ s , c .snd .fst , ∣ u , c .snd .snd .fst ,
    ∣ v , c .snd .snd .snd ,
      subst ⟨_⟩ (sym (prAtL-adequate (suc (suc (suc q))) (suc zero) zero δ)) e
      , into a (lift3 ρ) (suc zero) δ (element-fst a η)
```

扩展赋值 `δ` 就是 `v ∷ u ∷ s ∷ γ`，它的布局就是这一构造的全部簿记：

| 槽位 | 条目 | 角色 |
| --- | --- | --- |
| 0 | `v` | `b` 的内部元素 |
| 1 | `u` | `a` 的内部元素 |
| 2 | `s` | 中间集合，`q` 处条目的成员 |
| `i + 3` | 旧槽位 `i` | 原赋值，原样保留 |

配对公式断言 `s ∈ q`、`u ∈ s`、`v ∈ s`，以及 `q ≡ pr u v`；由于 `u` 位于一号槽位、`v` 位于零号槽位，经 `lift3` 后，在一号槽位处的 `read a` 与零号槽位处的 `read b` 所查询的恰是原来的槽位。每个子证明由 `into` 自身在移位槽位处组装，喂入被读分量的投影路径 `element-fst`；最后，三个嵌套的截断存在各以一个显式的 `∣_∣₁` 封口。

```agda
      , into b (lift3 ρ) zero δ (element-fst b η) ∣₁ ∣₁ ∣₁
    where
    η : Fin n → S
    η i = lookup (ρ i) γ
    u v : S
```

其余的局部定义记录这一构造的算术。`η` 把旧赋值限制到重标定后的槽位，`u` 与 `v` 是两个子表达式在其下的显式内部元素；它们是直接选定的，并非从任何截断中提取。路径 `e` 随后陈述：`q` 处的条目等于周遭配对 `pr (fst u) (fst v)`。它的方向很重要：前提 `h` 说条目等于整个配对所指的值，与分量的投影同余 `element-fst` 的对称复合后，得到的恰是容器构造所预期的目标。

```agda
    u = element a η
    v = element b η
    e : fst (lookup q γ) ≡ pr (fst u) (fst v)
    e = h ∙ sym (cong₂ pr (element-fst a η) (element-fst b η))
    c : Container (lookup q γ) u v
```

容器由路径 `e` 造出，其第一个分量正是所需的可构造集合 `s`，它是到达两个 Kuratowski 分量的公共中间体：`s` 是 `q` 处条目的成员，而 `u` 与 `v` 是 `s` 的成员。把 `v`、`u`、`s` 依次推到 `γ` 的最前，便得到比原来多元数三的扩展赋值 `δ`。此后内向构造所需的每个材料都不再是游离的元素，而是 `δ` 的一个条目。

```agda
    c = container (lookup q γ) u v e
    s : S
    s = c .fst
    δ : S ^ (suc (suc (suc m)))
    δ = v ∷ u ∷ s ∷ γ
```

两个方向组装成所宣称的形状。`adequate` 陈述：在 `γ` 处的满足判断，作为一个真值，等于「`q` 处条目的投影」与「周遭所指」之间打包后的等式；`⇔toPath` 把 `out` 与 `into` 这对蕴含变成这条路径。作为第一个应用，`member e C` 说表达式 `e` 的取值属于词项 `C` 的所指：它对 `C` 所指的成员作有界量化，并要求在该成员扩展后的赋值处成立表达式读式，其中表达式被移入首位槽位。

```agda
  adequate : ∀ {n m} (e : Expr n) (ρ : Fin n → Fin m) (q : Fin m) (γ : S ^ m)
            → (γ ⊨ read e ρ q) ≡ PairIs (fst (lookup q γ)) (value e (λ i → fst (lookup (ρ i) γ)))
  adequate e ρ q γ = ⇔toPath (out e ρ q γ) (into e ρ q γ)

  member : ∀ {n} → Expr n → Term S n → Formula S n
  member e C = ∃̇∈ C (read e suc zero)
```

`member` 的向外读式消去截断的有界存在，得到成员 `x`、其隶属证明 `h`，以及「`x` 的扩展赋值满足表达式读式」的证明 `p`。把充分性沿向外方向施于 `p`，得到等式 `fst x ≡ value e ...`；再沿这条等式搬运 `h`，便把 `fst x` 的隶属变成所指取值的隶属。目标正是隶属命题 `value e ... ∈ fst (⟦ C ⟧ γ)`，其第二分量给出 `PT.rec` 所需的命题性证明。

```agda
  member-out : ∀ {n} (e : Expr n) (C : Term S n) (γ : S ^ n)
              → ⟨ γ ⊨ member e C ⟩ → ⟨ value e (λ i → fst (lookup i γ)) ∈ fst (⟦ C ⟧ γ) ⟩
  member-out e C γ = PT.rec (snd (value e (λ i → fst (lookup i γ)) ∈ fst (⟦ C ⟧ γ)))
    (λ { (x , h , p) → subst (λ v → ⟨ v ∈ fst (⟦ C ⟧ γ) ⟩) (out e suc zero (x ∷ γ) p) h })

  member-in : ∀ {n} (e : Expr n) (C : Term S n) (γ : S ^ n)
```

向内读式必须给出那个成员，而表达式 `e` 的取值本身即可充当，只需先把它变成模型的元素。由前提它是 `fst (⟦ C ⟧ γ)` 的成员，而该词项的解释可构造，于是 `L` 的传递性给出该取值的可构造性证书：这正是 `isL-trans` 在此处所做的事。这里没有消去截断；证书与周遭取值组成显式的模型元素 `x`，作为有界存在的见证。扩展赋值处的首项按定义投影为该取值，故递归的 `into` 收到路径 `refl`。

```agda
             → ⟨ value e (λ i → fst (lookup i γ)) ∈ fst (⟦ C ⟧ γ) ⟩ → ⟨ γ ⊨ member e C ⟩
  member-in e C γ h = ∣ x , h , into e suc zero (x ∷ γ) refl ∣₁
    where
    x : S
    x = value e (λ i → fst (lookup i γ)) , isL-trans h (snd (⟦ C ⟧ γ))
```

第一个特化把一般读式变成标签识别器。`tagAtL s k x` 在槽位 `s` 处读取「数码 `k` 与槽位 `x` 配对」的表达式，因而是一条有界公式，断言 `s` 处的条目是 `# k` 与 `x` 处条目的有序对。递归中的码都带有一个与载荷配对的数字标签，而这正是那个形状。

```agda
tagAtL : ∀ {n} → Fin n → ℕ → Fin n → Formula S n
tagAtL s k x = PairExpression.read
  (PairExpression.pair (PairExpression.numeral k) (PairExpression.slot x)) id s

tagAtL-adequate : ∀ {n} (s : Fin n) (k : ℕ) (x : Fin n) (γ : S ^ n)
  → (γ ⊨ tagAtL s k x)
```

它的充分性引理无需新证明：在这一表达式处以恒等改名实例化一般充分性，其计算结果已经是「满足判断等同于投影条目与 `pr (# k)` 投影载荷的 `PairIs`」。这是全节的模式：选定一个表达式，引用 `PairExpression.adequate`，子句的含义便被读出。

```agda
  ≡ PairIs (fst (lookup s γ)) (pr (# k) (fst (lookup x γ)))
tagAtL-adequate s k x γ = PairExpression.adequate
  (PairExpression.pair (PairExpression.numeral k) (PairExpression.slot x)) id s γ

tagPairAtL : ∀ {n} → Fin n → ℕ → Fin n → Fin n → Formula S n
tagPairAtL s k a b = PairExpression.read
```

第二个特化处理本身是对形式的载荷，两层配对嵌套在表达式之内。`tagPairAtL s k a b` 读取「数码 `k` 与槽位 `a`、`b` 之对配对」的表达式，故识别形如 `pr (# k) (pr (entry a) (entry b))` 的条目：一个标签架在双分量载荷之上。

```agda
  (PairExpression.pair (PairExpression.numeral k)
    (PairExpression.pair (PairExpression.slot a) (PairExpression.slot b))) id s

tagPairAtL-adequate : ∀ {n} (s : Fin n) (k : ℕ) (a b : Fin n) (γ : S ^ n)
  → (γ ⊨ tagPairAtL s k a b)
  ≡ PairIs (fst (lookup s γ))
```

充分性引理再次由一般引理直接计算而得，恢复全部三个分量：标签数码，以及投影后的两个载荷条目。嵌套完全在表达式读式内部处理；在这一层子句上，除表达式形状外什么都看不见。

```agda
      (pr (# k) (pr (fst (lookup a γ)) (fst (lookup b γ))))
tagPairAtL-adequate s k a b γ = PairExpression.adequate
  (PairExpression.pair (PairExpression.numeral k)
    (PairExpression.pair (PairExpression.slot a) (PairExpression.slot b))) id s γ
```

## 以外延给出集合

上一节的结构读式经由 Kuratowski 配对层识别取值；而许多递归子句要说的却是「一个集合的成员是什么」。二者是同类陈述：模型中的一条一阶公式，读回周遭层级后，恰能指认槽位中的取值。本节构造外延形状。

`extAt` y φ 对槽位 `y` 中的集合断言：其成员恰为满足一元条件 `φ` 的对象。它的外层结构是两条无界全称量词经普通合取相连：一条从属于该集合推出 `φ`，一条反向。`extAt` 自身不引入新的命题截断，但参数 `φ` 是任意公式，内部可以含有自己的量词与截断存在。由于外层的证据只是普通的合取，它的两种读法就是该合取的两个投影，而它的引入也就是二者的有序对。这正是一条描述所需的强度：该公式刻画一个候选集合，对这样的集合是否存在不置一词；存在与否，属于日后给出该取值的构造的事。

该定义为候选者绑定一个新变元，整体是两条无界全称量词的合取：槽位 `y` 中集合的每个成员满足 `φ`，而每个满足者也属于该集合。外层的联结词是普通合取，`extAt` 不把任何一条蕴含包进截断，但条件 `φ` 按原样传入，可以是任何公式，内部含有量词或截断存在均可。`extAt` 自身固定的只是外层形状：量词之下的一对蕴含，每侧都是模型元素及其满足证明上的函数。这正是该公式得以充当描述的原因：它约束一个取值，却从不断言取值的存在。

```agda
extAt : ∀ {n} → Fin n → Formula S (suc n) → Formula S n
extAt y φ = ∀̇ ((var zero ∈̇ var (suc y)) ⇒̇ φ)
         ∧̇ ∀̇ (φ ⇒̇ (var zero ∈̇ var (suc y)))

module _ {n : ℕ} (y : Fin n) (φ : Formula S (suc n)) (γ : S ^ n) where
  extAt-out : ⟨ γ ⊨ extAt y φ ⟩ → (z : S)
```

两个读式就是外层合取的两个投影。由 `extAt y φ` 的一个证明出发，`extAt-out` 取第一分量：它对每个模型元素 `z` 给出一条蕴含，从 `fst z` 属于槽位 `y` 处集合，到扩展环境中 `φ` 成立；`extAt-in` 取第二分量，给出反方向的同一条蕴含。两个读式都不消去截断、不选取见证、也不沿路径搬运；无论 `φ` 内部含有什么，在这一外层上证据就是一个有序对，而每个读式恰是它的投影。

```agda
            → ⟨ fst z ∈ fst (lookup y γ) ⟩ → ⟨ (z ∷ γ) ⊨ φ ⟩
  extAt-out h = h .fst

  extAt-in : ⟨ γ ⊨ extAt y φ ⟩ → (z : S)
           → ⟨ (z ∷ γ) ⊨ φ ⟩ → ⟨ fst z ∈ fst (lookup y γ) ⟩
  extAt-in h = h .snd
```

引入把两个投影反向运行，就是那两条蕴含的有序对，各以函数形式给出。于是有 `extAt-in-both`：一个能同时建立其条件两个方向的子句，只需把两个函数配成对，便满足这条公式，外层无须再做任何事；量词或截断的工作都发生在 `φ` 内部，并在那里完成。这条陈述本身值得细读：它从两个函数造出满足判断的一个证明，而对「成员满足 `φ` 的集合是否存在」不作任何断言。这样的集合是否真的被给出，由构造取值之处决定，与此处无关。

```agda
  extAt-in-both : ((z : S) → ⟨ fst z ∈ fst (lookup y γ) ⟩ → ⟨ (z ∷ γ) ⊨ φ ⟩)
                → ((z : S) → ⟨ (z ∷ γ) ⊨ φ ⟩ → ⟨ fst z ∈ fst (lookup y γ) ⟩)
                → ⟨ γ ⊨ extAt y φ ⟩
  extAt-in-both f g = f , g
```

## 分两层读一个键

满足关系递归的键是一个由两层嵌套配对组装而成的集合：元数与一个码配成对，而码本身又是标签数码与载荷之对。因此用有界公式识别一个键，就意味着检查这两层配对；而结构读式本就处理任意嵌套的表达式，恰好胜任。于是下面的每条公式都是把该读式用于相应的表达式，每条充分性引理也都是 `PairExpression.adequate` 的相应特例。元数被有意保留为变元槽位而非固定为某个数码，因为那些会产出不同元数子公式的构造子，其子句需要谈论元数值本身。

`arityTagPairAtL c ar k a b` 断言槽位 `c` 中的集合是一个有序对：第一分量是槽位 `ar` 中的集合，第二分量本身又是一个配对，即数码 `# k` 与槽位 `a`、`b` 中集合之对的配对。定义表达式为 `pair (slot ar) (pair (numeral k) (pair (slot a) (slot b)))`，在恒等改名下于 `c` 处读取；这正是载荷为双槽位码的键的形状。

```agda
arityTagPairAtL : ∀ {n} → Fin n → Fin n → ℕ → Fin n → Fin n → Formula S n
arityTagPairAtL c ar k a b = PairExpression.read
  (PairExpression.pair (PairExpression.slot ar)
    (PairExpression.pair (PairExpression.numeral k)
      (PairExpression.pair (PairExpression.slot a) (PairExpression.slot b)))) id c
```

充分性陈述把该公式的真值等同于命题 `PairIs (fst (lookup c γ)) (...)`，这是周遭层级中的一条路径，断言 `c` 处的集合等于由各槽位投影构造的嵌套 Kuratowski 对。各分量便可从右边读出：标签数码 `# k` 是固定的，而 `ar`、`a` 与 `b` 各自贡献其查得的值。由于该陈述是真理值之间的路径而非单向蕴含，后续证明可以在任一方向上用它改写。

```agda
arityTagPairAtL-adequate : ∀ {n} (c ar : Fin n) (k : ℕ) (a b : Fin n) (γ : S ^ n)
  → (γ ⊨ arityTagPairAtL c ar k a b)
  ≡ PairIs (fst (lookup c γ))
      (pr (fst (lookup ar γ))
        (pr (# k) (pr (fst (lookup a γ)) (fst (lookup b γ)))))
```

证明是 `PairExpression.adequate` 对同一表达式、同一改名与同一槽位的一行特例。有界见证、截断存在的消去与引入、以及沿 `prAtL` 充分性的搬运，都已在结构定理中一次性完成，故这里不再出现新的语义论证。双槽位载荷的情形就绪之后，单载荷变体 `arityTagAtL c ar k a` 以同样方式定义，唯一差别是最内层表达式是单个槽位 `a`，而非两个槽位之对。

```agda
arityTagPairAtL-adequate c ar k a b γ = PairExpression.adequate
  (PairExpression.pair (PairExpression.slot ar)
    (PairExpression.pair (PairExpression.numeral k)
      (PairExpression.pair (PairExpression.slot a) (PairExpression.slot b)))) id c γ

arityTagAtL : ∀ {n} → Fin n → Fin n → ℕ → Fin n → Formula S n
```

主体是在恒等改名下于 `c` 处应用结构读式，充分性陈述同样取 `PairIs` 路径的形式：`c` 处的集合等于元数值与「`# k` 与 `a` 处的值之对」的配对。当码的载荷是单个槽位而非两个时，需要的正是这个形状，例如一个变元指标或一个子公式槽位。

```agda
arityTagAtL c ar k a = PairExpression.read
  (PairExpression.pair (PairExpression.slot ar)
    (PairExpression.pair (PairExpression.numeral k) (PairExpression.slot a))) id c

arityTagAtL-adequate : ∀ {n} (c ar : Fin n) (k : ℕ) (a : Fin n) (γ : S ^ n)
  → (γ ⊨ arityTagAtL c ar k a)
```

充分性证明再次在同样的表达式与槽位上引用 `PairExpression.adequate`，与配对情形如出一辙。因此两个元数标签公式与两个充分性引理都立足于那一个结构定理，这正是把读式写成通用形式所得到的回报。至于恢复出的元数值之后如何使用，属于满足关系递归的子句，它们陈述于 `L.Coding.SatisfactionClauses`；本章给出的正是那些子句所读取的形状。

```agda
  ≡ PairIs (fst (lookup c γ))
      (pr (fst (lookup ar γ)) (pr (# k) (fst (lookup a γ))))
arityTagAtL-adequate c ar k a γ = PairExpression.adequate
  (PairExpression.pair (PairExpression.slot ar)
    (PairExpression.pair (PairExpression.numeral k) (PairExpression.slot a))) id c γ
```

## 在表中查一个子码

满足关系表的一个条目记录的是：对由元数与码组成的键，满足该公式的环境之集。因此读取一个子公式的取值，意味着在对象语言内部构造那个键：把元数与子码配成对，并断言其与一个候选集合相等。在子公式自身的元数处，公式全称遍历表中条目，并以键相等作为蕴含的前件来选出相符条目；当子公式绑定变元时，同样的查表发生在下一个元数处，该元数由下一节的后继公式在内部给出见证。

## 一条子句的形状

递归的一条子句绑定码、其元数、其载荷分量以及表在该码处记录的取值，然后断言码的带标签形状，并在被记录的取值之间陈述一条构造子特有的条件。把子句读回去，是沿本章建立的诸充分性引理作一串改写；而组装一条子句，就是把这些改写反向运行。

## 正的联结词

对合取与析取而言，那条构造子特有的条件很小：码处的取值是两个子取值的逐点合取，或逐点析取，都从同一元数处的表读出。该条件之外子句所需的一切，就是上面的查表机制。

## 周遭环境集

`envSetAt` 以外延刻画描述一个集合：以一个槽位所存元数为元数、相对于另一槽位中的载体的环境之集。它刻画这个集合，而不构造它。

该定义把外延刻画施于槽位 `E`，条件取为环境谓词 `envOverAt`。这个谓词相对于一个定义域与一个值域，对单个候选环境加以分类，因此 `extAt` 新绑定的变元 (位于扩展环境的零号位置) 就扮演候选者的角色。定义域与值域的参数写作 `suc ar` 与 `suc B`，因为条件是在扩展环境中求值的，比公式自身绑定的槽位高一个元数。由投影 `extAt-out` 与 `extAt-in`，`envSetAt E ar B` 的证明恰给出一对蕴含：`E` 处的集合恰含那些以 `ar` 处记录的元数为元数、且为 `B` 处载体所容纳的候选环境。这条公式只描述集合；其构造发生在构造满足关系表之处。

```agda
envSetAt : ∀ {n} → Fin n → Fin n → Fin n → Formula S n
envSetAt E ar B = extAt E (envOverAt zero (suc ar) (suc B))
```

## 蕴含与底

在诸逻辑子句之中，蕴含与底在取值形状上不同于正的联结词。底没有子码，并在共同的外延框架中以假为条件，故其取值为空；它仍使用框架所绑定的周遭环境集。蕴含则在该码元数处的全体环境之集上解释，故其子句必须点名那个周遭集合，并以外延方式约束它；这也正是上一节的环境之集存在的原因。蕴含写成蕴含式，而非「前件之补与后件之并」，才与`hProp` 上的函数空间蕴涵相合；直接使用蕴含正合构造性语义，并不调用排中律。

## 下一个元数

`sucAtL` 是断言槽位 `j` 中的集合等于槽位 `i` 中集合之 `sucV` 的内部公式；其充分性引理适用于任意集合，并不假定两者是数码或序数。

当子公式比原式高一个元数时，子句必须在受约束为当前元数后继的元数处查询表。层级一侧的公式 `sucAt` 表达这一集合等式，且不点名常元。抬升它需要 `liftFo` 所要求的 `BoundedFo InL` 参数；另一个独立定理 `Δ₀-sucAt` 则稍后交给 `transferFo`，用来证明有界绝对性。

定义为 `sucAtL i j = liftFo (sucAt i j) _`。由于 `sucAt` 不含常元，其 `BoundedFo InL` 参数没有非平凡的常元可构造性见证。在充分性证明中，`transferFo` 分别接收这个参数与 `Δ₀-sucAt i j`，后者才是层级一侧的 Δ₀ 证书。所得路径把满足等同于 `PairIs (fst (lookup j γ)) (sucV (fst (lookup i γ)))`：即槽位 `j` 的集合是槽位 `i` 集合的后继集这一命题。

```agda
sucAtL : ∀ {n} → Fin n → Fin n → Formula S n
sucAtL i j = liftFo (sucAt i j) _

sucAtL-adequate : ∀ {n} (i j : Fin n) (γ : S ^ n)
  → (γ ⊨ sucAtL i j) ≡ PairIs (fst (lookup j γ)) (sucV (fst (lookup i γ)))
sucAtL-adequate i j γ =
```

证明串联三条路径。转换引理先借有界性证书，把抬升公式在 `L` 中的满足等同于 `sucAt i j` 在投影赋值 `map fst γ` 处的周遭满足；该转换立足于既有的传递模型设置。层级一侧的充分性定理 `sucAt-adequate` 随后把那个满足改写为被解释取值之间的等式。最后，`lookup-fst` 把投影赋值处的两次查表换成 `γ` 中查表后的投影，同余把 `sucV` 移到内部，再由 `cong₂` 在 `PairIs` 之下重新组装等式。所得即所陈述的等同。

```agda
    transferFo (sucAt i j) _ (Δ₀-sucAt i j) γ
  ∙ sucAt-adequate i j (map fst γ)
  ∙ cong₂ PairIs (lookup-fst j γ) (cong sucV (lookup-fst i γ))
```

## 扩展一个环境

`consAtL` 描述以一个新的首值扩展环境，其充分性引理准确对应所得的码化环境。

量词主体在当前环境前添入一个取值后求值。层级一侧的公式 `consAt` 已刻画这一运算，`consAtL` 则要在可构造模型内部表达同一刻画。抬升所需的有界性证书分别对应组成码化扩展的单集、配对、标签和键移位关系。这些关系没有引入常元数码：指定标签是空集，而新的首值从槽位 `m` 读取。紧接着在此定义的独立引理 `numL` 记录周遭数码的可构造性，供确实点名数码的其他有界公式使用。

`numL k` 在此定义，并证明周遭数码 `# k` 可构造。内部数码 `numeralL k` 已带有其投影可构造的证明，`numeralL-fst k` 把该投影与 `# k` 等同；沿此路径搬运证书，便得到 `⟨ isL (# k) ⟩`。随后的私有定义为识别空标签的公式提供 `BoundedFo InL` 数据：既记录有界形状，也为其中出现的常元给出可构造性见证。其中 `sgl0At k` 把槽位 `k` 中的集合刻画为 `{∅}`：它有一个空成员，并且每个成员都是空的。`bddSgl0` 给出这种组合数据，而不是一条独立的 Δ₀ 定理。

```agda
numL : (k : ℕ) → InL (# k)
numL k = subst (λ w → ⟨ isL w ⟩) (numeralL-fst k) (numeralL k .snd)

private
  bddSgl0 : ∀ {n} (k : Fin n) → BoundedFo InL (sgl0At k)
  bddSgl0 k = (_ , (_ , _)) , (_ , (_ , _))
```

`pair0At k j` 把槽位 `k` 中的集合刻画为无序对 `{∅, W}`，其中 `W` 是原赋值槽位 `j` 的取值；进入内部量词后，同一取值由 `suc j` 指向。它并不是两个槽位取值的 Kuratowski 对。`tag0At s x` 再组合 `sgl0At` 与 `pair0At`：两个指定成员分别是 `{∅}` 与 `{∅, W}`，所以槽位 `s` 中的集合就是 Kuratowski 对 `pr ∅ W`。`bddPair0` 与 `bddTag0` 为这些描述给出 `BoundedFo InL` 数据，其中包括所需的常元可构造性见证。

```agda
  bddPair0 : ∀ {n} (k j : Fin n) → BoundedFo InL (pair0At k j)
  bddPair0 k j = (_ , (_ , _)) , ((_ , _) , (_ , ((_ , _) , (_ , _))))

  bddTag0 : ∀ {n} (s x : Fin n) → BoundedFo InL (tag0At s x)
  bddTag0 {n} s x =
      (_ , bddSgl0 {suc n} zero)
```

`bddTag0` 的其余部分把用于空集标签本身的单集证书，与外、内两层配对的证书配成对。其后 `bddShift` 为 `shiftPairAt p' p` 作证：`p'` 处的条目是由 `p` 处的条目把其数码键换成其后继、而配对的值保持不变所得；这里证书写成一个占位符，因为该公式的有界子公式仍是已被覆盖的叶子与有界量词。

```agda
    , ( (_ , bddPair0 {suc n} zero (suc x))
      , (_ , (bddSgl0 {suc n} zero , bddPair0 {suc n} zero (suc x))) )

  bddShift : ∀ {n} (p' p : Fin n) → BoundedFo InL (shiftPairAt p' p)
  bddShift p' p = _

  bddCons : ∀ {n} (e' m e : Fin n) → BoundedFo InL (consAt e' m e)
```

`bddCons` 装配扩展公式所需的一切。按其三个合取项来读：扩展后的图持有一个条目，即架在 `m` 处之值上的空集标签，也就是新的首条目，由移位槽位处的 `bddTag0` 作证；旧图的每个条目带其后移的键重现，由高两个元数处的 `bddShift` 作证；其余合取项为从扩展中向外读出的隶属方向重复这两个证书。每个合取项的证书位于其量词所创造的深度，这正说明注记中的元数增长到 `suc (suc n)`。

```agda
  bddCons {n} e' m e =
      (_ , bddTag0 {suc n} zero (suc m))
    , ( (_ , (_ , bddShift {suc (suc n)} zero (suc zero)))
      , (_ , ( bddTag0 {suc n} zero (suc m)
             , (_ , bddShift {suc (suc n)} (suc zero) zero) )) )
```

有界性证书装配齐备之后，`consAtL e' m e` 就是层级一侧公式 `consAt e' m e` 经 `liftFo` 的抬升，其证书由 `bddCons` 提供。它的充分性陈述带有一个后继情形所没有的条件：给定一个族 `g : Fin k → V ℓ`，以及「槽位 `e` 中的集合是码化环境 `env g`」的证明 `hE`。在该假设下，`consAtL e' m e` 的满足作为一个真值被等同于 `PairIs (fst (lookup e' γ)) (env (cons (fst (lookup m γ)) g))`：`e'` 处的集合恰是把 `m` 处的取值推到 `g` 前端所得的码化环境。这条公式是针对一个已被码化的环境作分类，而非构造环境；关于旧环境的那个假设，正是使这一分类适定的前提。

```agda
consAtL : ∀ {n} → Fin n → Fin n → Fin n → Formula S n
consAtL e' m e = liftFo (consAt e' m e) (bddCons e' m e)

consAtL-adequate : ∀ {n} (e' m e : Fin n) (γ : S ^ n)
  {k : ℕ} (g : Fin k → V ℓ)
  → fst (lookup e γ) ≡ env g
```

证明以转换引理开场，一次给足它的全部输入：公式 `consAt e' m e`、其有界性证书 `bddCons`、以及层级一侧记录的 Δ₀ 证书 `Δ₀-consAt`。这一步是有界绝对性的实际运用，并依赖于既已建立的传递模型设置：由于 `L` 传递、且公式点名的每个常元都可构造，抬升公式在载体中的满足，就移为原公式在投影赋值 `map fst γ` 处的满足，而在那里周遭的事实可以直接陈述。

```agda
  → (γ ⊨ consAtL e' m e)
  ≡ PairIs (fst (lookup e' γ)) (env (cons (fst (lookup m γ)) g))
consAtL-adequate e' m e γ g hE =
    transferFo (consAt e' m e) (bddCons e' m e) (Δ₀-consAt e' m e) γ
  ∙ consAt-adequate e' m e (map fst γ) g
```

层级一侧的充分性定理 `consAt-adequate` 随后把周遭满足改写为新槽位与扩展后的码化环境的等同。它需要假设以投影形式给出，这正是入口处把 `lookup-fst e γ` 与 `hE` 串联的原因：`e` 处条目的投影等于 `env g`。接着，同余移走剩下的两次查表：`e'` 处的取值由 `lookup-fst` 处理，`m` 处的取值在函数 `λ w → env (cons w g)` 之下由 `cong` 处理。路径链条的终点恰是所允诺的 `PairIs` 等同。本章自身的数学至此收束：识别语法形状、元数、环境及其扩展所需的每条内部公式都已就位。

```agda
      (lookup-fst e γ ∙ hE)
  ∙ cong₂ PairIs (lookup-fst e' γ)
      (cong (λ w → env (cons w g)) (lookup-fst m γ))
```

## 无界量词

两条无界量词子句使用共同的有界框架 `extB`；它先绑定周遭环境集 `F` 与扩展数据，再应用量词专有的主体。在 `quBody q` 中，参数 `q` 是遍历载体集 `w` 的外层量词：存在情形取有界存在，全称情形取有界全称。内部公式 `∃̇∈ ya (consAtL ...)` 表示扩展环境出现在主体所记录的取值中，在两种情形下都不改变。因此，全称情形只把外层量词改成蕴含语义，并没有把某个最内层合取改成蕴含。

## 求一个词项的值，与两个原子

一个词项是变元或常元，故求值码化词项的子句有两种情形：变元的取值是环境在其键处记录的东西，而常元的取值就是那个常元，在任何环境中都一样。两个原子随后求出两个词项码的值并在模型中比较所得，其一断言隶属，另一断言相等；它们的载荷是一对词项码，满足关系表在该处没有条目，这正是该子句自行构造查表、而不由框架代劳的原因。

## 有界量词

有界量词的载荷是「词项码与公式码的对」。界由两情形的求值读式在环境中求值，主体的取值在高一个元数处读出，而被推入的取值同时限于载体与所得界中的元素。同时遍历载体与那个界并非冗余：参照语义是在载体上作量化、再以「属于那个界」设防，而一个界完全可以有落在载体之外的成员；只在那个界上作量化，就会索要表所没有的条目。

## 小结

本章建立了码化满足关系的子句在 `L` 内部识别复合取值所需的一阶公式。支撑它的是三类陈述。表达式读式的结构充分性在两个方向上把「关于槽位、字面常元、数码与 Kuratowski 对的公式」的满足，等同于「投影条目与所指周遭取值」的相等，配对情形经由一个可构造的中间集合完成。外延刻画 `extAt` 是两条全称蕴含的普通合取，其读法与引入就是投影与配对。内部的后继公式与环境扩展公式由传递模型上的有界绝对性抬升，其充分性路径由转换后的满足、层级一侧的定理、以及查值在投影下的相容性串联而成。码化满足关系递归的诸子句形状正立足于此。