---
title: "可定义幂集的 Δ₀ 描述"
module: L.GCH.DefinablePowerSetDescription
lang: zh
site: "Bedrock"
description: "可定义幂集的 Δ₀ 描述"
stage: "证明 GCH"
reading_order: 101
canonical: https://bedrock.institute/zh/L.GCH.DefinablePowerSetDescription.html
html: L.GCH.DefinablePowerSetDescription.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/GCH/DefinablePowerSetDescription.lagda.md
prerequisites: [Base.Prelude, Base.Classical, FOL.ZFStructure, FOL.Syntax, FOL.LevyHierarchy, FOL.Manipulation.ConstantMapping, FOL.Absoluteness, V.Hierarchy, V.Coding, L.Constructible, L.Definability, L.Coding.Model, L.Coding.SatisfactionBridge, L.Coding.DefinablePowerSet, L.Coding.CodeSet, L.Coding.UniformSatisfaction, L.Coding.Satisfaction, L.Coding.Quantification, L.Coding.CodeDomain, L.Coding.CodeAlphabet, L.GCH.SatisfactionDescription]
routes: [gch-descriptions]
translations: [https://bedrock.institute/en/L.GCH.DefinablePowerSetDescription.md, https://bedrock.institute/ja/L.GCH.DefinablePowerSetDescription.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
本章要解决的问题是：怎样用有界公式识别一个可构造载体的所有一阶可定义子集，其中允许使用该载体中的参数。这个集合是可定义幂集 `𝒟ₒ`，不是完整的内部幂集。只有当数码标签、码域与满足关系表都具有预期含义时，内部描述才是正确的。

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

这个构造把排中律作为全书唯一的显式经典假设。即便如此，命题截断仍会贯穿本章：存在性证明可以表明某个公式或表值存在，却不从中作出全局选择。

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

固定宇宙层级 `ℓ` 及实例 `lem : LEM (ℓ-suc ℓ)`。本模块的每项结果，包括最后的可靠性与完备性定理，都恰在这一假设下成立。

```agda
module L.GCH.DefinablePowerSetDescription {ℓ : Level} (lem : LEM (ℓ-suc ℓ)) where
```

对象语言中的描述刻意保持有界。它只由隶属原子式、合取、蕴涵、有界存在量词与有界全称量词组成；稍后 `checkΔ₀` 将核验这一句法形状。把外部给定的公式与编码满足构造中的解释相比较时，还需要常元映射。

```agda
open import FOL.ZFStructure using ( module hPropStructure )
open import FOL.Syntax using ( Formula; var; _∈̇_; _∧̇_; _⇒̇_; ∃̇∈; ∀̇∈ )
open import FOL.LevyHierarchy using ( Δ₀; checkΔ₀ )
open import FOL.Manipulation.ConstantMapping using ( mapFo )
import FOL.Absoluteness
```

预期输出是 `𝒟ₒ W`：在 `W` 上的受限结构中、允许使用 `W` 中参数而可定义的子集所成的集合。证明两个隶属方向后，外延性将候选输出与这个集合等同；有序对编码则用来表示环境、公式键与表条目。

```agda
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ; extensionalV )
open import V.Coding {ℓ} using ( pr )
open import L.Constructible {ℓ} using ( 𝒮ʟ; isL; isL-trans; 𝒟ₒ; 𝒟ₒ-intro; 𝒟ₒ-inv )
open import L.Definability {ℓ} using ( module DefOf )
open import L.Coding.Model {ℓ} using ( prAtL; container )
```

对公式 `ψ`，满足构造记录哪些单条目环境满足 `ψ`。桥接定理把由此从 `W` 中切出的部分认同为 `ψ` 所定义的子集。真正的码集包含由 `ψ` 构造的键，而真正满足关系表的函数性固定该键处的取值。只有在 `satAt` 已校准候选码集与表之后，才能使用这些事实；它们既不使解码唯一，也不为某个子集选取定义公式。

```agda
open import L.Coding.SatisfactionBridge {ℓ} lem using ( asConst; defSet-Sat )
open import L.Coding.DefinablePowerSet {ℓ} lem using ( envOne )
open import L.Coding.CodeSet {ℓ} lem using ( keyS; key∈AllCodes )
open import L.Coding.UniformSatisfaction {ℓ} lem using ( module Table; val-at )
open import L.Coding.Satisfaction {ℓ} lem using ( Sat )
```

描述中的每个量词都必须受环境中已有集合约束。下文的辅助量词在这些界限内表达有序对编码的两个分量；它们的两个方向使我们能在对象语言的满足与相应语义见证之间来回转换。

```agda
open import L.Coding.Quantification {ℓ} using
  ( sh; i0; i1; i3; i6; f0; f1; down
  ; sndEx; sndAll; sndEx-out; sndAll-in; fillSnd; useSnd
  ; pr-out; pr-in; sndS )
open import L.Coding.CodeDomain {ℓ} using ( Tags )
```

`Tags` 把十个指定槽位解释为数码零至九。特别地，下文的子句用标签零识别单条目环境，并用标签一识别元数一的键。另一个谓词 `satAt` 提供更强的语义事实：候选码域与表确实实现了该载体上的字母表和递归满足构造。

```agda
open import L.Coding.CodeAlphabet {ℓ} using ( module Alphabet )
open import L.GCH.SatisfactionDescription {ℓ} lem using ( satAt; module SatRead; module Match )
```

环境由可构造集合组成的有限向量表示。积类型合并定义切出关系的两个隶属条件，而这些条件的命题性保证可以把截断见证消去到其中，而不引入选择。

```agda
open import Cubical.Data.Nat using ( _+_ )
open import Cubical.Data.Unit using ( tt )
open import Cubical.Data.Vec using ( _∷_; lookup )
open import Cubical.Data.Sigma using ( _×_ )
open import Cubical.Foundations.HLevels using ( isProp× )
```

证明会反复把逐点的隶属等价转成集合相等。隶属是命题值的，因此在证明任一隶属方向时，可以消去仅仅存在的码、公式或表示；当外围成员需要作为载体元素读取时，`∈-asFiber` 再恢复其呈现索引。

```agda
open import Cubical.Functions.Logic using ( ⇔toPath )
import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∥_∥₁; ∣_∣₁; squash₁ )
open import Cubical.HITs.CumulativeHierarchy.Base using ( V; _∈_; setIsSet )
open import Cubical.HITs.CumulativeHierarchy.Properties using ( ∈-asFiber )
```

用作标签的冯·诺伊曼数码位于累积层级中。特别地，零标记单变元环境的唯一条目，一标记本章所考虑公式的元数。

```agda
open import Cubical.HITs.CumulativeHierarchy.Constructions using ( module InfinitySet )
open InfinitySet {ℓ} using ( #_ )
```

记可构造集合的载体为 `S`。`S` 的元素由底层集合及其可构造性证书组成，因此公式中的有界见证始终留在预期模型内。

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

以 `γ ⊨ φ` 表示对象语言公式在一个可构造集合有限环境处的满足。该记号背后的绝对性结果使后面的语义论证能把这种内部读法与周遭累积层级中的通常隶属相比较。

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

单点环境由一个槽位上的两条有界子句描述：编码集合 `e` 的每个成员都是「标签零与值 `z` 的有序对」，且 `e` 中存在一个成员等于该对。全称子句排除所有其他成员，存在子句排除空集。

```agda
singleOf : ∀ {j} → Fin j → Fin j → Fin j → Formula S j
singleOf e N0 z = ∀̇∈ (var e) (prAtL i0 (sh 1 N0) (sh 1 z)) ∧̇ ∃̇∈ (var e) (prAtL i0 (sh 1 N0) (sh 1 z))
```

可定义子集子句有两个合取支。第一支说编码集合 `x` 的每个成员都属于 `w`，且其单条目环境落在值 `y` 中。第二支说 `w` 的每个成员 `z`，只要其单条目环境落在 `y` 中，就属于 `x`。两者合起来恰好说明 `x` 是由值 `y` 从 `w` 中切出的。

```agda
definesB : ∀ {j} → Fin j → Fin j → Fin j → Fin j → Formula S j
definesB x w y N0 =
    ∀̇∈ (var x) ((var i0 ∈̇ var (sh 1 w)) ∧̇ ∃̇∈ (var (sh 1 y)) (singleOf i0 (sh 2 N0) i1))
  ∧̇ ∀̇∈ (var w) (∃̇∈ (var (sh 1 y)) (singleOf i0 (sh 2 N0) i1) ⇒̇ (var i0 ∈̇ var (sh 1 x)))
```

隶属子句遍历候选值的成员。对每个成员，它只要求候选域 `C` 中有一个形如「标签一与某个第二分量之对」的元素 `c`，并有一个表条目把 `c` 与值 `y` 配对，而 `y` 从 `w` 中切出该成员。此时 `c` 仅具有键的形状；只有稍后加入 `satAt` 假设，才能把它解码为真实公式的键。

```agda
memAt : ∀ {m} → Fin m → Fin m → Fin m → Fin m → (Fin 10 → Fin m) → Formula S m
memAt v w T C N =
  ∀̇∈ (var v) (∃̇∈ (var (sh 1 C)) (sndEx i0 (sh 2 (N f1))
    (∃̇∈ (var (sh 4 T)) (sndEx i0 i3 (definesB i6 (sh 7 w) i0 (sh 7 (N f0)))))))
```

覆盖子句给出反向条件。只要 `C` 的元素 `c` 具有标签一之键的形状，它便仅仅要求 `c` 处有表值 `y`，并且候选输出中有一个由 `y` 切出的成员 `x`。因此它覆盖候选域中每个具有这种形状的元素；要把这些元素认同为全部真实的元数一公式键，仍须依赖 `satAt`。

```agda
allAt : ∀ {m} → Fin m → Fin m → Fin m → Fin m → (Fin 10 → Fin m) → Formula S m
allAt v w T C N =
  ∀̇∈ (var C) (sndAll i0 (sh 1 (N f1))
    (∃̇∈ (var (sh 3 T)) (sndEx i0 i3 (∃̇∈ (var (sh 6 v)) (definesB i0 (sh 7 w) i1 (sh 7 (N f0)))))))
```

公式 `defAt` 合取隶属子句与覆盖子句。它单独只把候选输出同候选码域及表联系起来；与正确的 `Tags` 和 `satAt` 数据结合后，两条子句才成为证明输出等于 `𝒟ₒ W` 的两个包含方向。

```agda
opaque
  defAt : ∀ {m} → Fin m → Fin m → Fin m → Fin m → (Fin 10 → Fin m) → Formula S m
  defAt v w T C N = memAt v w T C N ∧̇ allAt v w T C N
```

在通常论证中，这一定义保持不透明，使后续证明通过两个包含方向这一数学接口使用它，而不依赖冗长的句法展开。只有在核验有界性和证明两个读取方向时，才在局部展开它。

```agda
opaque
  unfolding defAt
```

Δ₀ 证书由结构性检查器产出：该公式只用变元、隶属、合取、蕴涵与有界量词。它证明的是公式的形状，而非描述的正确性。

```agda
  Δ₀-defAt : ∀ {m} (v w T C : Fin m) (N : Fin 10 → Fin m) → Δ₀ (defAt v w T C N)
  Δ₀-defAt v w T C N = checkΔ₀ (defAt v w T C N) tt
```

读取描述即把它拆成两个合取支。

```agda
  defAt-out : ∀ {m} (v w T C : Fin m) (N : Fin 10 → Fin m) (γ : S ^ m)
            → ⟨ γ ⊨ defAt v w T C N ⟩ → ⟨ γ ⊨ memAt v w T C N ⟩ × ⟨ γ ⊨ allAt v w T C N ⟩
  defAt-out v w T C N γ h = h
```

填充描述把两个合取支重新配对。

```agda
  defAt-in : ∀ {m} (v w T C : Fin m) (N : Fin 10 → Fin m) (γ : S ^ m)
           → ⟨ γ ⊨ memAt v w T C N ⟩ → ⟨ γ ⊨ allAt v w T C N ⟩ → ⟨ γ ⊨ defAt v w T C N ⟩
  defAt-in v w T C N γ h1 h2 = h1 , h2
```

第一个语义计算处理 `singleOf`。固定编码集合 `E` 与值 `Z`，并假定指定标签确实指称零。在此前提下，将证明两条有界子句等价于集合等式 `E = envOne Z`。

```agda
module _ {j : ℕ} (e N0 z : Fin j) (δ : S ^ j) (q0 : fst (lookup N0 δ) ≡ # 0) where
  private
    E = fst (lookup e δ)
    Z = fst (lookup z δ)
```

读取单点子句得到「编码集合等于值的标准单点环境」。正向：编码集合的每个成员都是「数码零与值」的有序对，经配对原子的充分性搬运。

```agda
  singleOf-out : ⟨ δ ⊨ singleOf e N0 z ⟩ → E ≡ envOne Z
  singleOf-out (hall , hex) = extensionalV (λ y → ⇔toPath (fwd y) (bwd y))
    where
    fwd : (y : V ℓ) → ⟨ y ∈ E ⟩ → ⟨ y ∈ envOne Z ⟩
    fwd y hy = ∣ lift zero , sym (pr-out i0 (sh 1 N0) (sh 1 z) (down (lookup e δ) y hy ∷ δ) (hall (down (lookup e δ) y hy) hy)
```

证明反向包含时，从标准单条目环境的一个成员出发。存在合取支给出编码集合的某个成员；它的配对等式与已知的零标签一起，把这个成员认同为起初给定的成员。沿此等式搬运隶属证明，便得到原成员属于编码集合。

```agda
                                 ∙ cong (λ a → pr a Z) q0) ∣₁
    bwd : (y : V ℓ) → ⟨ y ∈ envOne Z ⟩ → ⟨ y ∈ E ⟩
    bwd y = PT.rec (snd (y ∈ E))
      (λ { (lift zero , qy) → PT.rec (snd (y ∈ E))
        (λ { (y' , (y'∈ , hy')) →
```

`envOne Z` 的成员是有序对 `pr (# 0) Z`。因此，把标签槽改写为数码零后，这个成员便与 `singleOf` 所要求的有序对认同；它并不与 `Z` 本身认同。

```agda
          subst (λ u → ⟨ u ∈ E ⟩)
            (pr-out i0 (sh 1 N0) (sh 1 z) (y' ∷ δ) hy' ∙ cong (λ a → pr a Z) q0 ∙ qy) y'∈ })
        hex
         ; (lift (suc ()) , _) })
```

反过来，假设编码集合等于标准单条目环境。该环境唯一的索引是零，所以每个成员都具有所需的有序对形式；其余后继索引情形由不可能性排除。典范的零号条目提供有界存在见证，沿所给等式搬运则提供它的隶属证明。

```agda
  singleOf-in : E ≡ envOne Z → ⟨ δ ⊨ singleOf e N0 z ⟩
  singleOf-in q =
      (λ y hy → pr-in i0 (sh 1 N0) (sh 1 z) (y ∷ δ)
         (PT.rec (setIsSet (fst y) (pr (fst (lookup N0 δ)) Z))
           (λ { (lift zero , qy) → sym qy ∙ cong (λ a → pr a Z) (sym q0) ; (lift (suc ()) , _) })
```

该成员被命名，其隶属被搬运，而存在见证把零数码与值配对，并逆着标签等式搬运。

```agda
           (subst (λ u → ⟨ fst y ∈ u ⟩) q hy)))
    , ∣ yS , ( subst (λ u → ⟨ pr (# 0) Z ∈ u ⟩) (sym q) ∣ lift zero , refl ∣₁
             , pr-in i0 (sh 1 N0) (sh 1 z) (yS ∷ δ) (cong (λ a → pr a Z) (sym q0)) ) ∣₁
    where
    yS : S
```

被命名的成员是「零数码与值的对」在编码集合内的呈现。

```agda
    yS = down (lookup e δ) (pr (# 0) Z) (subst (λ u → ⟨ pr (# 0) Z ∈ u ⟩) (sym q) ∣ lift zero , refl ∣₁)
```

集合 `X`、载体 `Wv` 与值 `Y` 之间的切割关系是逐点双向的：`X` 的每个成员都属于 `Wv` 且其单点环境在 `Y` 中；而 `Wv` 中单点环境落在 `Y` 的每个成员都属于 `X`。量化遍历可构造集合，因此该关系在可构造载体上陈述。

```agda
Cuts : (X Wv Y : V ℓ) → Type (ℓ-suc ℓ)
Cuts X Wv Y = ((z : S) → ⟨ fst z ∈ X ⟩ → ⟨ fst z ∈ Wv ⟩ × ⟨ envOne (fst z) ∈ Y ⟩)
            × ((z : S) → ⟨ fst z ∈ Wv ⟩ → ⟨ envOne (fst z) ∈ Y ⟩ → ⟨ fst z ∈ X ⟩)
```

为了把对象语言子句与数学上的切割关系比较，固定 `x`、`w`、`y` 与零标签的槽位。将它们的解释分别记作 `X`、`Wv` 与 `Y`；标签等式恰好使 `singleOf` 能表示标准单条目环境。

```agda
module _ {j : ℕ} (x w y N0 : Fin j) (δ : S ^ j) (q0 : fst (lookup N0 δ) ≡ # 0) where
  private
    X = fst (lookup x δ)
    Wv = fst (lookup w δ)
    Y = fst (lookup y δ)
```

由于 `Y` 是可构造集合，单条目环境属于 `Y` 的任何证明都能转换为该环境的一个载体表示。正是这个呈现使 `definesB` 中的有界存在量词能够在 `Y` 的实际成员上取值。

```agda
    YS = lookup y δ
```

读取单点子句的存在量化，将其转换为标准单点环境在值中的隶属：见证是值的成员，而单点子句把编码条目认同为该索引的标准环境。

```agda
    one-out : (z : S) → ⟨ (z ∷ δ) ⊨ ∃̇∈ (var (sh 1 y)) (singleOf i0 (sh 2 N0) i1) ⟩ → ⟨ envOne (fst z) ∈ Y ⟩
    one-out z = PT.rec (snd (envOne (fst z) ∈ Y))
      (λ { (e , (e∈ , he)) → subst (λ u → ⟨ u ∈ Y ⟩) (singleOf-out i0 (sh 2 N0) i1 (e ∷ z ∷ δ) q0 he) e∈ })
```

填充存在量化是反向：标准单点环境在值内被呈现，而单点子句在延拓环境处填充。

```agda
    one-in : (z : S) → ⟨ envOne (fst z) ∈ Y ⟩ → ⟨ (z ∷ δ) ⊨ ∃̇∈ (var (sh 1 y)) (singleOf i0 (sh 2 N0) i1) ⟩
    one-in z h = ∣ down YS (envOne (fst z)) h , (h , singleOf-in i0 (sh 2 N0) i1 (down YS (envOne (fst z)) h ∷ z ∷ δ) q0 refl) ∣₁
```

读取可定义子集子句便得到切割关系的两个方向。第一个合取支对 `X` 的每个成员给出它属于 `Wv`，以及其单条目环境属于 `Y`；第二个合取支把这两个事实转换回该成员属于 `X`。

```agda
  definesB-out : ⟨ δ ⊨ definesB x w y N0 ⟩ → Cuts X Wv Y
  definesB-out (h1 , h2) = (λ z hz → h1 z hz .fst , one-out z (h1 z hz .snd)) , (λ z hw he → h2 z hw (one-in z he))
```

反过来，`Cuts X Wv Y` 的两个逐点方向填充对象语言中可定义子集子句的两个合取支。上面的私有转换恰在「有界的单条目见证」与「标准单条目环境属于 `Y`」之间往返。

```agda
  definesB-in : Cuts X Wv Y → ⟨ δ ⊨ definesB x w y N0 ⟩
  definesB-in (o , i) = (λ z hz → o z hz .fst , one-in z (o z hz .snd)) , (λ z hw he → i z hw (one-out z he))
```

## 读取有界子集的诸子句

完整读取模块命名四个集合：拟议值、载体、表与码域。

```agda
module Read {m : ℕ} (v w T C : Fin m) (N : Fin 10 → Fin m) (γ : S ^ m) (tg : Tags γ N) where
  private
    Vv = fst (lookup v γ)
    Wv = fst (lookup w γ)
    Tv = fst (lookup T γ)
```

码域的底层集与标签一背后的数码被命名，因为隶属子句选取的码形如「标签一与第二分量」之对。

```agda
    Cv = fst (lookup C γ)
    N1v = fst (lookup (N f1) γ)
```

读取隶属子句对拟议值的每个成员给出截断记录：码域中的一个码 (拆为标签一与某分量之对)、把该码与某值配对的表条目，以及该成员与该值之间的切割关系。记录在截断下存在；不选定任何码或值。

```agda
  mem-out : ⟨ γ ⊨ memAt v w T C N ⟩ → (x : S) → ⟨ fst x ∈ Vv ⟩
          → ∥ Σ[ c ∈ S ] Σ[ p ∈ S ] Σ[ y ∈ S ]
              (⟨ fst c ∈ Cv ⟩ × ((fst c ≡ pr (# 1) (fst p)) × (⟨ pr (fst c) (fst y) ∈ Tv ⟩ × Cuts (fst x) Wv (fst y)))) ∥₁
  mem-out h x x∈ = PT.rec squash₁
    (λ { (c , (c∈ , hc)) → PT.rec squash₁
```

读取隶属子句时，先取得候选码域中具有键形状的成员 `c`，再取得把 `c` 与值 `y` 配对的表条目。配对规格把编码的第二分量转成结果中所示的语义等式，而标签等式把形式标签改写为真正的数码一。

```agda
      (λ { (p , s , (ec , he)) → PT.rec squash₁
        (λ { (e , (e∈ , hy)) → PT.map
          (λ { (y , s' , (ee , hd)) →
            c , p , y , ( c∈ , ( ec ∙ cong (λ a → pr a (fst p)) (tg f1)
                        , ( subst (λ u → ⟨ u ∈ Tv ⟩) ee e∈
```

最内层存在经 `definesB-out` 读取，产出该成员与表条目之值 `y` 之间的切割关系。

```agda
                          , definesB-out i6 (sh 7 w) i0 (sh 7 (N f0)) (y ∷ s' ∷ e ∷ p ∷ s ∷ c ∷ x ∷ γ) (tg f0) hd ) ) ) })
          (sndEx-out i0 i3 (definesB i6 (sh 7 w) i0 (sh 7 (N f0))) (e ∷ p ∷ s ∷ c ∷ x ∷ γ) hy) })
        he })
      (sndEx-out i0 (sh 2 (N f1)) (∃̇∈ (var (sh 4 T)) (sndEx i0 i3 (definesB i6 (sh 7 w) i0 (sh 7 (N f0))))) (c ∷ x ∷ γ) hc) })
    (h x x∈)
```

填充隶属子句是反向构造：它收取为每个成员产出截断记录的函数，并组装子句的满足。

```agda
  mem-in : ((x : S) → ⟨ fst x ∈ Vv ⟩
            → ∥ Σ[ c ∈ S ] Σ[ p ∈ S ] Σ[ y ∈ S ]
                (⟨ fst c ∈ Cv ⟩ × ((fst c ≡ pr (# 1) (fst p)) × (⟨ pr (fst c) (fst y) ∈ Tv ⟩ × Cuts (fst x) Wv (fst y)))) ∥₁)
         → ⟨ γ ⊨ memAt v w T C N ⟩
  mem-in g x x∈ = PT.map
```

反过来，设候选输出的每个成员都带有这样一个截断的语义记录。等式 `c = pr (# 1) p` 给出有界公式所需的元数一形状，而 `pr(c,y)` 属于表的证明为表条目提供一个有界表示。

```agda
    (λ { (c , p , y , (c∈ , (ec , (e∈ , cuts)))) →
      let ec' : fst c ≡ pr N1v (fst p)
          ec' = ec ∙ cong (λ a → pr a (fst p)) (sym (tg f1))
          δ4 = p ∷ container c (lookup (N f1) γ) p ec' .fst ∷ c ∷ x ∷ γ
          eS = down (lookup T γ) (pr (fst c) (fst y)) e∈
```

随后组装七槽环境，并由 `definesB-in` 把切割关系转换回可定义子集子句。

```agda
          δ7 = y ∷ container eS c y refl .fst ∷ eS ∷ δ4
      in c , ( c∈ , fillSnd i0 (c ∷ x ∷ γ) (lookup (N f1) γ) p ec'
                 (∃̇∈ (var (sh 4 T)) (sndEx i0 i3 (definesB i6 (sh 7 w) i0 (sh 7 (N f0)))))
                 ∣ eS , ( e∈ , fillSnd i0 (eS ∷ δ4) c y refl (definesB i6 (sh 7 w) i0 (sh 7 (N f0)))
                              (definesB-in i6 (sh 7 w) i0 (sh 7 (N f0)) δ7 (tg f0) cuts) i3 refl ) ∣₁
```

键的形状、表条目与切出条件编码完毕后，外层有界量词把这个截断整体用于候选输出的原成员。因此，这个语义记录足以重建整个隶属子句的满足。

```agda
                 (sh 2 (N f1)) refl ) })
    (g x x∈)
```

读取覆盖子句：取一个可拆成「标签一与 `p` 之对」的码 `c`，则仅仅地给出 `c` 处的表值 `y` 以及被 `y` 切出的集合 `x`。

```agda
  all-out : ⟨ γ ⊨ allAt v w T C N ⟩ → (c p : S) → ⟨ fst c ∈ Cv ⟩ → fst c ≡ pr (# 1) (fst p)
          → ∥ Σ[ y ∈ S ] Σ[ x ∈ S ] (⟨ pr (fst c) (fst y) ∈ Tv ⟩ × (⟨ fst x ∈ Vv ⟩ × Cuts (fst x) Wv (fst y))) ∥₁
  all-out h c p c∈ ec = PT.rec squash₁
    (λ { (e , (e∈ , hy)) → PT.rec squash₁
      (λ { (y , s' , (ee , hx)) → PT.map
```

证明消去表条目与三槽存在量化，而可定义子句读取产出成员与表值之间的切割关系。

```agda
        (λ { (x , (x∈ , hd)) →
          y , x , ( subst (λ u → ⟨ u ∈ Tv ⟩) ee e∈
                  , ( x∈ , definesB-out i0 (sh 7 w) i1 (sh 7 (N f0)) (x ∷ y ∷ s' ∷ e ∷ δ3) (tg f0) hd ) ) })
        hx })
      (sndEx-out i0 i3 (∃̇∈ (var (sh 6 v)) (definesB i0 (sh 7 w) i1 (sh 7 (N f0)))) (e ∷ δ3) hy) })
```

为作反向构造，固定码域的成员 `c`，并考察它作为 `pr (# 1) p` 的任一呈现。语义覆盖假设随后在命题截断下给出一个表取值及由该取值切出的子集；这些见证填入该呈现所需的有界结论。

```agda
    (useSnd i0 (c ∷ γ) (lookup (N f1) γ) p ec'
      (∃̇∈ (var (sh 3 T)) (sndEx i0 i3 (∃̇∈ (var (sh 6 v)) (definesB i0 (sh 7 w) i1 (sh 7 (N f0))))))
      (sh 1 (N f1)) refl (h c c∈))
    where
    ec' : fst c ≡ pr N1v (fst p)
```

借助 `Tags`，使用形式标签的等式被转换为所需的元数一等式。辅助容器只负责让分量与码始终处于有界量词内；它们不会给语义见证增加任何选择或唯一性。

```agda
    ec' = ec ∙ cong (λ a → pr a (fst p)) (sym (tg f1))
    δ3 : S ^ (3 + m)
    δ3 = p ∷ container c (lookup (N f1) γ) p ec' .fst ∷ c ∷ γ
```

因此，填充覆盖子句时遍历候选码域中每个被呈现为元数一键形状的成员。对每个这样的呈现，语义假设在命题截断下给出表取值、候选输出中由它切出的成员及二者的隶属。直到后文加入 `satAt`，这里都不声称这些成员是真正的公式键。

```agda
  all-in : ((c p : S) → ⟨ fst c ∈ Cv ⟩ → fst c ≡ pr (# 1) (fst p)
            → ∥ Σ[ y ∈ S ] Σ[ x ∈ S ] (⟨ pr (fst c) (fst y) ∈ Tv ⟩ × (⟨ fst x ∈ Vv ⟩ × Cuts (fst x) Wv (fst y))) ∥₁)
         → ⟨ γ ⊨ allAt v w T C N ⟩
  all-in g c c∈ = sndAll-in' (λ p s s∈ p∈ ec →
    PT.map (λ { (y , x , (e∈ , (x∈ , cuts))) →
```

最内层的有界存在量词现在以切出的集合 `x` 为见证，并同时接收 `x` 属于取值集合的证明以及刚由 `definesB` 编码的 `Cuts` 证据。这便完成反向翻译：表条目及其所切子集的语义见证给出隶属子句的满足，而所有存在数据仍保留在命题截断中。

```agda
      let eS = down (lookup T γ) (pr (fst c) (fst y)) e∈
          δ6 = y ∷ container eS c y refl .fst ∷ eS ∷ p ∷ s ∷ c ∷ γ
      in eS , ( e∈ , fillSnd i0 (eS ∷ p ∷ s ∷ c ∷ γ) c y refl (∃̇∈ (var (sh 6 v)) (definesB i0 (sh 7 w) i1 (sh 7 (N f0))))
                       ∣ x , (x∈ , definesB-in i0 (sh 7 w) i1 (sh 7 (N f0)) (x ∷ δ6) (tg f0) cuts) ∣₁ i3 refl ) })
      (g c p c∈ (ec ∙ cong (λ a → pr a (fst p)) (tg f1))))
```

覆盖子句含有同样两层存在选择：满足关系表的一个取值，以及该取值从工作集中切出的子集。为二者合成后的向外读法命名，使下一个论证能把这对仅仅存在的见证作为一个命题值整体处理。

```agda
    where
    sndAll-in' = sndAll-in i0 (sh 1 (N f1))
      (∃̇∈ (var (sh 3 T)) (sndEx i0 i3 (∃̇∈ (var (sh 6 v)) (definesB i0 (sh 7 w) i1 (sh 7 (N f0)))))) (c ∷ γ)
```

## 有界描述的正确性

现在可以把有界描述与真正的可定义性算子比较。这个比较不只需要 `defAt` 成立：数码标签必须取预期值，工作集槽必须指称 `W`，而 `satAt` 必须保证码集与满足关系表具有其真正的满足语义。

```agda
module DefRead {m : ℕ} (v w T C E : Fin m) (N : Fin 10 → Fin m) (γ : S ^ m) (W : S)
  (qw : fst (lookup w γ) ≡ fst W) (tg : Tags γ N) (hs : ⟨ γ ⊨ satAt T w C E N ⟩) where
  open Alphabet W
  open Match W
  private
```

前面的两个读取器提供所需桥梁。`SatRead` 把描述中的码域和表与 `W` 上真正的码及满足取值对齐；`Read` 把 `defAt` 读成两个语义切出条件。随后 `DefOf (fst W)` 把每条解码得到的元数一公式解释为 `W` 的一个子集。

```agda
    module SR = SatRead T w C E N γ W qw tg hs
    module RD = Read v w T C N γ tg
    module DA = DefOf (fst W)
    Vv = fst (lookup v γ)
    Wv = fst (lookup w γ)
```

记表槽与码槽所指称的底层集合为 `Tv` 与 `Cv`。`satAt` 的作用正在于：如今可以在这些描述集合中的隶属与真正满足关系表、码域中的隶属之间来回转换。

```agda
    Tv = fst (lookup T γ)
    Cv = fst (lookup C γ)
```

映射 `toS` 把字母表上公式的每个常元改名为 `S` 的相应常元，产出可由环境满足判断的公式。

```agda
    toS : Formula Ab 1 → Formula S 1
    toS = mapFo (asConst W)
```

表取值引理说：在公式键处记录的取值等于改名后公式的显式满足集合。证明复合表的外向投影与一致满足的取值认同。

```agda
    valOf : (ψ : Formula Ab 1) (c y : S) → fst c ≡ fst (keyS W ψ) → ⟨ pr (fst c) (fst y) ∈ Tv ⟩
          → fst y ≡ fst (Sat W (toS ψ))
    valOf ψ c y qc h = SR.T-out c y h .snd ∙ cong fst (val-at W W ψ c (SR.T-out c y h .fst) qc)
```

核心桥梁逐条处理公式。若 `Cuts` 说明 `x` 恰由 `W` 中那些其单变元环境属于 `ψ` 的满足集合的元素组成，那么 `x` 就等于这个特定的可定义子集 `DA.defSet ψ`。外延性通过两个隶属方向证明此等式。

```agda
    cut≡ : (ψ : Formula Ab 1) (x : S) → Cuts (fst x) Wv (fst (Sat W (toS ψ))) → DA.defSet ψ ≡ fst x
    cut≡ ψ x (o , i) = extensionalV (λ z → ⇔toPath (fwd z) (bwd z))
      where
      fwd : (z : V ℓ) → ⟨ z ∈ DA.defSet ψ ⟩ → ⟨ z ∈ fst x ⟩
      fwd z = PT.rec (snd (z ∈ fst x))
```

第一个方向中，属于 `DA.defSet ψ` 的证明在命题截断下给出 `W` 中元素的一个表示。满足桥梁把该表示的单变元环境放入 `ψ` 的满足集合，于是 `Cuts` 的向内一半把所表示的集合放入 `x`。

```agda
        (λ { ((q , hq) , e) →
          i (down W z (subst (λ u → ⟨ u ∈ fst W ⟩) e (ι∈ q)))
            (subst (λ u → ⟨ z ∈ u ⟩) (sym qw) (subst (λ u → ⟨ u ∈ fst W ⟩) e (ι∈ q)))
            (subst (λ u → ⟨ envOne u ∈ fst (Sat W (toS ψ)) ⟩) e
              (subst ⟨_⟩ (defSet-Sat W ψ q) ∣ (q , hq) , refl ∣₁)) })
```

另一个方向从 `z ∈ x` 出发。`Cuts` 的向外一半同时给出 `z ∈ W` 以及其单变元环境属于满足集合。`∈-asFiber` 把第一项转换为 `W` 的呈现中的一个实际索引，并给出回到 `z` 的路径。

```agda
      bwd : (z : V ℓ) → ⟨ z ∈ fst x ⟩ → ⟨ z ∈ DA.defSet ψ ⟩
      bwd z hz =
        let zS = down x z hz
            zW = subst (λ u → ⟨ z ∈ u ⟩) qw (o zS hz .fst)
            fib = ∈-asFiber {a = z} {b = fst W} zW
```

沿该呈现路径运输环境隶属，再反向应用 `defSet-Sat`，便证明对应表示属于 `DA.defSet ψ`；沿同一路径运回后得到 `z ∈ DA.defSet ψ`，从而完成外延等式。

```agda
        in subst (λ u → ⟨ u ∈ DA.defSet ψ ⟩) (fib .snd)
             (subst ⟨_⟩ (sym (defSet-Sat W ψ (fib .fst)))
               (subst (λ u → ⟨ envOne u ∈ fst (Sat W (toS ψ)) ⟩) (sym (fib .snd)) (o zS hz .snd)))
```

反过来，设已知 `DA.defSet ψ` 等于 `x`。为重建 `Cuts`，先取 `x` 的一个成员，把它改写为 `DA.defSet ψ` 的成员，再展开可定义子集的隶属。由此同时得到它作为 `W` 中元素的表示，以及相应单变元环境属于满足集合的证明。

```agda
    cuts-of : (ψ : Formula Ab 1) (x : S) → DA.defSet ψ ≡ fst x → Cuts (fst x) Wv (fst (Sat W (toS ψ)))
    cuts-of ψ x e = o , i
      where
      o : (z : S) → ⟨ fst z ∈ fst x ⟩ → ⟨ fst z ∈ Wv ⟩ × ⟨ envOne (fst z) ∈ fst (Sat W (toS ψ)) ⟩
      o z hz = PT.rec (isProp× (snd (fst z ∈ Wv)) (snd (envOne (fst z) ∈ fst (Sat W (toS ψ)))))
```

展开这一隶属，得到 `W` 中的一个表示，并经 `defSet-Sat` 得到其单变元环境属于所需满足集合。表示与原成员之间的等式把这两个结论都运输回 `x` 的该成员。

```agda
        (λ { ((q , hq) , eq) →
            subst (λ u → ⟨ fst z ∈ u ⟩) (sym qw) (subst (λ u → ⟨ u ∈ fst W ⟩) eq (ι∈ q))
          , subst (λ u → ⟨ envOne u ∈ fst (Sat W (toS ψ)) ⟩) eq (subst ⟨_⟩ (defSet-Sat W ψ q) ∣ (q , hq) , refl ∣₁) })
        (subst (λ u → ⟨ fst z ∈ u ⟩) (sym e) hz)
      i : (z : S) → ⟨ fst z ∈ Wv ⟩ → ⟨ envOne (fst z) ∈ fst (Sat W (toS ψ)) ⟩ → ⟨ fst z ∈ fst x ⟩
```

为证明 `Cuts` 的向内一半，从 `W` 中一个已呈现的成员出发，并假定其单变元环境满足 `ψ`。满足桥梁把它转成属于 `DA.defSet ψ`，再由假定的等式 `DA.defSet ψ = fst x` 把该成员放入 `x`。

```agda
      i z hw he =
        let fib = ∈-asFiber {a = fst z} {b = fst W} (subst (λ u → ⟨ fst z ∈ u ⟩) qw hw)
        in subst (λ u → ⟨ fst z ∈ u ⟩) e
             (subst (λ u → ⟨ u ∈ DA.defSet ψ ⟩) (fib .snd)
               (subst ⟨_⟩ (sym (defSet-Sat W ψ (fib .fst)))
```

最后的运输只是在所选成员表示与其底层集合之间作对齐。因此，`cut≡` 与 `cuts-of` 合起来把 `ψ` 的 `Cuts` 谓词同「等于单个可定义子集 `DA.defSet ψ`」对应起来；两个方向都没有断言定义公式唯一。

```agda
                 (subst (λ u → ⟨ envOne u ∈ fst (Sat W (toS ψ)) ⟩) (sym (fib .snd)) he)))
```

现在可以准确陈述可靠性。在工作集槽与 `W` 已对齐、数码标签正确且 `satAt` 已校准码集和满足关系表的背景下，`defAt` 的满足迫使取值槽恰等于 `𝒟ₒ (fst W)`。这里的 `𝒟ₒ` 收集由允许取 `W` 中参数的一阶公式定义出的 `W` 的子集，并非完整的内部幂集。

```agda
  def-sound : ⟨ γ ⊨ defAt v w T C N ⟩ → Vv ≡ 𝒟ₒ (fst W)
  def-sound hd = extensionalV (λ x → ⇔toPath (fwd x) (bwd x))
    where
    hm = defAt-out v w T C N γ hd .fst
    ha = defAt-out v w T C N γ hd .snd
```

对正向包含，隶属子句在命题截断下给出一个具有键形状的码、一个满足关系表条目，以及描述该条目所切子集的条件。`satAt` 把候选码域同真正码域对齐后，`decodeAll` 仅仅给出一条元数一公式，其编码具有所需的第二分量。表取值引理再把该条目的取值认同为这条公式的满足集合。

```agda
    fwd : (x : V ℓ) → ⟨ x ∈ Vv ⟩ → ⟨ x ∈ 𝒟ₒ (fst W) ⟩
    fwd x hx = PT.rec (snd (x ∈ 𝒟ₒ (fst W)))
      (λ { (c , p , y , (c∈ , (ec , (e∈ , cuts)))) → PT.rec (snd (x ∈ 𝒟ₒ (fst W)))
        (λ { (ψ , qp) →
          𝒟ₒ-intro (fst W) x ∣ ψ , cut≡ ψ xS
```

`Cuts` 事实沿表取值认同被运至解码公式的满足集，而可定义幂集引入把切片集合放进 `𝒟ₒ`。截断的公式解码被消耗到命题值的引入中。

```agda
            (subst (λ u → Cuts x Wv u) (valOf ψ c y (ec ∙ cong (pr (# 1)) qp) e∈) cuts) ∣₁ })
        (decodeAll c (SR.C-out c c∈) 1 (fst p) ec) })
      (RD.mem-out hm xS hx)
      where
      xS : S
```

取值槽被呈现为载体元素，以供隶属子句向外方向读取。

```agda
      xS = down (lookup v γ) x hx
```

对反向包含，属于 `𝒟ₒ (fst W)` 只给出命题截断下的一条公式 `ψ` 及等式 `DA.defSet ψ = x`。在消去到隶属命题的过程中，`defAt` 的覆盖部分针对由这个临时见证 `ψ` 构造的键，给出一个表取值以及取值槽中的集合 `x'`。

```agda
    bwd : (x : V ℓ) → ⟨ x ∈ 𝒟ₒ (fst W) ⟩ → ⟨ x ∈ Vv ⟩
    bwd x hx = PT.rec (snd (x ∈ Vv))
      (λ { (ψ , e) → PT.rec (snd (x ∈ Vv))
        (λ { (y , x' , (e∈ , (x'∈ , cuts))) →
          subst (λ u → ⟨ u ∈ Vv ⟩)
```

切片等式沿表取值认同运输以恢复切片集的底层集合，运输把它放进取值槽。

```agda
            (sym (cut≡ ψ x' (subst (λ u → Cuts (fst x') Wv u) (valOf ψ (keyS W ψ) y refl e∈) cuts)) ∙ e)
            x'∈ })
        (RD.all-out ha (keyS W ψ) (sndS (keyS W ψ) (# 1) (cd ψ) refl) (SR.C-in (keyS W ψ) (key∈AllCodes W ψ)) refl) })
      (𝒟ₒ-inv (fst W) x hx)
```

完备性把同一等价关系反向使用。在仍假定工作集已对齐、标签正确且 `satAt` 成立时，取值槽与 `𝒟ₒ (fst W)` 的相等足以构造 `defAt` 的满足。两个合取项分别说明：列出的每个集合都有定义公式，而每条元数一公式所定义的子集都会出现。

```agda
  def-complete : Vv ≡ 𝒟ₒ (fst W) → ⟨ γ ⊨ defAt v w T C N ⟩
  def-complete qv = defAt-in v w T C N γ mem all
    where
```

每条公式的表条目从已定义的递归表中选取，后者同时保证表中的隶属与显式满足集的认同。

```agda
    entry : (ψ : Formula Ab 1) → Σ[ y ∈ S ] (⟨ pr (fst (keyS W ψ)) (fst y) ∈ Tv ⟩ × (fst y ≡ fst (Sat W (toS ψ))))
    entry ψ = Table.val W W (keyS W ψ) (key∈AllCodes W ψ)
            , ( SR.T-in (keyS W ψ) (key∈AllCodes W ψ)
              , cong fst (val-at W W ψ (keyS W ψ) (key∈AllCodes W ψ) refl) )
```

对隶属合取项，先把取值槽的成员运输到 `𝒟ₒ (fst W)`，再由 `𝒟ₒ-inv` 展开。定义公式只在命题截断下存在。在该截断内部，证明组装它的公式键、相应表条目和所需的 `Cuts` 证据；整个过程没有全局选取定义公式，也没有把某条公式保留为规范数据。

```agda
    mem : ⟨ γ ⊨ memAt v w T C N ⟩
    mem = RD.mem-in (λ x x∈ → PT.map
      (λ { (ψ , e) →
        keyS W ψ , sndS (keyS W ψ) (# 1) (cd ψ) refl , entry ψ .fst
        , ( SR.C-in (keyS W ψ) (key∈AllCodes W ψ)
```

所用表取值是递归满足关系表已为该公式键确定的取值。沿它与显式满足集合的等式运输 `cuts-of`，便得到切出证据。这个临时公式见证始终留在 `PT.map` 内，因此所得隶属见证仍受命题截断。

```agda
          , ( refl
            , ( entry ψ .snd .fst
              , subst (λ u → Cuts (fst x) Wv u) (sym (entry ψ .snd .snd)) (cuts-of ψ x e) ) ) ) })
      (𝒟ₒ-inv (fst W) (fst x) (subst (λ u → ⟨ fst x ∈ u ⟩) qv x∈)))
```

覆盖合取项对码域中每个元数一的键证明，对分解被显式名指。

```agda
    all : ⟨ γ ⊨ allAt v w T C N ⟩
    all = RD.all-in (λ c p c∈ ec → PT.map
      (λ { (ψ , qp) →
        let qc : fst c ≡ fst (keyS W ψ)
            qc = ec ∙ cong (pr (# 1)) qp
```

对给定的元数一键，解码仅仅给出一条公式 `ψ`，其编码是该键的第二分量。由引入规则，可定义子集 `DA.defSet ψ` 属于 `𝒟ₒ (fst W)`；再沿假定的等式运输，便得到它属于取值槽。解码并未选出唯一或规范的公式。

```agda
            xS : S
            xS = down (lookup v γ) (DA.defSet ψ)
                   (subst (λ u → ⟨ DA.defSet ψ ∈ u ⟩) (sym qv) (𝒟ₒ-intro (fst W) (DA.defSet ψ) ∣ ψ , refl ∣₁))
        in entry ψ .fst , xS
         , ( subst (λ u → ⟨ pr u (fst (entry ψ .fst)) ∈ Tv ⟩) (sym qc) (entry ψ .snd .fst)
```

满足关系表给出解码公式键所对应的取值，而 `cuts-of` 证明该取值从工作集中切出的恰是 `DA.defSet ψ`。连同刚得到的隶属，这些数据满足覆盖子句。由于 `decodeAll` 的结果受命题截断，且只被消去到这个命题值子句中，构造只记录存在性，并不保留解码所得的公式。

```agda
           , ( subst (λ u → ⟨ DA.defSet ψ ∈ u ⟩) (sym qv) (𝒟ₒ-intro (fst W) (DA.defSet ψ) ∣ ψ , refl ∣₁)
             , subst (λ u → Cuts (DA.defSet ψ) Wv u) (sym (entry ψ .snd .snd)) (cuts-of ψ xS refl) ) ) })
      (decodeAll c (SR.C-out c c∈) 1 (fst p) ec))
```

导出的可靠性方向给出后文实际使用的精确接口：一旦工作集槽指称 `W`、`Tags` 固定数码槽且 `satAt` 校准码与满足数据，`defAt` 就推出与 `𝒟ₒ (fst W)` 相等。因此，这条有界公式只有在这一已校准背景中才具有预期语义。

```agda
def-sound : ∀ {m} (v w T C E : Fin m) (N : Fin 10 → Fin m) (γ : S ^ m) (W : S)
          → fst (lookup w γ) ≡ fst W → Tags γ N → ⟨ γ ⊨ satAt T w C E N ⟩
          → ⟨ γ ⊨ defAt v w T C N ⟩ → fst (lookup v γ) ≡ 𝒟ₒ (fst W)
def-sound v w T C E N γ W qw tg hs = DefRead.def-sound v w T C E N γ W qw tg hs
```

导出的完备性方向具有相同前提，并反转上述蕴含：与 `𝒟ₒ (fst W)` 的相等可重建 `defAt` 的满足。两条定理合起来刻画可定义子集的集合，既不为每个成员选取代表公式，也不把它等同于完整的内部幂集。

```agda
def-complete : ∀ {m} (v w T C E : Fin m) (N : Fin 10 → Fin m) (γ : S ^ m) (W : S)
             → fst (lookup w γ) ≡ fst W → Tags γ N → ⟨ γ ⊨ satAt T w C E N ⟩
             → fst (lookup v γ) ≡ 𝒟ₒ (fst W) → ⟨ γ ⊨ defAt v w T C N ⟩
def-complete v w T C E N γ W qw tg hs = DefRead.def-complete v w T C E N γ W qw tg hs
```