---
title: "L 中的无穷公理"
module: L.Axioms.Infinity
lang: zh
site: "Bedrock"
description: "L 中的无穷公理"
stage: "可构造层与公理"
reading_order: 39
canonical: https://bedrock.institute/zh/L.Axioms.Infinity.html
html: L.Axioms.Infinity.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/Axioms/Infinity.lagda.md
prerequisites: [Base.Prelude, Base.Classical, FOL.ZFStructure, FOL.ZFModel, L.Constructible, L.Ordinal, L.Ordinal.Stages, L.Axioms.Basic, L.Axioms.Numerals]
routes: [constructible-axioms]
translations: [https://bedrock.institute/en/L.Axioms.Infinity.md, https://bedrock.institute/ja/L.Axioms.Infinity.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
# L 中的无穷公理

`L` 内构造性定义的数码链 `numeralL` 为每个自然数给出一个内部数码。但一条由各自分离的集合组成的链还不是无穷集合：无穷公理要求一个可构造集合，其成员恰为诸数码。本章给出这个集合，并顺带指出把候选集合放进可构造层级时所用的经典依赖：所导入的层定理依赖序数比较，因此以模块参数 `lem` 为参数。

模块只带一个假设 `lem : LEM (ℓ-suc ℓ)`，即比工作层级 ℓ 高一层级的命题的判定。本章所需的一切，要么是构造性的，要么由这一个参数导出，因此后文的证明可以带着「哪些步骤是经典的」这一精确账目来读。

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

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

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

周遭集合层级提供 `ω` 与后继 `sucV`，而 `numeralL-fst` 把每个内部数码同 `ω` 的相应成员联系起来。以 `lem` 实例化的层定理 `ord∈Lset-suc` 把序数置于其后继层。下述证明只在这里调用以排中律为参数的结果。

```agda
open import FOL.ZFStructure using ( module hPropStructure )
import FOL.ZFModel
open import L.Constructible {ℓ} using ( 𝒮ʟ; isL )
open import L.Ordinal {ℓ} using ( suc-ord; ω-ord )
open import L.Ordinal.Stages {ℓ} lem using ( ord∈Lset-suc )
```

命题截断表达单纯存在：`∣_∣₁` 把给定见证置于这一截断中。运算 `⇔toPath` 把真值间的两个蕴涵转换为真值间的路径，这正是集合规格所要求的形式。

```agda
open import L.Axioms.Basic {ℓ} using ( uniqueL )
open import L.Axioms.Numerals {ℓ} using ( numeralL; numeralL-fst )

import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∣_∣₁ )
open import Cubical.Functions.Logic using ( ⇔toPath )
```

这里的真值是 `hProp` 封装；其索引析取 `∃[ x ] P x` 表达沿某个载体的单纯存在。对可构造结构 `𝒮ʟ`，`∈ˢ` 表示属于，`≈ˢ` 表示结构相等，其底层等式是周遭集合之间的等式。

```agda
open import Cubical.HITs.CumulativeHierarchy.Constructions
  using ( module InfinitySet )
open InfinitySet using ( sucV; ω )

open hPropStructure 𝒮ʟ
```

最后，`SetOf` 指名一个类的实现者类型：一个可构造集合，连同「对每个元素，其属于真值等于该类的值」的证明。模型 record 的无穷字段将要求这个类型具有可缩性，而 `uniqueL` 会从单独一个实现者提供它。

```agda
module ModelL = FOL.ZFModel 𝒮ʟ
open ModelL using ( SetOf )
```

## 收集这条链

周遭集合 `ω` 的成员是库中的数码，因此它是自然的候选。其可构造性证明把 `ord∈Lset-suc` 应用于 `ω`；这条导入的层定理以模块参数 `lem` 实例化。数码链及其成员规格的定义本身不调用该参数。

命题 `ω∈L` 具有 `isL` 定义所规定的截断形式。截断前的一个见证是层 `sucV ω`：`ω-ord` 说明 `ω` 是序数，`suc-ord` 说明其冯·诺伊曼后继 `sucV ω` 仍是序数，而 `ord∈Lset-suc` 把 `ω` 置于该层。元素 `ωʟ` 把周遭集合 `ω` 与这一可构造性证明配对，因此 `x ∈ˢ ωʟ` 就是对其底层周遭集合的属于关系。

```agda
ω∈L : ⟨ isL ω ⟩
ω∈L = ∣ sucV ω , (suc-ord ω-ord , ord∈Lset-suc ω ω-ord) ∣₁

ωʟ : S
ωʟ = ω , ω∈L
```

余下的工作是核实 `ωʟ` 的成员恰是内部数码。类 `isNumeralL` 对元素 `x` 说：存在某个自然数 `n`，使 `x` 结构上等于链的第 `n` 节；作为索引析取，它仅仅断言某个下标可行，而不选定任何一个。规格 `ω-specL` 接着证明，属于 `ωʟ` 与 `isNumeralL` 作为真值逐点一致；`hasInfinityL` 再把这个实现者提升为公理字段所要求的可缩性。规格的两个方向都经过同样两件素材：`ω` 中属于关系的周遭刻画，以及链的投影方程 `numeralL-fst`。

类 `isNumeralL` 沿载体 `Lift ℕ` 析取命题族 `x ≈ˢ numeralL (lower n)`。这里的 `Lift` 值得一提：`∃[ x ] P x` 要求载体住在工作层级，而 `ℕ` 住在 `ℓ-zero`；提升是纯粹的对齐层级的调整，恰带同样的元素，`lower` 取回普通下标。规格 `ω-specL` 把目标写成真值之间的一条路径 `(x ∈ˢ ωʟ) ≡ isNumeralL x`，而 `⇔toPath` 把这条路径的证明化归为两个蕴涵的证明。

```agda
isNumeralL : S → hProp (ℓ-suc ℓ)
isNumeralL x = ∃[ n ∶ Lift {ℓ-zero} {ℓ-suc ℓ} ℕ ] x ≈ˢ numeralL (lower n)

ω-specL : (x : S) → (x ∈ˢ ωʟ) ≡ isNumeralL x
ω-specL x = ⇔toPath
  (PT.map (λ { (k , p) → lift (lower k)
```

两个方向都在命题截断内部映射见证。正向把提升后的下标写成 `k : Lift ℕ`，并令 `n = lower k`。`ω` 中的周遭属于关系给出 `p : # n ≡ fst x`，于是 `sym p ∙ sym (numeralL-fst n)` 证明 `x ≈ˢ numeralL n`。反向从 `q : fst x ≡ fst (numeralL n)` 构造路径 `sym (q ∙ numeralL-fst n) : # n ≡ fst x`，得到所需的周遭属于见证。因此 `ωʟ` 的成员恰为内部数码。最后，`uniqueL` 以显式实现者 `(ωʟ , ω-specL)` 为可缩中心，并给出从该中心到任意其他实现者的路径，从而证明 `SetOf isNumeralL` 可缩。

```agda
             , (sym p ∙ sym (numeralL-fst (lower k))) }))
  (PT.map (λ { (n , q) → lift (lower n)
             , (sym (q ∙ numeralL-fst (lower n))) }))

hasInfinityL : isContr (SetOf isNumeralL)
hasInfinityL = uniqueL isNumeralL (ωʟ , ω-specL)
```

## 小结

可构造集合 `ωʟ` 恰好收集数码链 `numeralL`。显式实现者与外延唯一性给出无穷字段所要求的可缩性。证明在确立 `ω` 的可构造性时通过 `ord∈Lset-suc` 使用排中律参数；成员规格本身则由上述两个投影路径得到。