---
title: "使编码槽位对七种构造闭合"
module: L.Coding.SlotClosure
lang: zh
site: "Bedrock"
description: "使编码槽位对七种构造闭合"
stage: "内部编码：表与统一满足关系"
reading_order: 53
canonical: https://bedrock.institute/zh/L.Coding.SlotClosure.html
html: L.Coding.SlotClosure.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/Coding/SlotClosure.lagda.md
prerequisites: [Base.Prelude, Base.Classical, FOL.ZFStructure, FOL.Syntax, FOL.Absoluteness, V.Hierarchy, V.Coding, L.Constructible, L.Coding.Model, L.Coding.Closure, L.Axioms.Numerals, L.Coding.SatisfactionTable]
routes: [internal-satisfaction]
translations: [https://bedrock.institute/en/L.Coding.SlotClosure.md, https://bedrock.institute/ja/L.Coding.SlotClosure.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
# 使编码槽位对七种构造闭合

在 `L` 内部，每条公式都被编码为载体的元素，且每条公式都有一个键：以元数数码居前、公式编码居后的有序对。某个界处的槽位收集一条公式及其全部子公式的键，因此槽位是一棵键树，而界只是相关引理的接口参数。本章证明槽位是闭合的：凡复合公式的键位于槽位中，其直接子公式的键也位于其中；这对带子公式的七种构造子逐一成立。

抽象的闭合原理在这里落实到具体对象：由公式语法树生成的诸键满足 `closedAt`。这正是沿这些键递归定义图时所需的闭合前提。

语言的构造子中有七个带子公式，其余三个不带，对后者无可闭合。七条子句各是四个动作：把槽位的成员求逆回「它是谁的键」的那条公式、从子句的标签算出那条公式的构造子、把部件的键放回复合公式自己的槽位、再把它们提升到整体的槽位。

本章围绕三个数学对象展开。元数为 `j` 的公式 `χ` 的键 `keyʟ χ` 是数码 `j` 与 `χ` 的编码构成的有序对，而编码本身是编码模块的编码 `LCode.⌜ χ ⌝`。槽位 `slot B φ` 是由这类键组成的集合，即 `φ` 及其整棵子公式树的键。`closedAt` 则陈述：一个槽位对七个构造子闭合，即合取、析取、蕴含、两个量词与两个有界量词。

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

open import Base.Prelude
open import Base.Classical using ( LEM )

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

公式即对象语言的公式，其满足在可构造结构中读取：下文的满足符号一律指那里的满足。外围层级提供键与槽位所由构成的底层元素。

```agda
open import FOL.ZFStructure using ( module hPropStructure )
open import FOL.Syntax
  using ( Term; Formula; _∧̇_; _∨̇_; _⇒̇_; ∃̇_; ∀̇_; ∀̇∈; ∃̇∈ )
import FOL.Absoluteness
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ )
```

有序对编码键，且分量可恢复，因此一个键可以拆开为元数分量与编码分量。可构造结构承载诸编码；编码模块定义公式的编码 `⌜_⌝` 与码上的配对运算；闭包模块则逐形状陈述七条闭合子句及其引入形式。

```agda
open import V.Coding {ℓ} using ( pr; pr-inj )
open import L.Constructible {ℓ} using ( 𝒮ʟ; isL; isL-trans )
open import L.Coding.Model {ℓ} using ( module LCode; prʟ; prʟ-fst )
open import L.Coding.Closure {ℓ} using ( closedAt; binSameClosed-in; unSameClosed-in; unSuccClosed-in; binSuccClosed-in; binShapeAt; unShapeAt; bothSameAt; oneSameAt; oneSuccAt; succSndAt )
```

满足表一章是三个核心对象的出处。它定义了公式的键 `keyʟ`、按构造子标签分解公式的形状引理 `keyʟ-shape`、挂在公式与某个界上的槽位 `slot`、把槽位成员求逆回其键所属公式的 `slot-inv`，以及关于键树的部件引理 `Parts`。

```agda
open import L.Axioms.Numerals {ℓ} using ( numeralL; numeralL-fst )
open import L.Coding.SatisfactionTable {ℓ} lem
  using ( keyʟ; keyʟ-shape; slot; satTable; slot-inv; module Parts )
```

槽位成员只能在命题截断下求逆，因此每条子句都把该截断消去到一个命题。保持元数的二元情形以两个隶属命题的合取为目标；一元情形与有界情形的目标则各是一个隶属命题。

```agda
import Cubical.HITs.PropositionalTruncation as PT
open import Cubical.Foundations.HLevels using ( isProp× )
open import Cubical.HITs.CumulativeHierarchy.Base using ( V; _∈_ )
open import Cubical.HITs.CumulativeHierarchy.Constructions
  using ( module InfinitySet )
```

元数以数码记录，而抬升元数的构造子记录的是数码的后继；二者都取自外围的无穷集合。

```agda
open InfinitySet using ( #_; sucV )
```

可构造结构的载体是本章一切码、键与槽位所居的类型。

```agda
open hPropStructure 𝒮ʟ
```

这里的 `S ^ n` 表示长度为 `n` 的环境向量；重命名为 `_⊨_` 的关系，则是在这种环境下读取限制可构造结构中的满足。

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

## 把部件的键放回去

键树由部件引理支配。`Parts.self` 说公式自己的键在自己的槽位中；`Parts.left`、`Parts.right` 与 `Parts.only` 说复合公式的槽位包含其直接部件槽位中的键：这是沿构造子树的子树包含，由部件引理与求逆给出，从不来自界的任何序或向下的闭合。界 `B` 在其中只是作为接口参数传递。于是闭合子句所需做的，是把子句所读的对认作某个部件的键；下面两条引理恰完成此事。

```agda
module _ (B : S) where
  private
    Sl : ∀ {n} → Formula S n → S
    Sl = slot B
```

键的计算，就元数为 `j` 的公式 `χ` 陈述：凡第一分量为元数数码 `# j`、第二分量为 `⌜ χ ⌝` 的编码分量的对，都等于键 `fst (keyʟ χ)`。注意三个量互不相同：`⌜ χ ⌝` 是公式的编码，其第一分量才是进入键的那个量，而键是数码居前的有序对。

```agda
  key≡ : ∀ {j} (χ : Formula S j) (ar p : V ℓ) → # j ≡ ar
       → p ≡ fst LCode.⌜ χ ⌝ → pr ar p ≡ fst (keyʟ χ)
```

两条假设都必须用到：元数等式与编码分量等式。证明是穿过两条计算法则的短链：`j` 的数码的第一分量是 `# j`，而编码对的第一分量是第一分量的对。

```agda
  key≡ {j} χ ar p qa qp =
      cong₂ pr (sym qa) qp
    ∙ cong (λ w → pr w (fst LCode.⌜ χ ⌝)) (sym (numeralL-fst j))
    ∙ sym (prʟ-fst (numeralL j) LCode.⌜ χ ⌝)
```

抬升形式对元数为 `suc j` 的公式 `χ` 陈述同一事实：此时键的第一分量是元数数码的后继，而这恰是构造子抬升元数时子句所读取的量。

```agda
  keyS≡ : ∀ {j} (χ : Formula S (suc j)) (ar p : V ℓ) → # j ≡ ar
        → p ≡ fst LCode.⌜ χ ⌝ → pr (sucV ar) p ≡ fst (keyʟ χ)
```

链是同一条，只是把后继沿元数等式推过去：`suc j` 的数码的第一分量是 `suc (# j)`，而子句的抬升读法与之相合。

```agda
  keyS≡ {j} χ ar p qa qp =
      cong₂ pr (cong sucV (sym qa)) qp
    ∙ cong (λ w → pr w (fst LCode.⌜ χ ⌝)) (sym (numeralL-fst (suc j)))
    ∙ sym (prʟ-fst (numeralL (suc j)) LCode.⌜ χ ⌝)
```

## 七条子句

子句按各构造子所要求的闭合形状组织。共证明四个主体，每种形状一个：保持元数的二元构造子、保持元数的一元构造子、抬升元数的一元构造子、把项与抬升元数公式配对的二元构造子。同一主体下两条子句的不同只在构造子的标签与其交还的部件，而两者都是参数。每条子句经四个动作运行：把槽位成员求逆成一条公式、按标签读出其构造子、把部件的键放回该公式自己的槽位、再提升到整体的槽位。

```agda
  module _ {n : ℕ} (φ : Formula S n) {k : ℕ} (γ : S ^ k) where
    private
      δ : S ^ (suc (suc (suc k)))
      δ = B ∷ satTable B φ ∷ Sl φ ∷ γ
```

被证明闭合的递归以固定公式 `φ` 的槽位为索引，其环境携带三个具名条目：界、`φ` 处的满足表，以及该槽位。环境的其余槽位留给具体实例。

```agda
      Ci : Fin (suc (suc (suc k)))
      Ci = suc (suc zero)
```

位置 `Ci` 是槽位在此环境中的索引；每条子句都恰在这个位置读取槽位。

```agda
    binSame : (k' : ℕ) (op : ∀ {m} → Formula S m → Formula S m → Formula S m)
            → (∀ {m} (ψ : Formula S m) → LCode.Match k' ψ
               → Σ[ a' ∈ Formula S m ] (Σ[ b' ∈ Formula S m ] (ψ ≡ op a' b')))
            → (∀ {m} (a' b' : Formula S m)
               → LCode.payOf (op a' b') ≡ prʟ LCode.⌜ a' ⌝ LCode.⌜ b' ⌝)
```

第一个主体覆盖保持元数的二元构造子，即合取、析取、蕴含的形状。其假设描述标签 `k'`：一条公式与该标签匹配，当且仅当它由同元数的两条公式 `op a' b'` 构成，且这种复合的载荷是两个部件编码构成的有序对。

```agda
            → (∀ {m} (a' b' : Formula S m) (z : V ℓ)
               → ⟨ z ∈ fst (Sl a') ⟩ → ⟨ z ∈ fst (Sl (op a' b')) ⟩)
            → (∀ {m} (a' b' : Formula S m) (z : V ℓ)
               → ⟨ z ∈ fst (Sl b') ⟩ → ⟨ z ∈ fst (Sl (op a' b')) ⟩)
            → ⟨ δ ⊨ binShapeAt Ci k' (bothSameAt Ci) ⟩
```

两条闭合方向分别是部件引理给出的左、右子树包含；结论即子句自身：槽位对标签 `k'` 以「交还两个部件的键」的形状闭合。

```agda
    binSame k' op get payOp inL inR = binSameClosed-in Ci k' δ
      (λ c ar a b c∈ sh → PT.rec
        (isProp× (snd (pr (fst ar) (fst a) ∈ fst (Sl φ)))
                 (snd (pr (fst ar) (fst b) ∈ fst (Sl φ))))
        (λ { (m , ψ , (q , incl)) →
```

第一步对槽位成员 `c` 求逆。它仅仅地是某条元数为 `m` 的公式 `ψ` 的键，求逆同时返回该键属于 `φ` 的槽位。目标是两个隶属的合取，由 `isProp×` 是命题，这使截断消去合法。

```agda
          let r  = keyʟ-shape ψ k' (fst ar) (pr (fst a) (fst b)) (sym q ∙ sh)
              g  = get ψ (r .fst)
              a' = g .fst
              b' = g .snd .fst
              eψ = g .snd .snd
```

第二步计算构造子。形状引理以子句的形状证明把 `ψ` 对上标签 `k'`，随同匹配返回元数等式与载荷等式；分解假设进而把 `ψ` 写成两个直接子公式的 `op a' b'`。

```agda
              pay = sym (prʟ-fst LCode.⌜ a' ⌝ LCode.⌜ b' ⌝)
                  ∙ cong fst (sym (payOp a' b'))
                  ∙ cong (λ w → fst (LCode.payOf w)) (sym eψ) ∙ r .snd .snd
```

第三步是关于载荷的共享计算。成员 `c` 是键形的对，其载荷分量记录着两个部件的编码分量；链条证明这些被记录的分量按分量分别是编码 `⌜ a' ⌝` 与 `⌜ b' ⌝`：由构造子自身的载荷法则，`ψ` 的载荷是两个部件编码构成的对，而形状引理的载荷等式把它与从 `c` 读出的对连接起来。此处切莫混淆三个量：整条公式的编码 `⌜ ψ ⌝`、位于其中的载荷分量，以及第一槽携带元数的最终的键。

```agda
              inψ : (χ : Formula S m) → ⟨ fst (keyʟ χ) ∈ fst (Sl ψ) ⟩
                  → ⟨ fst (keyʟ χ) ∈ fst (Sl φ) ⟩
              inψ χ h = incl (fst (keyʟ χ)) h
          in subst (λ w → ⟨ w ∈ fst (Sl φ) ⟩)
               (sym (key≡ a' (fst ar) (fst a) (r .snd .fst) (sym (pr-inj pay .fst))))
```

第四个动作把键送回。先由辅助函数借求逆返回的包含，把任一同元数公式的键从其槽位提升到 `φ` 的槽位；再由形状引理的元数等式与编码单射性供给的第一分量等式喂给 `key≡`，把子句所读对的隶属改写为 `a'` 的键的隶属。

```agda
               (inψ a' (subst (λ w → ⟨ fst (keyʟ a') ∈ fst (Sl w) ⟩) (sym eψ)
                 (inL a' b' _ (Parts.self B keyʟ a'))))
           , subst (λ w → ⟨ w ∈ fst (Sl φ) ⟩)
               (sym (key≡ b' (fst ar) (fst b) (r .snd .fst) (sym (pr-inj pay .snd))))
```

右分量以右侧闭合方向与单射性供给的第二分量等式重复同一组装，改写为含 `b'` 那个对的隶属。两半合拢，子句证毕。

```agda
               (inψ b' (subst (λ w → ⟨ fst (keyʟ b') ∈ fst (Sl w) ⟩) (sym eψ)
                 (inR a' b' _ (Parts.self B keyʟ b')))) })
        (slot-inv B φ (fst c) c∈))
```

消去由求逆供给，那条包含正是从那里来的。两侧分量组装完毕，子句即告证成。

```agda
    andC : ⟨ δ ⊨ binShapeAt Ci 2 (bothSameAt Ci) ⟩
    andC = binSame 2 _∧̇_ (λ _ m → m) (λ _ _ → refl)
             (λ a' b' → Parts.left B keyʟ (a' ∧̇ b') a' b')
             (λ a' b' → Parts.right B keyʟ (a' ∧̇ b') a' b')
```

合取是第一个实例：`a' ∧̇ b'` 的槽位包含两个合取支槽位的键。

```agda
    orC : ⟨ δ ⊨ binShapeAt Ci 3 (bothSameAt Ci) ⟩
    orC = binSame 3 _∨̇_ (λ _ m → m) (λ _ _ → refl)
            (λ a' b' → Parts.left B keyʟ (a' ∨̇ b') a' b')
            (λ a' b' → Parts.right B keyʟ (a' ∨̇ b') a' b')
```

析取是形状相同的第二个实例，带自己的标签与自己的部件引理。

```agda
    impC : ⟨ δ ⊨ binShapeAt Ci 4 (bothSameAt Ci) ⟩
    impC = binSame 4 _⇒̇_ (λ _ m → m) (λ _ _ → refl)
             (λ a' b' → Parts.left B keyʟ (a' ⇒̇ b') a' b')
             (λ a' b' → Parts.right B keyʟ (a' ⇒̇ b') a' b')
```

蕴含是第三个：`a' ⇒̇ b'` 的槽位包含前件槽位的键与后件槽位的键，子句由同样四个动作证得。

```agda
    unSame : (k' : ℕ) (op : ∀ {m} → Formula S m → Formula S m)
           → (∀ {m} (ψ : Formula S m) → LCode.Match k' ψ
              → Σ[ a' ∈ Formula S m ] (ψ ≡ op a'))
           → (∀ {m} (a' : Formula S m) → LCode.payOf (op a') ≡ LCode.⌜ a' ⌝)
```

辅助引理 `unSame` 证明了一个假想的、保持元数的一元运算所满足的相应闭合原理。本语言的十个构造子都不具有这种形状，因此 `closedAt` 不使用这一辅助引理。

```agda
           → (∀ {m} (a' : Formula S m) (z : V ℓ)
              → ⟨ z ∈ fst (Sl a') ⟩ → ⟨ z ∈ fst (Sl (op a')) ⟩)
           → ⟨ δ ⊨ unShapeAt Ci k' (oneSameAt Ci) ⟩
```

闭合方向与结论都是单部件形状：被要求交还的只有那唯一子公式的键。

```agda
    unSame k' op get payOp inA = unSameClosed-in Ci k' δ
      (λ c ar a c∈ sh → PT.rec (snd (pr (fst ar) (fst a) ∈ fst (Sl φ)))
        (λ { (m , ψ , (q , incl)) →
          let r  = keyʟ-shape ψ k' (fst ar) (fst a) (sym q ∙ sh)
              g  = get ψ (r .fst)
```

证明以一个分量运行同样的四个动作。求逆产出 `ψ` 及其到 `φ` 槽位的包含，形状引理按标签分解它，而此处的读取只涉及元数与那唯一的编码。

```agda
              a' = g .fst
              eψ = g .snd
              pay = cong fst (sym (payOp a'))
                  ∙ cong (λ w → fst (LCode.payOf w)) (sym eψ) ∙ r .snd .snd
          in subst (λ w → ⟨ w ∈ fst (Sl φ) ⟩)
```

这里的共享计算更短：`op a'` 的载荷就是 `a'` 自己的编码，故链条把成员 `c` 中记录的编码分量直接认同为 `a'` 的编码分量，无须拆分任何对。

```agda
               (sym (key≡ a' (fst ar) (fst a) (r .snd .fst) (sym pay)))
               (incl (fst (keyʟ a'))
                 (subst (λ w → ⟨ fst (keyʟ a') ∈ fst (Sl w) ⟩) (sym eψ)
                   (inA a' _ (Parts.self B keyʟ a')))) })
        (slot-inv B φ (fst c) c∈))
```

第四个动作一次性组装该情形：`a'` 的键在自己的槽位中，`inA` 把它移入 `op a'` 的槽位，`incl` 提升到 `φ` 的槽位，`key≡` 完成改写，元数等式包含在内。

```agda
    unSucc : (k' : ℕ) (op : ∀ {m} → Formula S (suc m) → Formula S m)
           → (∀ {m} (ψ : Formula S m) → LCode.Match k' ψ
              → Σ[ a' ∈ Formula S (suc m) ] (ψ ≡ op a'))
           → (∀ {m} (a' : Formula S (suc m)) → LCode.payOf (op a') ≡ LCode.⌜ a' ⌝)
           → (∀ {m} (a' : Formula S (suc m)) (z : V ℓ)
```

第三个主体覆盖抬升元数的一元构造子，即两个量词的形状。其假设是抬升版本：标签恰与由抬升元数公式经 `op` 构成的公式匹配，载荷就是该公式自己的编码，且唯一一条闭合方向把它的键送入复合槽位。

```agda
              → ⟨ z ∈ fst (Sl a') ⟩ → ⟨ z ∈ fst (Sl (op a')) ⟩)
           → ⟨ δ ⊨ unShapeAt Ci k' (oneSuccAt Ci) ⟩
```

读取与结论使用抬升形式：子句读取的对以元数数码的后继居首，并要求子公式的键以单部件形状交还。

```agda
    unSucc k' op get payOp inA = unSuccClosed-in Ci k' δ
      (λ c ar a c∈ sh → PT.rec (snd (pr (sucV (fst ar)) (fst a) ∈ fst (Sl φ)))
        (λ { (m , ψ , (q , incl)) →
          let r  = keyʟ-shape ψ k' (fst ar) (fst a) (sym q ∙ sh)
              g  = get ψ (r .fst)
```

前两个动作照旧：把成员求逆成公式，再按标签分解出唯一的、元数抬升的子公式。

```agda
              a' = g .fst
              eψ = g .snd
              pay = cong fst (sym (payOp a'))
                  ∙ cong (λ w → fst (LCode.payOf w)) (sym eψ) ∙ r .snd .snd
          in subst (λ w → ⟨ w ∈ fst (Sl φ) ⟩)
```

载荷计算把被记录的编码分量认同为子公式的编码。另一方面，形状等式给出 `# m ≡ fst ar`；只有 `keyS≡` 对该等式施加 `sucV` 时，后继才被引入。

```agda
               (sym (keyS≡ a' (fst ar) (fst a) (r .snd .fst) (sym pay)))
               (incl (fst (keyʟ a'))
                 (subst (λ w → ⟨ fst (keyʟ a') ∈ fst (Sl w) ⟩) (sym eψ)
                   (inA a' _ (Parts.self B keyʟ a')))) })
        (slot-inv B φ (fst c) c∈))
```

改写经由 `keyS≡` 完成：它对 `# m ≡ fst ar` 施加 `sucV`，再与编码分量等式合并，从而把子句所读的对认同为 `a'` 的键。

```agda
    binSucc : (k' : ℕ)
            → (op : ∀ {m} → Term S m → Formula S (suc m) → Formula S m)
            → (∀ {m} (ψ : Formula S m) → LCode.Match k' ψ
               → Σ[ t ∈ Term S m ] (Σ[ a' ∈ Formula S (suc m) ] (ψ ≡ op t a')))
            → (∀ {m} (t : Term S m) (a' : Formula S (suc m))
```

第四个主体覆盖有界量词，其构造子把一个项与一个元数抬升的公式配对。这种复合的载荷按次序编码项与子公式，而只有子公式本身是公式，故被要求交回的只有它的键。

```agda
               → LCode.payOf (op t a') ≡ prʟ LCode.⌜ t ⌝ᵗ LCode.⌜ a' ⌝)
            → (∀ {m} (t : Term S m) (a' : Formula S (suc m)) (z : V ℓ)
               → ⟨ z ∈ fst (Sl a') ⟩ → ⟨ z ∈ fst (Sl (op t a')) ⟩)
            → ⟨ δ ⊨ binShapeAt Ci k' (succSndAt Ci) ⟩
```

结论是第二分量形状：子句读取的对以抬升的元数居前、公式的编码分量居后，并要求交回子公式的键。

```agda
    binSucc k' op get payOp inA = binSuccClosed-in Ci k' δ
      (λ c ar a b c∈ sh → PT.rec (snd (pr (sucV (fst ar)) (fst b) ∈ fst (Sl φ)))
        (λ { (m , ψ , (q , incl)) →
          let r  = keyʟ-shape ψ k' (fst ar) (pr (fst a) (fst b)) (sym q ∙ sh)
              g  = get ψ (r .fst)
```

成员 `c` 是键形的对，其载荷携带两个分量：居前的项 `t` 的编码分量，与居后的子公式 `a'` 的编码分量。子句读取的是抬升元数连同第二分量。

```agda
              t  = g .fst
              a' = g .snd .fst
              eψ = g .snd .snd
              pay = sym (prʟ-fst LCode.⌜ t ⌝ᵗ LCode.⌜ a' ⌝)
                  ∙ cong fst (sym (payOp t a'))
```

共享计算把成员中记录的载荷按分量认同为 `⌜ t ⌝ᵗ` 与 `⌜ a' ⌝` 的编码对。改写所消耗的是由编码单射性供给的第二分量等式；项乘坐在第一分量里，随后退出。

```agda
                  ∙ cong (λ w → fst (LCode.payOf w)) (sym eψ) ∙ r .snd .snd
          in subst (λ w → ⟨ w ∈ fst (Sl φ) ⟩)
               (sym (keyS≡ a' (fst ar) (fst b) (r .snd .fst)
                 (sym (pr-inj pay .snd))))
               (incl (fst (keyʟ a'))
```

`keyS≡` 的改写使用元数等式与第二分量等式，落定为子句所读对的隶属。第四个动作随后把 `a'` 的键经它自己的槽位与闭合方向提升到 `φ` 的槽位，而求逆供给那条包含。

```agda
                 (subst (λ w → ⟨ fst (keyʟ a') ∈ fst (Sl w) ⟩) (sym eψ)
                   (inA t a' _ (Parts.self B keyʟ a')))) })
        (slot-inv B φ (fst c) c∈))
```

两个量词例示第三个主体。各自供给标签、分解、定义性成立的载荷等式，以及唯一一条闭合方向：`∃̇ a'` 的槽位包含 `a'` 槽位的键，全称量词亦然。

```agda
    exC : ⟨ δ ⊨ unShapeAt Ci 6 (oneSuccAt Ci) ⟩
    exC = unSucc 6 ∃̇_ (λ _ m → m) (λ _ → refl)
            (λ a' → Parts.only B keyʟ (∃̇ a') a')
```

全称量词是同一主体的第二个实例，带标签七与自己的部件引理。

```agda
    allC : ⟨ δ ⊨ unShapeAt Ci 7 (oneSuccAt Ci) ⟩
    allC = unSucc 7 ∀̇_ (λ _ m → m) (λ _ → refl)
             (λ a' → Parts.only B keyʟ (∀̇ a') a')
```

两个有界量词以标签八与九例示第四个主体：`∀̇∈ t a'` 的槽位包含 `a'` 槽位的键，存在有界量词亦然。

```agda
    allInC : ⟨ δ ⊨ binShapeAt Ci 8 (succSndAt Ci) ⟩
    allInC = binSucc 8 ∀̇∈ (λ _ m → m) (λ _ _ → refl)
               (λ t a' → Parts.only B keyʟ (∀̇∈ t a') a')
```

存在有界量词是七条子句中的最后一条。

```agda
    exInC : ⟨ δ ⊨ binShapeAt Ci 9 (succSndAt Ci) ⟩
    exInC = binSucc 9 ∃̇∈ (λ _ m → m) (λ _ _ → refl)
              (λ t a' → Parts.only B keyʟ (∃̇∈ t a') a')
```

七条子句组装成闭合陈述 `closedAt`：`φ` 在该界处的槽位对每个带子公式的构造子闭合。这就消解了对编码的递归对其索引集陈述的假设；也正因如此，这样的递归才能在每个复合码处求助于直接子公式键处记录的取值。本章的三个对象各尽其用：键识别了子句所读的对，槽位树供给了闭合方向，`closedAt` 汇集了结果。

```agda
    slotClosed : ⟨ δ ⊨ closedAt Ci ⟩
    slotClosed = andC , (orC , (impC
               , (exC , (allC , (allInC , exInC)))))
```