---
title: "首次与集合相交的层"
module: L.Choice.FirstIntersectionStage
lang: zh
site: "Bedrock"
description: "首次与集合相交的层"
stage: "典范良序与选择公理"
reading_order: 72
canonical: https://bedrock.institute/zh/L.Choice.FirstIntersectionStage.html
html: L.Choice.FirstIntersectionStage.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/Choice/FirstIntersectionStage.lagda.md
prerequisites: [Base.Prelude, Base.Classical, FOL.ZFStructure, V.Hierarchy, V.Model, L.Constructible, L.Ordinal, L.Ordinal.Stages, L.Stage, L.Axioms.Basic]
routes: [canonical-order]
translations: [https://bedrock.institute/en/L.Choice.FirstIntersectionStage.md, https://bedrock.institute/ja/L.Choice.FirstIntersectionStage.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
# 首次与集合相交的层

本章为内部选择构造提供两样原料。第一是关于最小层的引理。当一条序数性质首次成立时，它在一个最小层处成立；该层是否为后继并非自动成立，因为性质可能在零序数处首次成立。本章证明论证所需的条件形式：若除最小层之外，一次雕出仅仅存在，即存在低于它的序数 `δ` 使性质在后继 `sucV δ` 处已经成立，则最小层是后继，且有唯一的前一层。第二样原料是一个上界序数：对可构造集合而言，存在一个序数，其层同时容纳该集合、它的成员、成员的成员，以及塔的极限层。

这些材料服务于一把双钥匙的比较。首次出现在不同层的两个集合，仅凭各自的诞生序数比较，别无其他；只有首次出现在同一层的集合，才在该层之内按名字比较。第一样原料使每个诞生序数成为确定的对象，而非单纯的存在；第二样原料保证一整族候选者所需的材料都住进同一个层，从而名字的比较有共同的场地。

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

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

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

全章在唯一一条假设下运行：模型层级的后继处的一份排中律实例；以下每条陈述都在这一设定之内作出。

```agda
open import FOL.ZFStructure using ( module hPropStructure )
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ; ∈-irrefl )
open import V.Model {ℓ} using ( ∈sucV-elim; self∈sucV )
```

本章的问题是关于首次出现的。一个可构造集合会在某个时刻进入层之塔；塔所居于的环境层级具有非自反的隶属，故没有序数包含自身，而其后继的性质也已清楚：序数坐在自己的后继之内，后继的成员或是该序数的成员、或是该序数本身。

```agda
open import L.Constructible {ℓ}
  using ( IsOrd; isPropIsOrd; isL; Lset; Lset-layer; Lset-out
        ; Lset-mono; layer-trans )
```

可构造一侧以塔 `Lset` 作答，塔由序数索引，序数是层级的集合，而非宿主的宇宙层级。序数性 `IsOrd` 本身是命题；塔有层关系、向外的分解与单调性；传递性则在层之间搬运成员。

```agda
open import L.Ordinal {ℓ} using ( mem-ord; suc-ord; bound2; ω-ord )
open import L.Ordinal.Stages {ℓ} lem using ( suc∈or≡ )
open import L.Stage {ℓ} lem
  using ( isLeastOrd; stage; stage-ord; stage-mem )
open import L.Axioms.Basic {ℓ} using ( Lset-suc )
```

论证依靠比较与层。把低于某层的序数与该层自身相比，正是判定该层是否越过一个后继的方法；序数的成员与序数的后继都仍是序数。每个可构造集合携带着它最早的序数，连同序数性与隶属交付，而极小性以反驳形式陈述。两个序数有共同上界。后继恒等式则说：下一层恰是上一层的可定义子集，这正是任何东西得以进入塔的那一步。

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

论证以三个命题动作写成：分裂成情形、以空类型告终的反驳，以及仅知其为存在的存在。

```agda
open import Cubical.Data.Sigma using ( Σ≡Prop )
open import Cubical.Foundations.HLevels using ( isProp× )
open import Cubical.HITs.CumulativeHierarchy.Base using ( setIsSet )
```

前一层把一个序数与命题性的证据配成一对。这类序对由第一分量决定；累积层级本身又是集合，因此前一层的相等归结为其序数分量的相等。

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

层级的无穷构造同时给出冯·诺伊曼后继 `sucV`，以及上界所要包含的极限层 `ω`。

```agda
open hPropStructure 𝒮ᵥ
```

结构隶属 `∈ˢ` 是序数性、层与极小性共同陈述其中的关系。

## 最小层的前一层

问题是：某物现身的那个最小层是否为后继，若是，它后继的是哪一层。单独的最小层未必是后继，因为性质可能从零开始；构造在「其下有雕出」这一附加假设之下产出唯一的前一层。

后继决定它所后继的东西，至少在序数之内如此。把一个候选前一层与另一个相比：各自属于对方的后继，故各自或是对方的成员、或与对方相等；而两个序数不能互为成员，否则传递性会使其一属于自身。于是「是给定序数的前一层」是命题，正是这一点使一个仅仅存在的前一层可以被读作一个确定的前一层。

最小层凭什么有前一层？这需要两样输入，值得分开看。第一是最小层自身：性质在其中成立的序数 `σ`，其极小性以反驳形式陈述，即没有更小的序数拥有该性质。第二是 `σ` 处雕出的仅仅存在：`σ` 以下的某个序数 `δ`，其后续 `sucV δ` 处性质已经成立。有了雕出，极小性排除「后继仍严格在下」，而不越头的比较只剩一种情形：被雕出序数的后继恰是 `σ`。于是最小层是后继，而被雕出的序数就是它的前一层。没有雕出则推不出任何东西：性质可能恰在零序数处首次成立，而零以下根本没有序数。

```agda
IsPredOf : S → S → Type (ℓ-suc ℓ)
IsPredOf σ δ = IsOrd δ × (sucV δ ≡ σ)
```

序数 `σ` 的候选前一层 `δ` 是一个序数，其冯·诺伊曼后继就是 `σ` 本身。两半都不可或缺：序数性是比较所需的，等式则是把 `δ` 钉在 `σ` 上的。

```agda
private
  cycle₂ : (a b : S) → IsOrd a → ⟨ a ∈ˢ b ⟩ → ⟨ b ∈ˢ a ⟩ → Empty.⊥
  cycle₂ a b orda a∈b b∈a = ∈-irrefl a (orda .fst a∈b b∈a)
```

没有序数能属于它自己的某个成员：传递性会把这条隶属沿两步循环搬回 `a` 自身，与非自反性矛盾。正是这个两步的不可能性，禁止两个序数互为成员。

```agda
  mem-branch : (δ δ' : S) → IsOrd δ → ⟨ δ' ∈ˢ sucV δ ⟩ → ⟨ δ ∈ˢ δ' ⟩ → δ ≡ δ'
  mem-branch δ δ' ordδ δ'∈sδ δ∈δ' =
    ∈sucV-elim {A = δ} {x = δ'} (setIsSet δ δ') δ'∈sδ
      (λ δ'∈δ → Empty.rec (cycle₂ δ δ' ordδ δ∈δ' δ'∈δ))
      (λ δ'≡δ → sym δ'≡δ)
```

隶属分支读作：`δ'` 属于 `δ` 的后继，且 `δ` 属于 `δ'`；结论必为 `δ ≡ δ'`。倘若 `δ'` 属于 `δ` 自身，两步循环便会闭合；故 `δ'` 就是 `δ` 自身，消去恰返回这一点。

```agda
ord-suc-inj : (δ δ' : S) → IsOrd δ → sucV δ ≡ sucV δ' → δ ≡ δ'
ord-suc-inj δ δ' ordδ e =
  ∈sucV-elim {A = δ'} {x = δ} (setIsSet δ δ') δ∈sδ'
    (mem-branch δ δ' ordδ δ'∈sδ)
    (λ δ≡δ' → δ≡δ')
```

后继运算在序数上是单射的。由后继的等式，`δ` 属于 `sucV δ'`；消去给出两种读法。要么 `δ` 属于 `δ'`，此时隶属分支闭合循环并给出等式；要么 `δ` 本来就是 `δ'`。后继决定它所后继者。

```agda
  where
  δ∈sδ' : ⟨ δ ∈ˢ sucV δ' ⟩
  δ∈sδ' = subst (λ w → ⟨ δ ∈ˢ w ⟩) e (self∈sucV δ)
  δ'∈sδ : ⟨ δ' ∈ˢ sucV δ ⟩
  δ'∈sδ = subst (λ w → ⟨ δ' ∈ˢ w ⟩) (sym e) (self∈sucV δ')
```

喂给消去的两条隶属来自既有事实「序数坐在自己的后继之内」，沿等式及其反向运输而得。

```agda
isPropPredOf : (σ : S) → isProp (Σ[ δ ∈ S ] IsPredOf σ δ)
isPropPredOf σ (δ , (ordδ , e)) (δ' , (ordδ' , e')) =
  Σ≡Prop (λ d → isProp× (isPropIsOrd d) (setIsSet (sucV d) σ))
    (ord-suc-inj δ δ' ordδ (e ∙ sym e'))
```

于是同一序数的任意两个前一层相等。第一分量由单射性一致，其余数据都是命题，故前一层组成的整个类型是命题。正是这一点使「仅仅存在的前一层」可当作确定的前一层使用：把截断展开到命题值的目标永远合法。

```agda
module _ (P : S → hProp (ℓ-suc ℓ)) where
```

最小层论证对每条序数性质同时只写一次：性质是参数，以下任何地方都不读入其内部。

```agda
  Carved : S → Type (ℓ-suc ℓ)
  Carved σ = Σ[ δ ∈ S ] (⟨ δ ∈ˢ σ ⟩ × ⟨ P (sucV δ) ⟩)
```

`σ` 处的一次雕出是论证所运行的数据：一个严格低于 `σ` 的序数 `δ`，其后继已携带该性质。若雕出仅仅存在，最小层就不可能远在 `δ` 之上，因为性质在 `sucV δ` 处已经成立。

```agda
  private
    below-case : (σ δ : S) → isLeastOrd P σ → IsOrd δ → ⟨ P (sucV δ) ⟩
               → ⟨ sucV δ ∈ˢ σ ⟩ → sucV δ ≡ σ
    below-case σ δ least ordδ m s∈σ =
      Empty.rec (least (sucV δ) (suc-ord ordδ) m s∈σ)
```

below 分支处理「后继仍严格低于最小层」的情形。极小性以反驳形式陈述，而本分支的假设恰是它的前提，故 `least` 先给出矛盾；`Empty.rec` 再把该矛盾消去成分支所欠的路径 `sucV δ ≡ σ`。

```agda
    same-case : (σ δ : S) → sucV δ ≡ σ → sucV δ ≡ σ
    same-case σ δ e = e
```

相等情形无须任何工作：交给该情形的恰是「后继与最小层等同」这件事本身。

```agda
    atCarve : (σ : S) → IsOrd σ → isLeastOrd P σ
            → Carved σ → Σ[ δ ∈ S ] IsPredOf σ δ
    atCarve σ ordσ least (δ , (δ∈σ , m)) = δ , (ordδ , suc≡σ)
```

`atCarve` 把一次雕出变成确定的前一层。见证 `δ` 被保留，其序数性由属于序数 `σ` 而恢复，而把 `sucV δ` 钉到 `σ` 上的等式正是那场情形分析的内容。

```agda
      where
      ordδ : IsOrd δ
      ordδ = mem-ord {A = σ} ordσ δ δ∈σ
```

`δ` 的序数性承继自序数 `σ`，因为序数的成员是序数。

```agda
      suc≡σ : sucV δ ≡ σ
      suc≡σ = Sum.rec (below-case σ δ least ordδ m) (same-case σ δ)
        (suc∈or≡ δ σ ordδ ordσ δ∈σ)
```

由 `δ ∈ σ` 出发，`suc∈or≡` 为其后继留下两种可能：仍严格低于 `σ`，或等于 `σ`。极小性排除前者，后者便给出所需等式。

```agda
  predOf : (σ : S) → IsOrd σ → isLeastOrd P σ → ∥ Carved σ ∥₁
         → Σ[ δ ∈ S ] IsPredOf σ δ
  predOf σ ordσ least = PT.rec (isPropPredOf σ) (atCarve σ ordσ least)
```

`predOf` 消费一个仅知其存在的雕出，返回前一层。截断的输入被消去到「前一层类型是命题」这一事实之中，因此从不在假想的雕出之间作选择；无论截断交出哪次雕出，答案都是同一个确定的前一层。

```agda
  carveAt : (σ z : S) → ⟨ z ∈ˢ Lset σ ⟩
          → ((δ : S) → ⟨ z ∈ˢ Lset (sucV δ) ⟩ → ⟨ P (sucV δ) ⟩)
          → ∥ Carved σ ∥₁
```

`carveAt` 从最小层的一个成员 `z` 造出雕出，配合的是这样一条观察：但凡 `z` 在某个后继层现身，性质便已在彼处成立。这正是进入塔之下降的形状：出现在某层，就是出现在某个更早层的可定义幂集之内，而由后继恒等式，每个可定义幂集都是一个后继层。

```agda
  carveAt σ z z∈Lσ k = PT.map
    (λ { (δ , (δ∈σ , z∈𝒟)) → δ , (δ∈σ
      , k δ (subst (λ w → ⟨ z ∈ˢ w ⟩) (sym (Lset-suc δ)) z∈𝒟)) })
    (Lset-out σ z z∈Lσ)
```

塔以截断的方式分解 `z` 的隶属：给出某个低于 `σ` 的层 `δ`，使 `z` 落在 `Lset δ` 的可定义幂集之内。映射只在截断内部进行：后继恒等式反向读取，把 `z` 从 `𝒟ₒ (Lset δ)` 搬到 `Lset (sucV δ)`，观察 `k` 在该后继处触发，所得的雕出被重新注入截断。

## 一层装下一个集合以下的一切

本节用层的传递性与序数上界，得到一个同时包含集合的成员、成员的成员以及极限层 `ω` 的层。

构造还需要另一样东西：一个上界，而取得它不牵涉任何比较。层传递，故一个集合的层已经装着该集合的诸成员，以及其后它们的诸成员；最早的层与别的层无异，故它就够用。

还需确定一个包含塔的极限层的序数。前方的比较以对象语言书写，而各元数的无常元公式 `Formula ⊥* n` 的码都属于 `Lset ω`；这样的码可以带有自由变量，因此它们是公式，而非句子。后继层中一个成员的完整名字所说的多于它的码：它还要指名元数，以及取自更早层的参数向量。这里造出的界覆盖码，因为 `ω ∈ β` 加上单调性把 `Lset ω` 抬进 `Lset β`；参数低于界则另有原因，下一条事实记录的正是它：集合的成员与成员的成员落在同一层中。

```agda
stage-below : (a : S) (p : ⟨ isL a ⟩) (x : S) → ⟨ x ∈ˢ a ⟩
            → ⟨ x ∈ˢ Lset (stage a p) ⟩
stage-below a p x x∈a =
  layer-trans (Lset-layer (stage a p)) x∈a (stage-mem a p)
```

层传递，而 `a` 的最早层也是一个层。故 `a` 的成员 `x` 落在塔在 `a` 自身层处的层里：传递性把隶属从集合搬进容纳该集合的那一层。

```agda
stage-below₂ : (a : S) (p : ⟨ isL a ⟩) (x y : S) → ⟨ y ∈ˢ x ⟩ → ⟨ x ∈ˢ a ⟩
             → ⟨ y ∈ˢ Lset (stage a p) ⟩
stage-below₂ a p x y y∈x x∈a =
  layer-trans (Lset-layer (stage a p)) y∈x (stage-below a p x x∈a)
```

传递性应用两次即可下探两层：`a` 的成员的成员落在同一层里，因为它属于 `x`，而 `x` 属于那一层。

```agda
stageBound : (a : S) (p : ⟨ isL a ⟩)
           → Σ[ β ∈ S ] (IsOrd β × ⟨ ω ∈ˢ β ⟩ × ⟨ stage a p ∈ˢ β ⟩)
stageBound a p = bound2 ω (stage a p) ω-ord (stage-ord a p)
```

必须被支配的两个序数是极限层 `ω` 与该集合自身的最早层；`bound2` 返回一个同时高于两者的序数，并附带其序数性证书。

```agda
bound-below₂ : (a : S) (p : ⟨ isL a ⟩) (x y : S) → ⟨ y ∈ˢ x ⟩ → ⟨ x ∈ˢ a ⟩
             → ⟨ y ∈ˢ Lset (stageBound a p .fst) ⟩
bound-below₂ a p x y y∈x x∈a =
  Lset-mono (stageBound a p .snd .snd .snd) (stage-below₂ a p x y y∈x x∈a)
```

塔的单调性把「下探两层」的事实从最早层提升到界序数的层。现在这一层同时容纳 `a`、它的成员、成员的成员，以及比较所要读取的公式码。

## 小结

本章可复用的结果，是最小层为后继时的唯一前一层，以及足以承载选择构造的上界序数。最小层引理是带条件的，而条件正是它的内容。对以 `σ` 为最小层的某条序数性质而言，性质完全可能恰在零序数处首次成立，此时其下无可雕出之物。当 `σ` 处的雕出仅仅存在，即有低于 `σ` 的序数使其后继已具该性质时，`carveAt` 产出雕出，`predOf` 按 `isPropPredOf` 闭合截断，把它化为唯一的前一层；而 `ord-suc-inj` 正是「后继决定它所后继者」的理由。`stageBound` 给出上界序数：它在一个集合自身的层之上，从而在其成员及其成员之上，也在塔的极限层之上，而公式码恰在那里。