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

若一个公式码定义域中每个构造子键都带有其构造子所要求的公式子码，就称它对直接子公式码封闭；两个原子构造子与底不承担这类义务，因为它们的词项分量与数码分量不是 `closedAt` 的义务。本章解释为什么需要这项要求、以及它说了什么。`L.Coding.Expressions` 中的诸子码子句只在它所查询的码确实带有条目之处约束一张表，因此满足全部十条子句的表可以几乎为空；真正确定取值的是索引集自身的一个性质，而封闭谓词 `closedAt` 恰把这个性质表述为一条对象语言公式。本章用两个量化框架 (二元构造子一个、一元构造子一个) 构造该谓词，实例化三条载荷关系得到其七条子句，并证明这些子句的满足与元层面封闭数据之间的两个方向：把已满足的子句读回其所要求子码的消去，以及从这类隶属数据拼装满足的引入。此后，`closedAt` 便可支持对 `L` 内存储的码作结构归纳。

本章从一个缺陷开始，即已有编码子句的一个漏洞。在 `L.Coding.Expressions` 中，每个复合构造子都带有一条子句，把表在某个码处的条目与其直接子码处的条目联系起来。这类子句只在它所查询的码确实带有条目之处起约束作用，因此一张表可以在几乎为空的情况下满足全部十条子句：取索引集为单独一个**复合**码，在该处放一个值任取的条目，则所有查找子码条目的子句都空洞成立，因为诸子码没有条目。诸子句本身不能确定任何取值；真正起决定作用的是对索引集本身的一项要求：它须含有其每个成员的直接子公式码。这项要求以对象语言的公式表述，就是本章构造的封闭谓词 `closedAt`。

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

open import Base.Prelude
```

这个反例也显示了不修复会如何出错。条目位于一个复合码处，而封闭性恰恰是空子码无法伪装的性质：若索引集含有某个复合码，它就必须含有该码解码出的那些子码。「复合」在此要紧。若把那个条目改放在底公式 `⊥̇` 的码处，`⊥̇` 的子句便会立刻确定取值，因为该子句根本不做任何子码查找。这个小失败正是整个论证的缩影。

```agda
module L.Coding.Closure {ℓ : Level} where
```

修复是一个量化模式，所需的框架与诸子句相同，只是去掉了表。剩下的是形状读式与那个蕴含：对集合中每个该形状的键，某某几个键也在该集合中。一个键是元数与码之对，故一个子键或由同一个元数造出，或对绑定变元的四个构造子由其后继造出。有界全称遍历集合的成员，其余全称遍历解码出的各部分，而蕴含把要求置于形状检查之后。

```agda
open import FOL.ZFStructure using ( module hPropStructure )
open import FOL.Syntax
  using ( Formula; var; _∧̇_; _⇒̇_; ∀̇_; ∀̇∈; ∃̇_ )
```

这些要求分为两种形状。三个二元联结词各贡献两个同元数的公式子码；两个无界量词贡献一个后继元数处的公式子码；两个有界量词只跟随其**第二个**、即公式分量，处在同一后继元数处，因为其第一个分量是词项。这给出七条义务。两个原子与底不添加任何义务：它们的词项与数码分量不是 `closedAt` 的义务，而底如反例所示由其自己的子句直接确定。

```agda
import FOL.Absoluteness
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ )
open import V.Coding {ℓ} using ( pr )
open import L.Constructible {ℓ} using ( 𝒮ʟ; isL; isL-trans )
open import L.Axioms.Numerals {ℓ} using ( sucʟ; sucʟ-fst )
```

框架中陈述的关系是一个参数，七条具体子句由实例化该参数而来。三种实例化覆盖上述分类：对两个分量的同元数要求、对一个分量的同元数要求，以及以存在量词给出更高元数的后继元数要求。每条都是框架自身打开的扩张环境上的一个朴素对象语言公式。

```agda
open import Cubical.Data.Nat using ( _+_ )
```

以存在量词给出的后继是唯一出现「仅仅存在」之处。在抬升元数的那些关系内部，约束变元被见证为框架元数的后继，而这个见证只以截断形式打包：这个命题记录后继的存在，却不把选定的见证保留为数据。后文这些子句的读式会消去该截断；这是合法的，因为它们所输送的隶属主张都是命题。

```agda
import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∣_∣₁ )
```

一切都在集合与隶属的层面陈述。存于 `L` 中的码被读作累积层级的一个元素；子码要求在字面上就是一列隶属陈述：由 `pr` 把元数与载荷配成的对属于定义域集合。这正是该谓词可被传递的原因：它只是关于隶属的对象语言公式的满足，别无其他。

```agda
open import Cubical.HITs.CumulativeHierarchy.Base using ( _∈_ )
open import Cubical.HITs.CumulativeHierarchy.Constructions using ( module InfinitySet )
open InfinitySet using ( #_; sucV )
```

这些公式在 `L` 的载体 `S` 上、于环境 `γ : S ^ n` 中求值，该环境为元数 `n` 的公式提供 `n` 个载体。这里的满足指 `L` 上受限结构中的满足；外围层级的满足关系另用其名，两种读法不会混淆。各框架以自身约束的槽扩张这样的环境，因此其元数是 `4 + n` 这类移位后的和。

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

在扩张环境中，每个框架用从内向外数的 de Bruijn 索引命名自己的槽。二元框架约束四个槽：载荷、载荷、元数、码，故码位于最外层索引；一元框架约束三个。移位映射把原 `n` 个环境变元推过被约束的槽，使框架外指称某值的变元在被量化的公式体内仍指同一个值。

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

四个对象语言读式提供构件，每个读式都带有一条充分性证明，把它的满足等同于它所读取的元层面主张。一个读取「属于某环境槽中存储的集合」；两个检查某个码确是元数与其一个或两个载荷分量的带标记对；一个表达「以某存储元数的后继作为载荷」。形状、隶属与后继都能在对象语言内部读取后，整个封闭要求便收缩为一个公式；本章其余部分展开这个公式说了什么、以及如何满足它。

```agda
open import L.Coding.Model {ℓ} using ( appAt; appAt-adequate )
open import L.Coding.Expressions {ℓ}
  using ( arityTagAtL; arityTagAtL-adequate; arityTagPairAtL; arityTagPairAtL-adequate
        ; sucAtL; sucAtL-adequate )
```

## 对子码封闭的定义域

上一节得到的封闭要求是关于解码后键的量化陈述，本节构造表达它的两条公式。唯一需要的分类按形状划分：一元构造子的解码键给出三个见证，即码、元数与一个载荷分量；二元构造子的解码键多给一个，即第二个分量。因此量化解码键的框架在一元情形量化三个值，在二元情形量化四个值，七条有效构造子的义务就挂在这两个框架上。

要形式化的封闭要求是关于解码后键的一个量化陈述。固定索引 `C`，记 `C` 处存储的集合为 `Cset`。它说的是：对 `Cset` 中每个码 `c`，若 `c` 解码为带构造子数码 `k` 标记的元数 `ar` 并带有载荷分量，则关系 `rel` 对这些数据成立。载荷分量的个数取决于构造子的形状。一元构造子的解码键给出三个见证：码、元数与一个分量；二元构造子的解码键给出四个，再加第二个分量。因此需要两个框架，一个量化三个值，一个量化四个值。

```agda
module _ {n : ℕ} where
```

两个框架都处在环境自由变元个数 `n` 之下：它们在长度为 `n` 的环境内量化，并追加自身约束的槽，二元框架四个，一元框架三个。环境变元必须在这一扩张中保持不变，故 `sh4` 这样的移位把 `n` 个索引逐一推过新约束的槽；在被量化的公式体内，它所指的仍是外面指的那个值。

```agda
  private
    sh4 : Fin n → Fin (4 + n)
    sh4 i = suc (suc (suc (suc i)))
```

在扩张环境中，框架自身的值必须可被指称，de Bruijn 编号以最内层变元为 `0` 做到这一点。对二元框架而言，两个载荷分量占据最内层的两个槽，元数次之，码是四者最外层。正是这四个名字使框架的公式体能准确指到扮演每个角色的那个值，无论框架嵌套多深。

```agda
    c4 n4 a4 b4 : Fin (4 + n)
    c4 = suc (suc (suc zero))
    n4 = suc (suc zero)
    a4 = suc zero
    b4 = zero
```

一元框架少约束一个槽，故其移位把环境变元推过三个槽而非四个；扩张的其余方面完全相同。

```agda
    sh3 : Fin n → Fin (3 + n)
    sh3 i = suc (suc (suc i))
```

其三个被约束槽遵循同样的由内向外的次序：唯一载荷分量最内，元数次之，码最外。两个框架各固定一次之后，凡建立在二元形状上的子句都复用四槽布局，凡建立在一元形状上的子句都复用三槽布局，于是封闭陈述的量化结构总共只写两遍。

```agda
    c3 n3 a3 : Fin (3 + n)
    c3 = suc (suc zero)
    n3 = suc zero
    a3 = zero
```

`binShapeAt` 就是二元框架本身，即去掉表的封闭性要求。它的量词结构是精确的：先由一个有界全称从定义域 `C` 中选出 `c`，然后量化另外三个值 `ar`、`a`、`b`；在配对读式证明 `c` 确实是元数 `ar` 与标签 `k` 及载荷 `a`、`b` 配成的带标签的对这一假设下，关系 `rel` 必须在扩张的环境 `b ∷ a ∷ ar ∷ c ∷ γ` 中成立。关系是参数，因此每条子句以自己的载荷要求实例化同一框架。

```agda
  binShapeAt : Fin n → ℕ → Formula S (4 + n) → Formula S n
  binShapeAt C k rel =
    ∀̇∈ (var C) (∀̇ (∀̇ (∀̇ ( arityTagPairAtL c4 n4 k a4 b4 ⇒̇ rel))))
```

`unShapeAt` 是一元构造子的同一框架：一个载荷分量代替两个，于是少一个被约束的槽，形状读式用 `arityTagAtL` 替代配对版本。其余部分，定义域上的有界全称与指向 `rel` 的蕴含，完全相同。

```agda
  unShapeAt : Fin n → ℕ → Formula S (3 + n) → Formula S n
  unShapeAt C k rel =
    ∀̇∈ (var C) (∀̇ (∀̇ ( arityTagAtL c3 n3 k a3 ⇒̇ rel)))
```

`binShape-out` 是二元框架的消去方向。其类型先取「环境 `γ` 满足任意关系 `rel` 上的该框架」这一证明，然后取选定的码 `c`、元数 `ar` 与分量 `a`、`b`，以及 `c` 属于定义域的隶属假设。

```agda
  binShape-out : (C : Fin n) (k : ℕ) (rel : Formula S (4 + n)) (γ : S ^ n)
    → ⟨ γ ⊨ binShapeAt C k rel ⟩
    → (c ar a b : S)
    → ⟨ fst c ∈ fst (lookup C γ) ⟩
```

其余的假设是形状等式，说 `c` 确实是带标签 `k`、载荷 `a`、`b` 的配对 `ar`。在这些假设下，结论是 `rel` 在扩张环境中的实例，其中被约束的槽恰好按 `b ∷ a ∷ ar ∷ c ∷ γ` 的次序填上这些值。

```agda
    → fst c ≡ pr (fst ar) (pr (# k) (pr (fst a) (fst b)))
    → ⟨ (b ∷ a ∷ ar ∷ c ∷ γ) ⊨ rel ⟩
```

证明很短，因为框架正是为这种读法设计的。假设 `h` 是一个函数，在 `c` 处连同隶属与形状施加它就得到所要的结论，只是形状论证须沿 `arityTagPairAtL` 在扩大环境中的充分性路径作移送：充分性是命题之间的路径，沿它的 `subst` 把证明移到结论所需的形式。

```agda
  binShape-out C k rel γ h c ar a b c∈ shape =
    h c c∈ ar a b
      (subst ⟨_⟩ (sym (arityTagPairAtL-adequate c4 n4 k a4 b4 (b ∷ a ∷ ar ∷ c ∷ γ)))
        shape)
```

`unShape-out` 是一元框架的同一消去。它取 `γ` 对 `unShapeAt C k rel` 的满足、带唯一载荷分量 `a` 与元数 `ar` 的码 `c`，以及 `c` 的隶属假设。

```agda
  unShape-out : (C : Fin n) (k : ℕ) (rel : Formula S (3 + n)) (γ : S ^ n)
    → ⟨ γ ⊨ unShapeAt C k rel ⟩
    → (c ar a : S)
```

形状等式通过一元形状读式 `arityTagAtL` 把 `c` 读作带标签 `k`、唯一载荷 `a` 的配对 `ar`。结论于是住在较短的扩张环境 `a ∷ ar ∷ c ∷ γ` 中，其中被约束的槽恰好填上这些值。

```agda
    → ⟨ fst c ∈ fst (lookup C γ) ⟩
    → fst c ≡ pr (fst ar) (pr (# k) (fst a))
    → ⟨ (a ∷ ar ∷ c ∷ γ) ⊨ rel ⟩
```

与二元情形一样，证明在选定分量处施加框架的函数，并沿 `arityTagAtL` 的充分性路径移送形状证明。这两条消去就是使用者所需的全部：下面七条具体的封闭子句都是通过实例化关系从它们得到的。

```agda
  unShape-out C k rel γ h c ar a c∈ shape =
    h c c∈ ar a
      (subst ⟨_⟩ (sym (arityTagAtL-adequate c3 n3 k a3 (a ∷ ar ∷ c ∷ γ))) shape)
```

四条通用关系描述各种载荷形状，七条封闭性子句使用其中三条。三个二元联结词要求两个分量都属于当前元数处的定义域；两个无界量词要求其唯一分量属于高一个元数处的定义域，这一后继元数通过存在量词给出；两个有界量词只要求**第二个**分量属于高一个元数处的定义域，因为第一个分量是词项。

两条保持元数的关系就是子码隶属的简单合取。在二元框架的四个新条目之下，`bothSameAt C` 断言由索引 `a4` 与 `b4` 指名的两个子公式槽位都已经属于条目 `sh4 C` 所指的那个集合。其一元对应物 `oneSameAt C` 则在一元框架的三个新条目之下给出单条这样的隶属断言，用于其唯一分量与自身同元数的构造子。

```agda
  bothSameAt : Fin n → Formula S (4 + n)
  bothSameAt C = appAt (sh4 C) n4 a4 ∧̇ appAt (sh4 C) n4 b4

  oneSameAt : Fin n → Formula S (3 + n)
  oneSameAt C = appAt (sh3 C) n3 a3

  oneSuccAt : Fin n → Formula S (3 + n)
```

两条抬升元数的关系以存在量词给出后继。位置 `zero` 处的约束变元经 `sucAtL` 被见证为框架元数的后继 `sucV`，并要求这同一见证与分量槽位配对，而该槽位在扩张后的环境中移到了 `suc a3` 或 `suc b4`。`succSndAt` 的配对只涉及第二个槽位 `b4`，因为对有界量词而言，二元键的第一个槽位放的是词项而非子公式。

```agda
  oneSuccAt C = ∃̇ (sucAtL (suc n3) zero ∧̇ appAt (suc (sh3 C)) zero (suc a3))

  succSndAt : Fin n → Formula S (4 + n)
  succSndAt C = ∃̇ (sucAtL (suc n4) zero ∧̇ appAt (suc (sh4 C)) zero (suc b4))
```

这些关系的反向读式由使用者调用，因此每条都直接在相应子句处陈述，并已与其框架复合：若集合中含有某种形状的键，那么相应构造子所需的子键也属于该集合。两条改变元数的读式途中消去一次截断；目标是隶属命题，因此允许该消去。

四个读式把各子句展开回具体的隶属数据，每种载荷形状一个。第一个处理同元数的二元联结词。其输入是完整子句 `binShapeAt C k (bothSameAt C)` 的满足证明，连同形状正确的键：模型元素 `c`、`ar`、`a`、`b`，`c` 在 `C` 处集合中的隶属，以及把 `c` 呈现为「元数 `ar` 与对 `a`、`b` 的编码应用之有序对」的形状等式。

```agda
  binSameClosed-out : (C : Fin n) (k : ℕ) (γ : S ^ n)
    → ⟨ γ ⊨ binShapeAt C k (bothSameAt C) ⟩
    → (c ar a b : S)
    → ⟨ fst c ∈ fst (lookup C γ) ⟩
    → fst c ≡ pr (fst ar) (pr (# k) (pr (fst a) (fst b)))
```

其结论是构造子所要求的合取：由同一元数 `ar` 分别与 `a`、`b` 配成的两个子公式键都属于该集合。证明先运行通用框架消去，再施加充分性转换，它把关于编码隶属读式的满足陈述转换为它所指的普通隶属主张；这一转换是四个读式共用的唯一证明步骤。

```agda
    → ⟨ pr (fst ar) (fst a) ∈ fst (lookup C γ) ⟩
    × ⟨ pr (fst ar) (fst b) ∈ fst (lookup C γ) ⟩
  binSameClosed-out C k γ h c ar a b c∈ shape =
      subst ⟨_⟩ (appAt-adequate (sh4 C) n4 a4 δ) (r .fst)
    , subst ⟨_⟩ (appAt-adequate (sh4 C) n4 b4 δ) (r .snd)
```

第二个读式覆盖同元数的一元构造子。其假设仿照第一个但少一个分量：由 `oneSameAt` 构造的子句的满足证明，键的各部分 `c`、`ar`、`a`，`c` 的隶属，以及把 `c` 呈现为「元数 `ar` 与编码数码 `k` 单独作用于 `a`」之对的形状等式。

```agda
    where
    δ : S ^ (4 + n)
    δ = b ∷ a ∷ ar ∷ c ∷ γ
    r = binShape-out C k (bothSameAt C) γ h c ar a b c∈ shape

  unSameClosed-out : (C : Fin n) (k : ℕ) (γ : S ^ n)
```

结论是一条隶属：`ar` 与 `a` 之对的隶属。由于 `oneSameAt` 从未抬升元数，其中不出现截断，证明就是一元框架消去再加充分性转换。第三个读式转向后继元数：`unSuccClosed-out` 读取由 `oneSuccAt` 构造的子句。

```agda
    → ⟨ γ ⊨ unShapeAt C k (oneSameAt C) ⟩
    → (c ar a : S)
    → ⟨ fst c ∈ fst (lookup C γ) ⟩
    → fst c ≡ pr (fst ar) (pr (# k) (fst a))
    → ⟨ pr (fst ar) (fst a) ∈ fst (lookup C γ) ⟩
```

其假设与前一条一元读式相同，但结论提到后继：所需的子公式键把 `a` 与键元数的后继 `sucV (fst ar)` 配对，而非 `ar` 本身。这正合无界量词：它们绑定变元，故把体存放在高一个元数处。下面三段说明存在见证及其充分性证明如何建立这个结论。

```agda
  unSameClosed-out C k γ h c ar a c∈ shape =
    subst ⟨_⟩ (appAt-adequate (sh3 C) n3 a3 (a ∷ ar ∷ c ∷ γ))
      (unShape-out C k (oneSameAt C) γ h c ar a c∈ shape)

  unSuccClosed-out : (C : Fin n) (k : ℕ) (γ : S ^ n)
    → ⟨ γ ⊨ unShapeAt C k (oneSuccAt C) ⟩
```

第三种读式面向无界量词，抬升了元数。其假设是通常的一元假设：`unShapeAt C k (oneSuccAt C)` 的满足，键的各部分 `c`、`ar`、`a`，`c` 的隶属，以及形状等式。结论把元数 `ar` 换成其后继：所需的子公式键把 `a` 与键元数的后继 `sucV (fst ar)` 配对，而非与 `ar` 本身配对。这正是无界量词所需的读式：它们绑定变元，因此把体存放在高一个元数处。

```agda
    → (c ar a : S)
    → ⟨ fst c ∈ fst (lookup C γ) ⟩
    → fst c ≡ pr (fst ar) (pr (# k) (fst a))
    → ⟨ pr (sucV (fst ar)) (fst a) ∈ fst (lookup C γ) ⟩
  unSuccClosed-out C k γ h c ar a c∈ shape =
```

这里 `oneSuccAt` 内部的存在量词起了作用。子句对后继只是「仅仅存在」式地要求：框架消去所给出的是被命题截断的见证，连同两个证书，即它是元数的后继，且它与 `a` 配对进入该集合。这一截断在此可以消去，因为目标是命题：集合中的隶属是 hProp，故 `PT.rec` 把「仅仅存在」转换为具体的隶属主张，而无须选定某个典范见证。

```agda
    PT.rec (snd target)
      (λ { (z , (sz , ap)) →
        subst (λ w → ⟨ pr w (fst a) ∈ fst (lookup C γ) ⟩)
          (subst ⟨_⟩ (sucAtL-adequate (suc n3) zero (z ∷ δ)) sz)
          (subst ⟨_⟩ (appAt-adequate (suc (sh3 C)) zero (suc a3) (z ∷ δ)) ap) })
```

两个读式的充分性引理随后把这些满足转换为关于模型实际取值的等式与隶属，沿第一条等式的移送把见证处的隶属改写为 `sucV (fst ar)` 处的隶属。于是这条读式恰好在应在之处结束：以后继键的隶属收尾。

```agda
      (unShape-out C k (oneSuccAt C) γ h c ar a c∈ shape)
    where
    δ : S ^ (3 + n)
    δ = a ∷ ar ∷ c ∷ γ
    target = pr (sucV (fst ar)) (fst a) ∈ fst (lookup C γ)
```

第四种读式覆盖有界量词。其假设照搬二元模式：`binShapeAt C k (succSndAt C)` 的满足，四个模型值 `c`、`ar`、`a`、`b`，`c` 的隶属，以及把 `c` 呈现为「`ar` 与对 `a`、`b` 的编码应用之对」的形状等式。

```agda
  binSuccClosed-out : (C : Fin n) (k : ℕ) (γ : S ^ n)
    → ⟨ γ ⊨ binShapeAt C k (succSndAt C) ⟩
    → (c ar a b : S)
    → ⟨ fst c ∈ fst (lookup C γ) ⟩
    → fst c ≡ pr (fst ar) (pr (# k) (pr (fst a) (fst b)))
```

结论只问第二个分量：`sucV (fst ar)` 与 `b` 之对须属于该集合，因为第一个槽放的是有界词项而非子公式。与无界情形一样，`succSndAt` 内部的存在量词以「仅仅存在」的方式给出后继，而该截断的消去合法，因为隶属目标是命题。

```agda
    → ⟨ pr (sucV (fst ar)) (fst b) ∈ fst (lookup C γ) ⟩
  binSuccClosed-out C k γ h c ar a b c∈ shape =
    PT.rec (snd target)
      (λ { (z , (sz , ap)) →
        subst (λ w → ⟨ pr w (fst b) ∈ fst (lookup C γ) ⟩)
```

证明体是上一条读式的二元对应：两个证书经 `sucAtL-adequate` 与 `appAt-adequate` 转换，沿后继等式的移送把配对隶属改写到 `sucV (fst ar)` 处。

```agda
          (subst ⟨_⟩ (sucAtL-adequate (suc n4) zero (z ∷ δ)) sz)
          (subst ⟨_⟩ (appAt-adequate (suc (sh4 C)) zero (suc b4) (z ∷ δ)) ap) })
      (binShape-out C k (succSndAt C) γ h c ar a b c∈ shape)
    where
    δ : S ^ (4 + n)
```

隶属结论的命题性，正是每条后继元数读式中截断消去所需的许可。这四种读式，两条保持元数、两条抬升元数，就是使用者的全部所需：每条封闭性子句都能展开为具体的隶属数据。

```agda
    δ = b ∷ a ∷ ar ∷ c ∷ γ
    target = pr (sucV (fst ar)) (fst b) ∈ fst (lookup C γ)
```

七条子句，及其合取。在消去一侧，读取已满足的 `closedAt` 合取的使用者按需选取其中一条子句，并应用与之配套的读式。引入方向在下一节给出。

首先声明七条子句的名字，类型全部相同：在每个索引 `C` 处，它们都是 `n` 环境上的公式，与该处存储的键的元数一致。其类型中不出现任何环境扩张，因为各框架都在内部以新移位的索引自行应用。

```agda
  andClosedAt orClosedAt impClosedAt : Fin n → Formula S n
  existClosedAt forallClosedAt allInClosedAt exInClosedAt : Fin n → Formula S n

  andClosedAt    C = binShapeAt C 2 (bothSameAt C)
  orClosedAt     C = binShapeAt C 3 (bothSameAt C)
  impClosedAt    C = binShapeAt C 4 (bothSameAt C)
```

每个定义把一个构造子键与恰当的关系配对：数码 2、3、4 是二元联结词，其子句使用 `bothSameAt`；6 与 7 是无界量词，使用 `oneSuccAt`；8 与 9 是有界量词，使用 `succSndAt`。框架 `binShapeAt` 或 `unShapeAt` 的选取取决于构造子码带有两个还是唯一一个载荷分量：二元联结词与有界量词有两个分量，故用 `binShapeAt`；无界量词只有一个分量，故用 `unShapeAt`。量词的体处在后继元数处，而有界量词只有第二个载荷分量是公式，因此其关系只跟随该分量。

```agda
  existClosedAt  C = unShapeAt  C 6 (oneSuccAt C)
  forallClosedAt C = unShapeAt  C 7 (oneSuccAt C)
  allInClosedAt  C = binShapeAt C 8 (succSndAt C)
  exInClosedAt   C = binShapeAt C 9 (succSndAt C)

  closedAt : Fin n → Formula S n
```

`closedAt C` 在单个索引 `C` 处合取全部七条子句。这就是日后被传递到 `L` 中的对象语言谓词：当该合取被满足时，集合在 `C` 处对子码封闭；对码的结构归纳随后逐个合取项推进，每个合取项各有自己的读式。

```agda
  closedAt C =
    andClosedAt C ∧̇ (orClosedAt C ∧̇ (impClosedAt C ∧̇ (existClosedAt C
      ∧̇ (forallClosedAt C ∧̇ (allInClosedAt C ∧̇ exInClosedAt C)))))
```

反方向从元层面真实的子码封闭数据出发，把它转成每条对象语言框架的满足。对同元数子句，给定的隶属事实直接建立所需的载荷隶属；对抬升元数的子句，L 数码 `sucʟ ar` 提供存在量化的后继见证，以及框架所需的等式与隶属证书。

引入方向回答相反的需求：给定元层面的封闭数据，产出子句的满足。对二元框架，`binShape-in` 取函数 `g`，它从键的各部分 `c`、`ar`、`a`、`b`、`c` 的隶属以及形状等式，给出任意关系 `rel` 在扩张环境中的满足；其结论是整个形状 `binShapeAt C k rel` 的满足。

```agda
  binShape-in : (C : Fin n) (k : ℕ) (rel : Formula S (4 + n)) (γ : S ^ n)
    → ((c ar a b : S)
       → ⟨ fst c ∈ fst (lookup C γ) ⟩
       → fst c ≡ pr (fst ar) (pr (# k) (pr (fst a) (fst b)))
       → ⟨ (b ∷ a ∷ ar ∷ c ∷ γ) ⊨ rel ⟩)
```

这正是把量词语义反过来读：有界全称的满足是定义在集合成员上的函数，蕴涵的满足是其前提之证明上的函数。因此把 `g` 施加于键的数据就已得到所需的满足；唯一需要的转换沿 `arityTagPairAtL-adequate` 完成，把框架读取的标记等式与 `g` 收到的形状等式对齐。

```agda
    → ⟨ γ ⊨ binShapeAt C k rel ⟩
  binShape-in C k rel γ g c c∈ ar a b sh =
    g c ar a b c∈
      (subst ⟨_⟩ (arityTagPairAtL-adequate c4 n4 k a4 b4 (b ∷ a ∷ ar ∷ c ∷ γ)) sh)

  unShape-in : (C : Fin n) (k : ℕ) (rel : Formula S (3 + n)) (γ : S ^ n)
```

一元版本少一个分量：`g` 收到 `c`、`ar`、`a`，返回 `rel` 在一元框架扩张环境上的满足，目标是 `unShapeAt C k rel` 的满足。下面的具体引入把 `rel` 实例化为四条关系；对两条抬升元数的关系，子句只以存在量词要求后继，此时数码章的 L 数码 `sucʟ ar` 便充当具体见证，与其证书一起注入截断。

```agda
    → ((c ar a : S)
       → ⟨ fst c ∈ fst (lookup C γ) ⟩
       → fst c ≡ pr (fst ar) (pr (# k) (fst a))
       → ⟨ (a ∷ ar ∷ c ∷ γ) ⊨ rel ⟩)
    → ⟨ γ ⊨ unShapeAt C k rel ⟩
```

同元数的引入通过把通用框架引入与具体关系复合而得到。对一元框架，`arityTagAtL-adequate` 给出的标记等式把框架读取的形状与使用者提供的数据对齐。第一条复合引入 `binSameClosed-in` 把二元框架实例化在 `bothSameAt C` 上：使用者不再对任意关系负责，而是交付元层面的隶属数据，这条引理把该数据重新包装为子句的满足。

```agda
  unShape-in C k rel γ g c c∈ ar a sh =
    g c ar a c∈
      (subst ⟨_⟩ (arityTagAtL-adequate c3 n3 k a3 (a ∷ ar ∷ c ∷ γ)) sh)

  binSameClosed-in : (C : Fin n) (k : ℕ) (γ : S ^ n)
    → ((c ar a b : S)
```

这里 `g` 就是以数据形式陈述的封闭义务：从给定形状的键出发，它须产出两个子公式键的隶属，即元数 `ar` 分别与 `a`、`b` 配成的两对。这条引理把该数据转换为完整子句的满足，因此对码作递归时，只需提供这样的隶属数据即可完成二元联结词的封闭义务。

```agda
       → ⟨ fst c ∈ fst (lookup C γ) ⟩
       → fst c ≡ pr (fst ar) (pr (# k) (pr (fst a) (fst b)))
       → ⟨ pr (fst ar) (fst a) ∈ fst (lookup C γ) ⟩
       × ⟨ pr (fst ar) (fst b) ∈ fst (lookup C γ) ⟩)
    → ⟨ γ ⊨ binShapeAt C k (bothSameAt C) ⟩
```

为构造合取的满足，须把 `g` 返回的两条隶属主张改写为两个 `appAt` 合取项的满足。`appAt` 的充分性引理把两种形态等同起来，这里它的使用方向与消去一侧相反，因为目标此时是从数据读向满足。

```agda
  binSameClosed-in C k γ g = binShape-in C k (bothSameAt C) γ
    (λ c ar a b c∈ sh →
        subst ⟨_⟩ (sym (appAt-adequate (sh4 C) n4 a4 (b ∷ a ∷ ar ∷ c ∷ γ)))
          (g c ar a b c∈ sh .fst)
      , subst ⟨_⟩ (sym (appAt-adequate (sh4 C) n4 b4 (b ∷ a ∷ ar ∷ c ∷ γ)))
```

两个分量按同一读法逐个合取项处理。随后，一元同元数引入 `unSameClosed-in` 对单分量关系重复这一构造，数据形状与二元情形相同，只是少了第二个分量。

```agda
          (g c ar a b c∈ sh .snd))

  unSameClosed-in : (C : Fin n) (k : ℕ) (γ : S ^ n)
    → ((c ar a : S)
       → ⟨ fst c ∈ fst (lookup C γ) ⟩
       → fst c ≡ pr (fst ar) (pr (# k) (fst a))
```

对一元同元数子句，一条隶属主张即可：`g` 给出唯一子公式键的隶属，把它与 `rel` 取为 `oneSameAt C` 的通用一元引入复合，便得到子句的满足。

```agda
       → ⟨ pr (fst ar) (fst a) ∈ fst (lookup C γ) ⟩)
    → ⟨ γ ⊨ unShapeAt C k (oneSameAt C) ⟩
  unSameClosed-in C k γ g = unShape-in C k (oneSameAt C) γ
    (λ c ar a c∈ sh →
      subst ⟨_⟩ (sym (appAt-adequate (sh3 C) n3 a3 (a ∷ ar ∷ c ∷ γ)))
```

最后两条引入抬升元数，先看 `unSuccClosed-in`。其假设 `g` 收到通常的一元键数据，但须得出后继键的隶属：键元数的后继 `sucV (fst ar)` 与 `a` 之对。

```agda
        (g c ar a c∈ sh))

  unSuccClosed-in : (C : Fin n) (k : ℕ) (γ : S ^ n)
    → ((c ar a : S)
       → ⟨ fst c ∈ fst (lookup C γ) ⟩
       → fst c ≡ pr (fst ar) (pr (# k) (fst a))
```

关系 `oneSuccAt` 仅以存在且「仅仅」的方式要求后继，因此任何携带两个证书的见证都可用，证明提供了一个具体见证：L 数码 `sucʟ ar`。它是合格的见证，因为其第一投影法则 `sucʟ-fst ar` 把它的第一分量等同于 `sucV (fst ar)`，而 `sucAtL` 的充分性引理把这条定义等式转换为子句所读取的满足。

```agda
       → ⟨ pr (sucV (fst ar)) (fst a) ∈ fst (lookup C γ) ⟩)
    → ⟨ γ ⊨ unShapeAt C k (oneSuccAt C) ⟩
  unSuccClosed-in C k γ g = unShape-in C k (oneSuccAt C) γ
    (λ c ar a c∈ sh → ∣ sucʟ ar
      , ( subst ⟨_⟩ (sym (sucAtL-adequate (suc n3) zero
```

第二个证书是配对主张。`g` 已经给出后继键的隶属，数码的投影法则把它改写为 `pr (sucʟ ar) (fst a)` 的隶属，再由 `appAt` 的充分性引理转换为配对合取项的满足。把见证与其证书注入命题截断不需要任何命题性前提；那一要求属于消去，而非引入。

```agda
            (sucʟ ar ∷ a ∷ ar ∷ c ∷ γ))) (sucʟ-fst ar)
        , subst ⟨_⟩ (sym (appAt-adequate (suc (sh3 C)) zero (suc a3)
            (sucʟ ar ∷ a ∷ ar ∷ c ∷ γ)))
            (subst (λ w → ⟨ pr w (fst a) ∈ fst (lookup C γ) ⟩)
              (sym (sucʟ-fst ar)) (g c ar a c∈ sh)) ) ∣₁)
```

最后一条引入 `binSuccClosed-in` 覆盖有界量词。其假设 `g` 收到二元键的四个值，须产出第二分量在后继元数下的隶属：`sucV (fst ar)` 与 `b` 之对，因为第一个槽放的是有界词项而非子公式。

```agda
  binSuccClosed-in : (C : Fin n) (k : ℕ) (γ : S ^ n)
    → ((c ar a b : S)
       → ⟨ fst c ∈ fst (lookup C γ) ⟩
       → fst c ≡ pr (fst ar) (pr (# k) (pr (fst a) (fst b)))
       → ⟨ pr (sucV (fst ar)) (fst b) ∈ fst (lookup C γ) ⟩)
```

这一构造与一元后继引入相同，只是施加于把 `rel` 取为 `succSndAt C` 的二元框架：见证仍取 L 数码 `sucʟ ar`，其投影法则仍见证后继，而配对主张只涉及第二分量 `b`，至此有界量词子句便得到满足。

```agda
    → ⟨ γ ⊨ binShapeAt C k (succSndAt C) ⟩
  binSuccClosed-in C k γ g = binShape-in C k (succSndAt C) γ
    (λ c ar a b c∈ sh → ∣ sucʟ ar
      , ( subst ⟨_⟩ (sym (sucAtL-adequate (suc n4) zero
            (sucʟ ar ∷ b ∷ a ∷ ar ∷ c ∷ γ))) (sucʟ-fst ar)
```

二元后继情形使用同一个见证和同两条充分性事实，只是这次用于有界量词的公式分量。于是每条有效构造子子句都有两个读法：满足给出所需的子码隶属，而真实的封闭数据给出满足。这两个方向使 `closedAt C` 正好成为元层面直接公式子码封闭的对象语言表达。

```agda
        , subst ⟨_⟩ (sym (appAt-adequate (suc (sh4 C)) zero (suc b4)
            (sucʟ ar ∷ b ∷ a ∷ ar ∷ c ∷ γ)))
            (subst (λ w → ⟨ pr w (fst b) ∈ fst (lookup C γ) ⟩)
              (sym (sucʟ-fst ar)) (g c ar a b c∈ sh)) ) ∣₁)
```

## 小结

`closedAt` 要求定义域中的每个复合码都带上其子句将读取的子公式码。消去引理取出这些子码，引入引理则从元语言的隶属事实构造同样的七项义务。