---
title: "对后继封闭的序数层中的数码"
module: L.Coding.NumeralBound
lang: zh
site: "Bedrock"
description: "对后继封闭的序数层中的数码"
stage: "内部编码：表与统一满足关系"
reading_order: 56
canonical: https://bedrock.institute/zh/L.Coding.NumeralBound.html
html: L.Coding.NumeralBound.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/Coding/NumeralBound.lagda.md
prerequisites: [Base.Prelude, Base.Classical, FOL.ZFStructure, V.Hierarchy, L.Constructible, L.Axioms.Numerals, L.Ordinal, L.Ordinal.Stages]
routes: [internal-satisfaction]
translations: [https://bedrock.institute/en/L.Coding.NumeralBound.md, https://bedrock.institute/ja/L.Coding.NumeralBound.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
# 对后继封闭的序数层中的数码

有限序数提供公式码所用的数码。本章证明，当层的序数指标包含零且对后继封闭时，每个数码都属于该层。我们先处理任意单调且在后继层包含原序数的层族，再将结论应用于可构造层级。

本章固定一个宇宙层级 ℓ，并把层级 ℓ-suc ℓ 上的排中律作为显式参数 `lem`。把数码放进序数的初等归纳并不使用它；这里之所以携带这个假设，是因为可构造特化的一项原料，即序数出现在以其后继为指标的层这一定理，来自经典的序数层章节。

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

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

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

必须区分数码的两种呈现。周遭数码 `# k` 是 `V ℓ` 中的有穷 von Neumann 序数；模型数码 `numeralL k` 是 `L` 的元素，其底层集合为 `# k`。论证先为周遭序数证明界，随后才用投影等式 `numeralL-fst` 把结论转到模型呈现。

```agda
open import FOL.ZFStructure using ( module hPropStructure )
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ )
open import L.Constructible {ℓ} using ( IsOrd; Lset; Lset-mono )
open import L.Axioms.Numerals {ℓ} using ( numeralL; numeralL-fst )
open import L.Ordinal {ℓ} using ( numeral-ord )
```

周遭数码就生活在累积层级自身之中：`∅` 是其中的空集，`# k` 是有 k 个成员的有限冯·诺伊曼序数，`sucV` 是后继步骤 a ↦ a ∪ {a}。注意 `# (suc k)` 定义地就是 `sucV (# k)`，因此 λ 对 `sucV` 封闭就自动覆盖零之后的每个数码。这里的真值是层级 ℓ-suc ℓ 上的命题，直接打包在 `hProp` 中，所以每条隶属断言都是命题。

```agda
open import L.Ordinal.Stages {ℓ} lem using ( ord∈Lset-suc )

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

论证中的三种隶属各有作用：`# k ∈ λ` 把有穷序数置于指标之下；`# k ∈ T (sucV (# k))` 把它置于自身的后继层；`# k ∈ T λ` 才是所求的界。它们都作为命题陈述，因而归纳与后续搬运不依赖证明的选择；三者之间的推导仍分别依靠后继封闭、序数层性质与单调性假设。

```agda
open hPropStructure 𝒮ᵥ
```

## 单调层族的界

设 λ 包含零且对后继封闭。归纳法先把每个数码 `# k` 放入 λ。要把同一个数码放入 `T λ`，先以 `numeral-ord k` 和后继层假设得到 `# k ∈ T (sucV (# k))`；后继封闭给出指标关系 `sucV (# k) ∈ λ`，单调性随即推出 `# k ∈ T λ`。

本节在固定载体 S 及其隶属 `⟨_∈ˢ_⟩` 上、其上的任意映射 T 以及关于 T 的两条假设来陈述。第一条 `T-mono` 把层指标的隶属 β ∈ α 连同 x ∈ T β 转换为 x ∈ T α。第二条 `T-ord` 是锚点：序数 δ 属于以其自身后继为指标的层 T (sucV δ)。

```agda
module BoundOver
  (T : S → S)
  (T-mono : {α β : S} → ⟨ β ∈ˢ α ⟩ → {x : S} → ⟨ x ∈ˢ T β ⟩ → ⟨ x ∈ˢ T α ⟩)
  (T-ord : (δ : S) → IsOrd δ → ⟨ δ ∈ˢ T (sucV δ) ⟩)
  (lam : S) (ordλ : IsOrd lam)
```

其余参数刻画指标 λ：它是一个集合，被证明为序数，包含 ∅，且对 `sucV` 封闭。证书 `ordλ` 记录 λ 自身是合法的序数层指标；两条封闭事实则是归纳法将要消耗的全部。

```agda
  (succλ : (d : S) → ⟨ d ∈ˢ lam ⟩ → ⟨ sucV d ∈ˢ lam ⟩)
  (∅∈λ : ⟨ ∅ ∈ˢ lam ⟩) where
```

每个周遭数码都落入 λ，其证明只使用刚才假设的两条封闭事实。这是论证中纯粹归纳的一半：不用排中律，不用 T 的任何性质，甚至连 λ 的序数证书也不参与。

对 k 归纳。基例恰是假设 ∅∈λ，因为 `# 0` 就是 ∅。归纳步中，`# (suc k)` 定义地就是 `sucV (# k)`，故把归纳假设 `# k ∈ λ` 交给 succλ 即得 `# (suc k) ∈ λ`。小情形显出形状：0 = ∅ ∈ λ，接着 {∅} = sucV ∅ ∈ λ，再接着数码 2 = sucV (sucV ∅) ∈ λ，每一步消耗一次后继封闭。

```agda
  #∈λ : (k : ℕ) → ⟨ (# k) ∈ˢ lam ⟩
  #∈λ zero    = ∅∈λ
  #∈λ (suc k) = succλ (# k) (#∈λ k)
```

属于 λ 是指标层面的陈述；属于层 T λ 是另一条不同的陈述，它需要 T 的两条性质，而不仅是 λ 的封闭性。路径要经过数码自身的后继层。

两步复合而成。第一步，在 δ = # k 处使用 T-ord，并以 `numeral-ord k` 证明该数码是序数，把 # k 放进 T (sucV (# k))。第二步，T-mono 把隶属从指标 sucV (# k) 提升到指标 λ：所需前提 # (suc k) ∈ λ 正是 #∈λ (suc k)，而它展开后就是 sucV (# k) ∈ λ，恰好是 T-mono 要求的指标间隶属。于是元素 # k 落入 T λ，序数证书在第一步中发挥了实际作用。

```agda
  #∈Tλ : (k : ℕ) → ⟨ (# k) ∈ˢ T lam ⟩
  #∈Tλ k = T-mono {α = lam} {β = sucV (# k)} (#∈λ (suc k))
    {x = # k} (T-ord (# k) (numeral-ord k))
```

## 可构造层级中的数码

可构造层具有单调性，每个序数也属于以后继为指标的层，因此一般的界适用于 L。我们还用模型内部的数码来表述这一隶属关系。

把抽象实例化只需指名见证。层族 T 取为 `Lset`，`Lset-mono` 提供沿序数指标隶属的单调性，`ord∈Lset-suc` 提供锚点：每个序数属于 `Lset (sucV α)`。定理 `ord∈Lset-suc` 携带这一特化所需的经典假设；数码归纳本身仍是前面给出的初等封闭论证。关于 λ 的假设原样传入，因此 `BoundOver` 内部关于 T λ 证明的一切，对 `Lset lam` 都同样可用。

```agda
module Bound (lam : S) (ordλ : IsOrd lam)
             (succλ : (d : S) → ⟨ d ∈ˢ lam ⟩ → ⟨ sucV d ∈ˢ lam ⟩)
             (∅∈λ : ⟨ ∅ ∈ˢ lam ⟩) where

  open BoundOver Lset Lset-mono ord∈Lset-suc lam ordλ succλ ∅∈λ public
```

在模型内部，数码不是环境序数本身，而是一个序对 `numeralL k`，其第一分量指称该序数。这条界通过一次搬运转移到该呈现上，而不必重做归纳。

等式 `numeralL-fst k` 是宿主理论中的一条路径 `fst (numeralL k) ≡ # k`。沿这条路径搬运隶属类型族，即可把关于 # k 的隶属证明变为关于 fst (numeralL k) 的证明。使用 `sym` 把路径定向为：从已经证明的 `# k` 的隶属，得到所求的 `fst (numeralL k)` 的隶属；于是 `#∈Tλ k` 化为关于模型数码的陈述。

```agda
  num∈λ : (k : ℕ) → ⟨ fst (numeralL k) ∈ˢ Lset lam ⟩
  num∈λ k = subst (λ w → ⟨ w ∈ˢ Lset lam ⟩) (sym (numeralL-fst k)) (#∈Tλ k)
```