---
title: "集合的可定义子集"
module: L.Definability
lang: zh
site: "Bedrock"
description: "集合的可定义子集"
stage: "可构造层与公理"
reading_order: 24
canonical: https://bedrock.institute/zh/L.Definability.html
html: L.Definability.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/Definability.lagda.md
prerequisites: [Base.Prelude, FOL.ZFStructure, FOL.Syntax, FOL.LevyHierarchy, FOL.Manipulation.ConstantMapping, FOL.Manipulation.Relabelling, FOL.Absoluteness, V.Hierarchy, V.Smallness]
routes: [constructible-axioms]
translations: [https://bedrock.institute/en/L.Definability.md, https://bedrock.institute/ja/L.Definability.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
# 集合的可定义子集

对集合 `A`，算子 `Def A` 恰好收集由 `A` 上限制结构中的一阶公式，并使用 `A` 中有限多个参数所定义的 `A` 的子集。其隶属定理给出后续可构造性论证所需的公式、环境与满足关系。

本章依赖两个设计点。公式以 `A` 的小成员类型 `⟪ A ⟫` 为常元域，因此类型本身保证参数来自 `A`。满足采用限制结构 `𝒮ᵥ ↾ (∈ A)` 上的**内层**语义，量词的范围只包括 `A` 的成员。这正是教科书中「在 `(A, ∈)` **中**可定义」的含义，也使前几章的本质小性在此适用：任何公式的求值都是小类型，因此 `Def A` 是集合，降层无需额外代价。

本章的问题是：对一个集合 `A`，哪些子集能被一阶公式在 `(A, ∈)` 内部解释时挑选出来？答案将被收集进一个算子 `Def A`，它本身是外围层级中的一个集合。一切都在一个固定的宇宙层级 ℓ 上进行，使 `Def A` 足够小，能与 `A` 在同一层级上作为集合存在。

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

open import Base.Prelude

module L.Definability {ℓ : Level} where

open import FOL.ZFStructure using ( ZFStructure; Transitive )
```

公式来自归纳的对象语言：`Formula K n` 的常元由类型 `K` 索引，`n` 个槽位索引自由变量，原子公式由结构的隶属与相等关系构成。取 `K = ⟪ A ⟫`，即 `A` 的小成员类型，「参数来自 `A`」便由构造自动成立：每个常元指称 `A` 的一个成员。有界片段 `Δ₀` 稍后比较满足的内层与外层读法时才会用到；常元映射与改名则是把公式在常元域之间移动并沿此移动搬运满足关系的操作。

```agda
open import FOL.Syntax using ( Formula; var; con; _∈̇_; ⊤̇ )
open import FOL.LevyHierarchy using ( Δ₀ )
open import FOL.Manipulation.ConstantMapping using ( mapFo )
open import FOL.Manipulation.Relabelling using ( mapΔ₀; ⊨-map )
import FOL.Absoluteness
```

「在 `(A, ∈)` **中**可定义」意味着量词只能在 `A` 的成员上取值。因此满足关系必须取在限制到类 `x ↦ x ∈ˢ A` 的结构上，而不是外围层级上。本章在层级 ℓ 上的外围结构 `𝒮ᵥ` 中工作，其载体为 `S`、隶属为 `∈ₛ`；向 `A` 的限制以及限制世界的小性来自小性章：给定一个类、一个与限制载体等价的小类型、以及常元解释，它重建限制结构并证明其中每个公式都求值为小命题。本章的限制类就是「属于 `A`」。

```agda
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ )
open import V.Smallness {ℓ} using ( module InnerSmall )

open import Cubical.Foundations.Equiv
  using ( _≃_; equivFun; invEq; invEquiv; compEquiv; propBiimpl→Equiv )
open import Cubical.Functions.Embedding using ( isEmbedding→Inj )
```

本质小性正是让满足关系能够为集合充当索引的关键。既然每个公式在 `(A, ∈)` 内都求值为**小**命题，满足公式的 `A` 的成员便可由一个小类型索引，而层级构造子 `sett` 把小索引类型和索引映射变成一个集合。一个公式定义出的子集与 `Def` 本身都将以这种方式构造。`sett` 的隶属于是只是截断的存在性陈述，而以命题为目标时截断只能消入命题，不会给出被选取的见证。这些构造的形状产生了本章基于路径的规格。

```agda
open import Cubical.Data.Sigma using ( Σ-cong-equiv-snd )
open import Cubical.Functions.Logic using ( ⇔toPath )
import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∣_∣₁ )
open import Cubical.HITs.CumulativeHierarchy.Base using ( sett )
```

最后是真值的词汇。联结词与量词直接作用于 `hProp (ℓ-suc ℓ)` 中的命题，因此满足关系取值于 `hProp (ℓ-suc ℓ)`，其中 `⟨ p ⟩` 取出 `hProp` 的底层命题。这类命题的相等是路径，因此关于隶属的规格将陈述为命题之间的路径，并用路径链来证明。就位之后，下一节固定一个集合 `A` 并定义其可定义子集。

```agda
open import Cubical.HITs.CumulativeHierarchy.Properties
  using ( _∈ₛ_; ∈∈ₛ; ⟪_⟫; ⟪_⟫↪; ∈ₛ⟪_⟫↪_; ∈-asFiber; presentation
        ; isEmb⟪_⟫↪; _⊆_; extensionality )

open ZFStructure 𝒮ᵥ
```

## 算子

以下一切都相对于一个集合 `A`，故本节在模块 `DefOf A` 中工作。限制类取「属于 `A`」，而本质小见证 `e` 就是库的 `presentation`：小成员类型 `⟪ A ⟫` 与限制载体等价 (小成员关系逐点换成大的即可)。常元解释 `ι` 把常元，即 `⟪ A ⟫` 的索引，送到限制载体的对应成员；其第一分量按定义就是该成员本身。

类 `M` 给每个集合 `x` 指派命题 `x ∈ˢ A`，因此限制载体 `Σ[ x ∈ S ] (x ∈ᶜ M)` 逐元素地就是 `A` 的一个成员连同「它是成员」的证明。等价 `e` 把这个载体表现为本质小。它的第一个因子是 `presentation A` 的逆，把仅仅落在索引映射纤维中的 `A` 的成员等同于 `⟪ A ⟫` 中的索引；第二个因子对每个 `v` 把小隶属陈述 `v ∈ₛ A` 双向换成大隶属陈述 `v ∈ˢ A`。由于这些是命题，逐点转换是合法的。

```agda
module DefOf (A : S) where

  M : S → hProp (ℓ-suc ℓ)
  M x = x ∈ˢ A

  e : ⟪ A ⟫ ≃ (Σ[ x ∈ S ] (x ∈ᶜ M))
  e = compEquiv (invEquiv (presentation A))
```

于是常元解释 `ι` 就是把等价 `e` 当作函数来读。由于公式的常元域将取 `⟪ A ⟫` 本身，语言中的一个常元就是 `A` 的某个成员的索引，`ι` 把它解码到限制载体中。`ι m` 的第一投影按定义就是底层集合 `⟪ A ⟫↪ m`，隶属证明会不加修饰地使用这一事实。

```agda
        (Σ-cong-equiv-snd (λ v →
          propBiimpl→Equiv (snd (v ∈ₛ A)) (snd (v ∈ˢ A))
            (∈∈ₛ {a = v} {b = A} .snd) (∈∈ₛ {a = v} {b = A} .fst)))

  ι : ⟪ A ⟫ → Σ[ x ∈ S ] (x ∈ᶜ M)
  ι = equivFun e
```

在这些数据上开启 `InnerSmall` 便重建了世界：限制到「属于 `A`」的结构 `𝒮M`、其满足关系 `⊨ᵐ`，以及定理 `⊨ᵐ-small`，即 `⟪ A ⟫` 上的每个公式都求值为小命题。以 public 开启意味着后续章节恰在这些名字下读取内层满足。从这里起，「满足」一律指这个内层关系，量词只限于 `A` 的成员。

```agda
  open InnerSmall M ⟪ A ⟫ e {K = ⟪ A ⟫} ι public
```

内层满足 `⊨ᵐ` 与其小性就位后，算子可直接定义。`smallSat φ m` 是 `φ` 在成员 `m` 处的真值，位于低一层宇宙；`defSet φ` 是 `φ` 从 `A` 中定出的子集，在 `φ` 选中的成员上应用 `sett`；`Def A` 则是这些子集的全体，以公式自身为索引。公式是 `Type ℓ` 中的归纳数据，恰好构成合法的小索引；这里使用的正是**语法当索引集**。

压缩 `smallSat` 打包了两步求值：`⊨ᵐ-small φ (ι m ∷ [])` 是一个对子，第一分量是与内层满足陈述等价的小命题，第二分量是那个等价本身。环境 `ι m ∷ []` 只有一项，因为 `φ` 只有一个自由变量槽位，由成员 `m` 经 `ι` 填入。与此独立地，`φ` 中出现的任何常元都经常元解释 `ι` 解释，因此可以指称 `A` 的任意成员：参数经由常元进入，而变量那一项只是固定单个自由槽位的求值位置。底层命题 `⟨ smallSat φ m ⟩` 表示 `φ` 在 `(A, ∈)` 内于 `m` 处成立，且已是适合为 `sett` 充当索引的小形式。

```agda
  smallSat : Formula ⟪ A ⟫ 1 → ⟪ A ⟫ → hProp ℓ
  smallSat φ m = ⊨ᵐ-small φ (ι m ∷ []) .fst

  defSet : Formula ⟪ A ⟫ 1 → S
  defSet φ = sett (Σ[ m ∈ ⟪ A ⟫ ] ⟨ smallSat φ m ⟩) (λ p → ⟪ A ⟫↪ (p .fst))

  Def : S
```

可定义子集 `defSet φ` 由索引类型 `Σ[ m ∈ ⟪ A ⟫ ] ⟨ smallSat φ m ⟩` 呈现：一个索引是成员 `m` 连同「`φ` 在 `m` 处成立」的证明，索引映射把这个对子送到集合 `⟪ A ⟫↪ m`。注意截断纪律：证明分量是证明而非被选取的数据，`defSet φ` 的成员只要求这样的证明**仅仅**存在。最后，`Def` 在上一层重复同一构造，以公式本身为索引族：每个索引仅仅命中某个 `defSet φ`。由于公式住在 `Type ℓ` 中，索引类型是小的，结果仍是层级中的集合。

```agda
  Def = sett (Formula ⟪ A ⟫ 1) defSet
```

## 隶属，给出规格

`Def` 与每个 `defSet φ` 都由 `sett` 构造，因此其隶属关系**按定义**表示相应索引的仅仅存在性。对 `Def` 无须另作证明：`Def` 的成员仅仅就是某个 `defSet φ`。可定义子集有两条规格：它的成员都属于 `A`；成员 `⟪ A ⟫↪ m` 属于 `defSet φ`，**当且仅当内层世界在 `m` 处满足 `φ`**。这两条规格直接给出「可定义子集」的含义；`smallSat` 的压缩只是编码，并不改变这个等价关系。

第一条规格说每个 `defSet φ` 都包含于 `A`。`defSet φ` 的成员仅仅来自带某个证明的索引 `(m , _)`，连同把索引集合等同于 `y` 的路径 `q`。由于 `A` 中的隶属是命题，截断可消入命题：该证明沿 `q` 把已知事实 `⟪ A ⟫↪ m ∈ˢ A` 搬运过去，得到 `y ∈ˢ A`。这个已知事实正是小隶属 `⟪ A ⟫↪ m ∈ₛ A` 经 `∈∈ₛ` 转换而来。

```agda
  defSet⊆A : (φ : Formula ⟪ A ⟫ 1) (y : S) → ⟨ y ∈ˢ defSet φ ⟩ → ⟨ y ∈ˢ A ⟩
  defSet⊆A φ y = PT.rec (snd (y ∈ˢ A)) λ { ((m , _) , q) →
    subst (λ v → ⟨ v ∈ˢ A ⟩) q
          (∈∈ₛ {a = ⟪ A ⟫↪ m} {b = A} .snd (∈ₛ⟪ A ⟫↪ m)) }

  private
```

第二条规格是本章的核心，它被陈述为命题之间的路径，而不是一对蕴含：`⟪ A ⟫↪ m` 属于 `defSet φ` 这一命题等于内层满足陈述 `(ι m ∷ []) ⊨ᵐ φ`。辅助定义 `decode` 把 `smallSat` 重新展开成完整的对子，于是其第二分量中的等价对两个方向都可用。另请注意私有的单射性引理：`⟪ A ⟫↪` 是从 `⟪ A ⟫` 到载体的嵌入，其值之间的路径来自索引之间的路径；这将从集合的路径恢复出 `m' ≡ m`。

```agda
    ⟪⟫↪-inj : {m' m : ⟪ A ⟫} → ⟪ A ⟫↪ m' ≡ ⟪ A ⟫↪ m → m' ≡ m
    ⟪⟫↪-inj {m'} {m} = isEmbedding→Inj isEmb⟪ A ⟫↪ m' m

  defSet-mem : (φ : Formula ⟪ A ⟫ 1) (m : ⟪ A ⟫)
             → (⟪ A ⟫↪ m ∈ˢ defSet φ) ≡ ((ι m ∷ []) ⊨ᵐ φ)
  defSet-mem φ m = ⇔toPath fwd bwd
```

正向展开隶属仅仅给出的内容：索引 `(m' , h)`，其中 `h` 证明 `smallSat φ m'`，以及满足 `⟪ A ⟫↪ m' ≡ ⟪ A ⟫↪ m` 的路径 `q`。单射性把 `q` 变成 `m' ≡ m`，沿它搬运 `h` 得到 `smallSat φ m` 的证明。然后 `decode` 的第二分量，即小命题与内层满足之间的等价，把这个证明转换为目标陈述。每个部件都派上用场：截断给出索引，嵌入给出索引间的路径，移送搬运证明，等价将其解码。

```agda
    where
    decode = ⊨ᵐ-small φ (ι m ∷ [])
    fwd : ⟨ ⟪ A ⟫↪ m ∈ˢ defSet φ ⟩ → ⟨ (ι m ∷ []) ⊨ᵐ φ ⟩
    fwd = PT.rec (snd ((ι m ∷ []) ⊨ᵐ φ)) λ { ((m' , h) , q) →
      invEq (decode .snd) (subst (λ k → ⟨ smallSat φ k ⟩) (⟪⟫↪-inj q) h) }
```

反向很短，因为等价同样可以反向运行：给定 `hφ : (ι m ∷ []) ⊨ᵐ φ`，应用该等价得到 `smallSat φ m` 的证明，取索引 `(m , 证明)` 与平凡路径 `refl`。结果用 `∣_∣₁` 截断，这正是隶属所要求的。两个方向合起来给出内层满足与可定义子集隶属之间的精确对应。

```agda
    bwd : ⟨ (ι m ∷ []) ⊨ᵐ φ ⟩ → ⟨ ⟪ A ⟫↪ m ∈ˢ defSet φ ⟩
    bwd hφ = ∣ (m , equivFun (decode .snd) hφ) , refl ∣₁
```

## Def 只精化，不缩水

在不假设传递性时，两条事实已经确定 `Def A` 的位置。恒真公式定义出整个 `A`，所以 `A` 本身是 `Def A` 的一个成员；而 `Def A` 的每个成员都是 `A` 的子集。这里尚未断言 `A ⊆ Def A`。下一节将在传递性前提下逐一可定义 `A` 的成员，从而证明这条更强的包含。

私有辅助 `A-mem` 把大的隶属证明转成纤维形式：`A` 的成员 `y` 仅仅来自某个索引 `m`，满足 `⟪ A ⟫↪ m ≡ y`；由于 `∈-asFiber` 以数据形式返回纤维 (截断位于它消费的隶属证明之内)，可以用 `let` 把对子拆开。两个集合的相等由 `extensionality` 证明，因此只需给出两个方向的包含。

```agda
  private
    A-mem : (y : S) → ⟨ y ∈ˢ A ⟩ → Σ[ m ∈ ⟪ A ⟫ ] (⟪ A ⟫↪ m ≡ y)
    A-mem y y∈ = ∈-asFiber {a = y} {b = A} y∈

  defSet⊤≡A : defSet ⊤̇ ≡ A
  defSet⊤≡A = extensionality (defSet ⊤̇) A (sub₁ , sub₂)
```

容易的方向复用刚证得的包含。`defSet ⊤̇` 的集合论成员 `y` 经 `sett` 隶属的定义给出截断的索引；`defSet⊆A` 随即把 `y` 放进 `A`，转换 `∈∈ₛ` 再把陈述包装成包含 `⊆` 所期望的形式。这一半完全不用 `⊤̇` 的含义：它对每个 `defSet φ` 都成立。

```agda
    where
    sub₁ : ⟨ defSet ⊤̇ ⊆ A ⟩
    sub₁ y y∈ₛ = ∈∈ₛ {a = y} {b = A} .fst
      (defSet⊆A ⊤̇ y (∈∈ₛ {a = y} {b = defSet ⊤̇} .snd y∈ₛ))
    sub₂ : ⟨ A ⊆ defSet ⊤̇ ⟩
```

反向用到「真」的含义：由于 `⊤̇` 在每个成员处成立，`defSet-mem ⊤̇ m` 把 `⟪ A ⟫↪ m ∈ˢ defSet ⊤̇` 等同于一个任何元素都能证明的命题，这里以恒等函数给出。于是 `A` 的每个成员 `y`，既然仅仅是 `⟪ A ⟫↪ m`，就沿纤维路径被搬运进 `defSet ⊤̇`。注意 `subst ⟨_⟩` 中 `sym (defSet-mem ⊤̇ m)` 的用法：该定理是命题之间的路径，因此可以按目标需要的方向搬运证明。

```agda
    sub₂ y y∈ₛ =
      let (m , q) = A-mem y (∈∈ₛ {a = y} {b = A} .snd y∈ₛ)
      in subst (λ v → ⟨ v ∈ₛ defSet ⊤̇ ⟩) q
           (∈∈ₛ {a = ⟪ A ⟫↪ m} {b = defSet ⊤̇} .fst
             (subst ⟨_⟩ (sym (defSet-mem ⊤̇ m)) (λ z → z)))
```

对偶的包含 `Def∋⊆A` 说 `Def A` 的每个元素都是 `A` 的子集。它的前提本身就是截断：`x` 仅仅是某个 `defSet φ`。目标是由命题经乘积构成的命题，因此 `PT.rec` 可以消去截断；随后沿把 `x` 等同于 `defSet φ` 的路径反向搬运 `y ∈ˢ x`，并应用 `defSet φ` 的包含。与给出 `A ∈ Def` 的 `defSet⊤≡A` 合观，图景完整：`Def` 把 `A` 作为元素包含在内，且只包含 `A` 的子集。

```agda
  Def∋⊆A : (x : S) → ⟨ x ∈ˢ Def ⟩ → (y : S) → ⟨ y ∈ˢ x ⟩ → ⟨ y ∈ˢ A ⟩
  Def∋⊆A x = PT.rec (isPropΠ λ y → isPropΠ λ _ → snd (y ∈ˢ A))
    (λ { (φ , q) y y∈x → defSet⊆A φ y (subst (λ s → ⟨ y ∈ˢ s ⟩) (sym q) y∈x) })
```

## 传递性之下，A ⊆ Def A

当 `A` 传递时，`A` 的每个**成员** `a` 自身也可定义：仍用模型章构造交集的那条两符号途径，即原子公式「该变量属于 `a`」。分离暗含的「∈ A」条件恰好由传递性保证：`a` 的成员已是 `A` 的成员，于是原子公式刻出的正是 `a`。故 `A ⊆ Def A`：没有任何元素被遗漏。与上一节合观，迭代 `Def` 只增不减，正合可构造塔的需要。

子模块以 `A` 的传递性为显式前提。原子公式 `atom mₐ` 是 `var zero ∈̇ con mₐ`：一个自由变量槽位，加上命名元素 `mₐ` 的单个常元。这里再次体现了以 `⟪ A ⟫` 为常元域这一设计选择的好处：`A` 的每个成员都可充作常元，由 `ι` 解码到限制载体。

```agda
  module Refine (Atrans : Transitive 𝒮ᵥ M) where

    atom : ⟪ A ⟫ → Formula ⟪ A ⟫ 1
    atom mₐ = var zero ∈̇ con mₐ

    atom-mem : (mₐ m : ⟪ A ⟫)
             → (⟪ A ⟫↪ m ∈ˢ defSet (atom mₐ)) ≡ (⟪ A ⟫↪ m ∈ˢ ⟪ A ⟫↪ mₐ)
```

把隶属定理特化到这个原子是直接的：环境固定为单个参数 `m`，而由原子公式的语义，`var zero ∈̇ con mₐ` 的内层真值恰是限制世界内的隶属 `⟪ A ⟫↪ m ∈ˢ ⟪ A ⟫↪ mₐ`。由于限制隶属由底层集合的外围隶属定义，这个原子确实选中 `⟪ A ⟫↪ mₐ` 的元素；剩下的工作只是证明呈现出的集合 `defSet (atom mₐ)` 等于那个元素。

```agda
    atom-mem mₐ m = defSet-mem (atom mₐ) m

    defSet-atom≡ : (mₐ : ⟪ A ⟫) → defSet (atom mₐ) ≡ ⟪ A ⟫↪ mₐ
    defSet-atom≡ mₐ = extensionality (defSet (atom mₐ)) (⟪ A ⟫↪ mₐ) (sub₁ , sub₂)
      where
      sub₁ : ⟨ defSet (atom mₐ) ⊆ ⟪ A ⟫↪ mₐ ⟩
```

正向包含消去 `y ∈ˢ defSet (atom mₐ)` 的截断索引：索引是一个对子 `(m , h)`，其中 `h` 证明原子在 `m` 处成立，再加上来自索引映射的路径 `q`。经 `atom-mem`，证明 `h` 变成环境意义下的隶属 `⟪ A ⟫↪ m ∈ˢ ⟪ A ⟫↪ mₐ`，`∈∈ₛ` 把它转换为 `⟪ A ⟫↪ mₐ` 的集合论成员；沿 `q` 搬运即完成。这与 `defSet⊆A` 的证明互为镜像，只是用原子的含义替代了平凡的「属于 `A`」。

```agda
      sub₁ y y∈ₛ = PT.rec (snd (y ∈ₛ ⟪ A ⟫↪ mₐ))
        (λ { ((m , h) , q) →
          subst (λ v → ⟨ v ∈ₛ ⟪ A ⟫↪ mₐ ⟩) q
            (∈∈ₛ {a = ⟪ A ⟫↪ m} {b = ⟪ A ⟫↪ mₐ} .fst
              (subst ⟨_⟩ (atom-mem mₐ m) ∣ (m , h) , refl ∣₁)) })
```

反向包含是传递性登场之处。给定 `y ∈ˢ ⟪ A ⟫↪ mₐ`，展开为外围隶属 `y∈a`；`A` 的传递性说「`A` 的成员的成员仍是 `A` 的成员」，这里以见证 `mₐ-as` (即 `⟪ A ⟫↪ mₐ ∈ˢ A`) 施用。于是 `y ∈ˢ A`，纤维分解交出一个索引 `m`，满足 `⟪ A ⟫↪ m ≡ y`，随时可呈现为 `defSet (atom mₐ)` 的元素。

```agda
        (∈∈ₛ {a = y} {b = defSet (atom mₐ)} .snd y∈ₛ)
      sub₂ : ⟨ ⟪ A ⟫↪ mₐ ⊆ defSet (atom mₐ) ⟩
      sub₂ y y∈ₛ =
        let y∈a     = ∈∈ₛ {a = y} {b = ⟪ A ⟫↪ mₐ} .snd y∈ₛ
            y∈A     = Atrans {x = ⟪ A ⟫↪ mₐ} {y = y} y∈a mₐ-as
```

收尾时，刚得到的索引 `m` 必须确实在自身处满足该原子。沿纤维路径反向搬运 `y∈a` 把隶属放进 `⟪ A ⟫↪ mₐ` 之内，`atom-mem` 经 `sym` 反向读出，把它转换为 `smallSat (atom mₐ) m` 的证明。最后沿 `q` 的搬运落在 `defSet (atom mₐ)` 中。两个包含合起来给出集合的相等。注意这里的每个移送都在沿集合或命题的路径搬运**证明**，从不制造新数据。

```agda
            (m , q) = ∈-asFiber {a = y} {b = A} y∈A
        in subst (λ v → ⟨ v ∈ₛ defSet (atom mₐ) ⟩) q
             (∈∈ₛ {a = ⟪ A ⟫↪ m} {b = defSet (atom mₐ)} .fst
               (subst ⟨_⟩ (sym (atom-mem mₐ m))
                 (subst (λ v → ⟨ v ∈ˢ ⟪ A ⟫↪ mₐ ⟩) (sym q) y∈a)))
```

有了这个等式，距 `Def` 的隶属只剩一次截断。给定 `a ∈ˢ A`，该隶属的纤维分解提供索引 `mₐ`，满足 `⟪ A ⟫↪ mₐ ≡ a`；由于此处纤维是数据，可以用 `let` 打开对子并命名 `mₐ`。

```agda
        where
        mₐ-as : ⟨ ⟪ A ⟫↪ mₐ ∈ˢ A ⟩
        mₐ-as = ∈∈ₛ {a = ⟪ A ⟫↪ mₐ} {b = A} .snd (∈ₛ⟪ A ⟫↪ mₐ)

    A⊆Def : (a : S) → ⟨ a ∈ˢ A ⟩ → ⟨ a ∈ˢ Def ⟩
    A⊆Def a a∈ =
```

`Def` 的元素 `defSet (atom mₐ)` 等于 `⟪ A ⟫↪ mₐ`，与纤维路径 `q` 复合得 `defSet (atom mₐ) ≡ a`。把「一个公式加上这条等式」用截断 `∣_∣₁` 包装，恰好给出 `Def` 的隶属所要求的：一个其定义出的子集为 `a` 的公式，仅仅存在。于是 `A` 的每个元素都进入 `Def`，结合上一节，该算子只作精化。

```agda
      let (mₐ , q) = ∈-asFiber {a = a} {b = A} a∈
      in ∣ atom mₐ , defSet-atom≡ mₐ ∙ q ∣₁
```

### 从外部读可定义性

有一条推论值得单独命名，因为可构造层的证明要反复倚重它。属于 `defSet φ` 是**内层**世界 `(A, ∈)` 中的陈述，而接下来的论证都在外围层级进行。对 Δ₀ 公式，两种读法一致，这就是绝对性定理；其余的只是层级核对，因为绝对性对类的成员陈述，而 `defSet` 对小索引类型陈述。重标正是为了消除这道层级差异，整个证明分三步：`defSet` 的规格、公式的重标、然后绝对性。

这需要 `A` 传递，故本引理归入这个子模块；塔的每层都传递。

绝对性模块在外围结构、类 `M` 与传递性前提上实例化，得到限制结构 `Abs.𝒮M`、外层满足 `Abs.⊨ᵛ` 与 Δ₀ 绝对性 `Abs.abs₀`。该陈述取一条证明 `φ` 是 Δ₀ 的见证 `d`，并断言命题之间的路径：`⟪ A ⟫↪ m` 属于 `defSet φ` 这一命题，等于公式 `mapFo ι φ` 在**外围**结构中于环境 `⟪ A ⟫↪ m ∷ []` 处的满足。右边的公式把常元经 `ι` 映射，因而是外围载体上的、指称 `A` 成员的公式。

```agda
    module Abs = FOL.Absoluteness.Single 𝒮ᵥ M Atrans

    abs-defSet : (φ : Formula ⟪ A ⟫ 1) → Δ₀ φ → (m : ⟪ A ⟫)
               → (⟪ A ⟫↪ m ∈ˢ defSet φ)
                 ≡ ((⟪ A ⟫↪ m ∷ []) Abs.⊨ᵛ (mapFo ι φ))
    abs-defSet φ d m =
```

证明复合三条路径。第一，`defSet-mem` 把可定义子集中的隶属读作 `φ` 在 `ι m` 处的内层满足。第二，`⊨-map` (取对称方向，故有 `sym`) 说经 `ι` 改名常元不改变真值，因为 `ι` 恰是内层世界的常元解释；剩下的是改名后公式 `mapFo ι φ` 的内层满足。第三，`abs₀` 把这条 Δ₀ 公式的内层满足搬运为外围结构中的外层满足，这也是唯一用到传递性的一步。此结果让后续章节可以把可定义子集中的隶属当作环境层面的陈述，而不只是内层陈述。

```agda
        defSet-mem φ m
      ∙ sym (⊨-map Abs.𝒮M ι id φ (ι m ∷ []))
      ∙ Abs.abs₀ (mapΔ₀ ι d) (ι m ∷ [])
```

## 小结

`Def A` 是内层世界 `(A, ∈)` 中由带 `A` 中参数的公式定义出的 `A` 的子集之集：语法充作索引集，内层满足给出含义，本质小性保证所需的宇宙层级。规格 `defSet-mem` 直接陈述「可定义」的含义，而算子只作精化：传递性下 `A ⊆ Def A` (`A⊆Def`)，且 `Def A` 的成员都是 `A` 的子集 (`Def∋⊆A`)。下一章把这一步迭代成一个宇宙。