---
title: "L 内部的基数与编码单射"
module: L.Cardinal
lang: zh
site: "Bedrock"
description: "L 内部的基数与编码单射"
stage: "序数、单射与基数"
reading_order: 89
canonical: https://bedrock.institute/zh/L.Cardinal.html
html: L.Cardinal.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/Cardinal.lagda.md
prerequisites: [Base.Prelude, Base.Classical, FOL.ZFStructure, FOL.Absoluteness, FOL.ZFModel, V.Hierarchy, V.Model, V.Presentation, V.Coding, L.Constructible, L.Ordinal, L.Ordinal.Stages, L.Ordinal.SquareLaw, L.WellOrder.Base, L.Coding.Model, L.Coding.Injection]
routes: [cardinal-tools]
translations: [https://bedrock.institute/en/L.Cardinal.md, https://bedrock.institute/ja/L.Cardinal.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
# L 内部的基数与编码单射

讨论 `L` 内部的基数，需要区分两种相互关联的比较。宿主可以用实际函数比较集合的小呈现类型；在 `L` 内部作出的陈述，则必须由本身可构造的图来见证。本章同时发展这两种概念，并明确保留它们的逻辑强度：具体函数与图码携带数据，后文所用的基数比较则只保留存在性。

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

论证在基础词汇章所介绍的宿主语言中进行。它唯一的经典资源，是对 `Type (ℓ-suc ℓ)` 中命题的排中律。这是一条受宇宙层级限制的假设，并非不受限制的排中律或选择原理。单射与图码的定义本身并不选取见证；经典推理在构造序数良序，以及后文利用该良序寻找最小元时才发挥作用。

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

因此，宇宙层级和这份排中律实例都明列为整章的参数。下面每项构造都相对于同一个 `lem`，途中不再加入其他公理。本章的目标是为后续基数论证准备精确的概念与有界次序，而不是已经断言基数代表或后继基数的存在。

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

后文始终同时涉及两种数学环境。累积层级提供外围集合以及取命题值的隶属关系；可构造模型则提供属于 `L` 的集合，以及在这些集合上解释的关系。基本事实 `a ∈ sucV a` 表明每个集合都属于其集合论后继 `a ∪ {a}`，它稍后会为一次有界搜索提供一个特定点。

```agda
open import FOL.ZFStructure using ( module hPropStructure )
import FOL.Absoluteness
import FOL.ZFModel
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ )
open import V.Model {ℓ} using ( self∈sucV )
```

每个外围集合还有一个典范的小呈现。呈现中的索引指名该集合的全部成员，`member` 把索引化为隶属证明，`fiber` 则从隶属恢复索引。有序对使一个集合能够表示关系。在可构造一侧，模型元素把外围集合与其属于 `L` 的证书配成一对；`L` 的传递性又把可构造性从集合传给它的每个成员。这些事实将把小呈现与可构造的图码联系起来。

```agda
open import V.Presentation {ℓ} using ( member; fiber )
open import V.Coding {ℓ} using ( pr )
open import L.Constructible {ℓ}
  using ( 𝒮ʟ; isL; isL-trans; IsOrd; Lset→isL )
open import L.Ordinal {ℓ} using ( suc-ord )
```

有界搜索将使用序数隶属关系在呈现上诱导的严格良序。它的三歧性最终使用 `lem`，良基性则来自外围隶属关系的正则性。另一些材料在对象语言中描述图的性质：单值性、恰当定义域与单射性。稍后用命题截断隐藏具体图码时，区分这些序论材料与逻辑材料十分重要。

```agda
open import L.Ordinal.Stages {ℓ} lem using ( ord∈Lset-suc )
open import L.Ordinal.SquareLaw {ℓ} lem using ( ordSWO )
open import L.WellOrder.Base {ℓₚ = ℓ-suc ℓ} using ( SWO; module SWO )
open import L.Coding.Model {ℓ} using ( svAt; domAt )
open import L.Coding.Injection {ℓ} lem using ( injAt )
```

对集合 `a`，以 `⟪ a ⟫` 表示索引其成员的小类型，以 `⟪ a ⟫↪` 表示把索引送到其所指成员的映射。集合论后继 `sucV a` 包含 `a` 的每个成员，也包含 `a` 本身。因此，当 `a` 是序数时，`⟪ sucV a ⟫` 是一个小搜索空间，其中既有指名所有更小序数的索引，也有指名 `a` 的索引。

```agda
open import Cubical.HITs.CumulativeHierarchy.Base using ( _∈_ )
open import Cubical.HITs.CumulativeHierarchy.Properties using ( ⟪_⟫; ⟪_⟫↪ )
open import Cubical.HITs.CumulativeHierarchy.Constructions
  using ( module InfinitySet )
open InfinitySet {ℓ} using ( sucV )
```

本书常用命题截断有意减弱存在性。`∥ X ∥₁` 的元素断言 `X` 有元素，却不透露具体元素。它可以消去到命题，例如用来表达反驳的空类型，却不能消去到任意数据。这条规则稍后会把 `InjCode` 中的具体图信息与 `InjL` 所断言的单纯存在严格区分开来。

```agda
import Cubical.Data.Empty as Empty
import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∥_∥₁ )
```

下面的记号标明一条陈述属于哪种环境。对外围结构，`_∈ˢ_` 是层级中裸集合之间取命题值的隶属关系。与此相对，`S` 是可构造结构的载体；元素 `a : S` 由底层外围集合 `fst a` 与其可构造性的命题值证书组成。因此，`⟨ fst x ∈ˢ fst a ⟩` 是关于底层外围集合的宿主层命题，而对 `x : S` 的量化只遍历可构造集合。对象语言的语法则通过下面引入的满足关系另行进入。

```agda
open hPropStructure 𝒮ᵥ using ( _∈ˢ_ )
open hPropStructure 𝒮ʟ using ( S )
```

可构造结构还带有取命题值的逐点包含关系。`⟨ a ⊆ˢ b ⟩` 的证明对每个 `x : S`，把 `x` 属于 `a` 的证明送到 `x` 属于 `b` 的证明；其中的量化因此遍历可构造载体。`L` 的传递性保证这与底层集合通常的包含读法一致。当 `a` 与 `b` 都是序数时，这正是它们的非严格次序。因此，后继基数的最小性条款以包含为结论，而严格比较则用隶属关系表达。

```agda
module ModelL = FOL.ZFModel 𝒮ʟ
open ModelL using ( _⊆ˢ_ )
```

满足记号 `_⊨_` 固定表示可构造结构中的解释。在判断 `γ ⊨ φ` 中，环境 `γ` 列出 `S` 的元素，所以 `φ` 中的无界量词遍历可构造集合。这正是 `InjCode` 前三个条件的语义内容；它们是在 `L` 内部成立的对象语言陈述，尽管其证明由宿主处理。

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

首先在宿主层定义单射。`X ↪ Y` 的元素由函数 `f : X → Y` 及其单射性证明组成；该证明表明，`f x` 与 `f y` 相等便推出 `x` 与 `y` 相等。函数是可以从这对数据中投影出的具体数据。定义不包含满射性或逆函数，也不涉及集合、可构造性证书、满足判断或截断。稍后，它的典型两端是两个外围集合的小呈现类型。

```agda
_↪_ : Type ℓ → Type ℓ → Type ℓ
X ↪ Y = Σ[ f ∈ (X → Y) ] ((x y : X) → f x ≡ f y → x ≡ y)
```

现在固定一个可构造集合 `α`，并假设其底层集合是序数。为了稍后寻找大小合适的序数，只需在 `sucV (fst α)` 的典范呈现中搜索。这个集合包含 `α` 的每个成员及 `α` 本身，所以搜索空间既是小类型，又带有一个自然起点。此处的定义只建立这个带序的搜索空间；后续论证才会给出候选谓词并执行最小元选择。

```agda
module LeastCardInjL (α : S) (oα : IsOrd (fst α)) where
```

第一项任务是证明这个集合论后继本身属于 `L`。由 `oα` 两次应用序数后继，可知 `sucV (sucV (fst α))` 是序数。序数属于下一可构造层的定理把 `sucV (fst α)` 放入这个明确给出的层，而属于某一层便给出其可构造性。因此，证明指明了一个包含该后继的具体层，并未诉诸「可构造性一般地对 `sucV` 封闭」这样的结论。

```agda
  hSucα : ⟨ isL (sucV (fst α)) ⟩
  hSucα = Lset→isL (sucV (sucV (fst α))) (suc-ord (suc-ord oα)) (sucV (fst α))
            (ord∈Lset-suc (sucV (fst α)) (suc-ord oα))
```

呈现中的每个索引 `m` 都指名 `sucV (fst α)` 的一个成员。这个后继已经证明可构造，而 `L` 具有传递性，所以被指名的成员也可构造。于是 `up` 保留 `m` 所指名的底层集合，并附上恰好由此得到的证书，从而产生 `S` 的元素。它只定义在这个有界呈现上，并不会把任意外围集合变成可构造集合。

```agda
  up : ⟪ sucV (fst α) ⟫ → S
  up m = ⟪ sucV (fst α) ⟫↪ m
       , isL-trans (member (sucV (fst α)) m) hSucα
```

序数的隶属关系为这些索引排序。把 `ordSWO` 应用于序数 `sucV (fst α)`，便在 `⟪ sucV (fst α) ⟫` 上得到严格良序 `w`：它依照所指集合之间的隶属关系作比较，三歧性依赖 `lem`，良基性则来自正则性。把这个值声明为不透明，只控制它在后续证明中是否展开，并不改变该关系、它的定律或这些定律所依赖的假设。

```agda
  opaque
    w : SWO (⟪ sucV (fst α) ⟫)
    w = ordSWO (sucV (fst α)) (suc-ord oα)
```

路径 `w-lt` 给出这个次序的可用描述。对索引 `m` 与 `n`，「`m` 在 `w` 下先于 `n`」这一命题，与「`m` 所指集合属于 `n` 所指集合」这一命题相等。这是命题类型之间的相等，并非集合之间的相等。后续证明可沿这条路径双向传输证据，在索引比较与序数隶属之间往返，同时无需展开良序的构造。

```agda
  opaque
    unfolding w
    w-lt : (m n : ⟪ sucV (fst α) ⟫)
         → SWO._<∙_ w m n ≡ ⟨ ⟪ sucV (fst α) ⟫↪ m ∈ˢ ⟪ sucV (fst α) ⟫↪ n ⟩
    w-lt m n = refl
```

这个搜索空间有一个指名 `fst α` 的特定索引。证明 `self∈sucV (fst α)` 给出该序数属于其集合论后继，而 `fiber` 把这条隶属化为一个索引以及描述其像的等式。层级中的隶属虽然取命题值，但呈现映射是嵌入，所以它的纤维本身是命题；因此可以把截断消去到这个唯一纤维，而无须调用选择原理。`self` 是由此恢复的索引，并不是该序数。

```agda
  self : ⟪ sucV (fst α) ⟫
  self = fiber (sucV (fst α)) (self∈sucV (fst α)) .fst
```

伴随等式准确说明 `self` 指名什么：它在呈现映射下的像等于 `fst α`。这条相等发生在底层外围集合之间；此处没有断言相应 `S` 元素相等，因为那还需要处理两边的可构造性证书。`self` 与 `self-eq` 合在一起，为后续搜索提供一个可以检验 `α` 之性质的具体索引。

```agda
  self-eq : ⟪ sucV (fst α) ⟫↪ self ≡ fst α
  self-eq = fiber (sucV (fst α)) (self∈sucV (fst α)) .snd
```

## 内部单射与后继基数

一个具体的可构造集合 `F`，首先通过 `L` 内部的三条满足条件来编码从 `a` 到 `b` 的单射。第一条说成对形状的条目具有单值性：同一输入不能有两个不相等的输出。第二条说定义域恰为 `a`，而且包含两个方向：每个成对形状条目的第一分量属于 `a`，`a` 的每个成员则仅仅存在某个输出。第三条说图具有单射性：输出相同的两个条目必有相等的输入。在三条判断中，环境都把 `F` 放在第一项、`a` 放在第二项，所有无界量词都遍历 `S`。

```agda
InjCode : S → S → S → Type (ℓ-suc ℓ)
InjCode F a b =
    ⟨ (F ∷ a ∷ []) ⊨ svAt zero ⟩
  × ⟨ (F ∷ a ∷ []) ⊨ domAt zero (suc zero) ⟩
  × ⟨ (F ∷ a ∷ []) ⊨ injAt zero ⟩
```

第四条条件直接在宿主中陈述。对任意 `x,y : S`，若它们的底层集合组成的有序对属于底层图，则底层输出属于 `b`。因此，`b` 是所有取值的陪域上界；条件并不说 `b` 的每个成员都被取到。`InjCode` 也没有断言 `F` 的每个成员都是有序对。它的条件只检查成对形状的成员，所以其他形状的附加成员不会影响从图码读出的函数。这个宿主层的值域约束必须与前三条对象语言满足判断区分开来。

```agda
  × ((x y : S) → ⟨ pr (fst x) (fst y) ∈ fst F ⟩ → ⟨ fst y ∈ fst b ⟩)
```

`InjL a b` 忘去是哪一个具体图满足这四条条件。它是依值对「`F` 与 `InjCode F a b`」的命题截断，所以只断言在 `L` 内部存在从 `a` 到 `b` 的编码单射。无法从中投影出特定图或宿主层函数。只有当目标是命题时，才能在局部分支中打开它；后续对单射作复合或变换的构造，会在这样的分支内使用图，再把所得图放回命题截断。方向也是陈述的一部分：`InjL a b` 本身并不蕴含 `InjL b a`。

```agda
InjL : S → S → Type (ℓ-suc ℓ)
InjL a b = ∥ Σ[ F ∈ S ] InjCode F a b ∥₁
```

当 `κ` 是序数时，基数性由初始性表达。冯·诺伊曼序数的每个成员 `δ` 都是更小的序数，而 `IsCardinalL κ` 反驳「存在满足 `InjCode F κ δ` 的可构造图」这一命题截断。用刚定义的记号说，它排除 `InjL κ δ`，并不排除 `InjL δ κ`。这两个都是内部编码单射的命题，不是宿主层类型 `_↪_` 的实例；一般也不能从它们的截断中抽取后一种宿主层单射。这一定义也可对一般可构造集合形成，其中没有 `κ` 为序数的证明；后续使用处会另行提供 `IsOrd (fst κ)`，然后才作初始序数的解释。由于反驳以空类型为目标，所需的命题截断消去是正当的。

```agda
IsCardinalL : S → Type (ℓ-suc ℓ)
IsCardinalL κ =
  (δ : S) → ⟨ fst δ ∈ fst κ ⟩
          → (∥ Σ[ F ∈ S ] InjCode F κ δ ∥₁ → Empty.⊥)
```

`SuccCardL δ κ` 的参数次序规定，`δ` 是候选后继基数，`κ` 是它所超越的对象。前三个条款分别说：`δ` 的底层集合是序数，`δ` 满足初始性谓词，并且 `κ ∈ δ`；在序数语境中，最后一点表示 `δ` 严格大于 `κ`。这些条款只描述给定一对对象的性质，并不产生这样的 `δ`，也不要求 `κ` 本身是序数或基数。定义的最后一个条款还会加入全局最小性。这里没有出现 `sucV`：后继基数不是集合论后继 `κ ∪ {κ}`。

```agda
SuccCardL : S → S → Type (ℓ-suc ℓ)
SuccCardL δ κ =
    IsOrd (fst δ)
  × IsCardinalL δ
  × ⟨ fst κ ∈ fst δ ⟩
```

最后一个字段表达 `κ` 之上所有内部序数基数中的最小性。给定任意 `c : S`，若其底层集合是序数，满足 `IsCardinalL c`，且包含 `κ`，该字段就给出内部包含 `δ ⊆ˢ c`。第一个字段已经说明 `δ` 是序数，因此包含关系在此就是序数的非严格比较：`δ` 不大于每个这样的 `c`。结论使用包含而非成员关系，因为它还必须适用于 `c` 就是 `δ` 的情形。对 `S` 的量化与 `_⊆ˢ_` 都作用于可构造载体，所以这是 `L` 中可见候选者之间的最小性。该字段对 `κ` 只假设 `κ ∈ c`；断言 `κ` 本身是序数和内部基数的假设，由使用这个谓词的各定理提供。

这个字段不构造任何单射图。`InjCode F a b` 保留一个特定的可构造码 `F` 及其四项单射条件，而 `InjL a b` 是 `∥ Σ[ F ∈ S ] InjCode F a b ∥₁` 的命题截断。因此，把假设 `IsCardinalL c` 与 `c` 的序数性合在一起，它说的是：不存在从 `c` 到其任一较小序数成员的 `InjL` 单射。`SuccCardL δ κ` 本身是固定之对 `δ, κ` 的未截断性质：它既不证明合适的 `δ` 存在，也不选定一个 `δ`。后文的 `succCardExists` 在 `κ` 是序数内部基数且不是有限序数时，证明这种 `δ` 的命题截断存在性；所用的经典假设仍只是模块参数 `LEM (ℓ-suc ℓ)`。集合论后继 `sucV` 并未出现在这个定义中。

```agda
  × ((c : S) → IsOrd (fst c) → IsCardinalL c → ⟨ fst κ ∈ fst c ⟩
             → ⟨ δ ⊆ˢ c ⟩)
```