---
title: "传递良基关系的塌缩"
module: L.Mostowski
lang: zh
site: "Bedrock"
description: "传递良基关系的塌缩"
stage: "序数、单射与基数"
reading_order: 95
canonical: https://bedrock.institute/zh/L.Mostowski.html
html: L.Mostowski.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/Mostowski.lagda.md
prerequisites: [Base.Prelude, FOL.ZFStructure, V.Hierarchy, L.Constructible]
routes: [cardinal-tools]
translations: [https://bedrock.institute/en/L.Mostowski.md, https://bedrock.institute/ja/L.Mostowski.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
# 传递良基关系的塌缩

一个关系自身能携带多少集合论结构？取带良基传递关系 `_≺_` 的小类型 `A`，该关系取值于 `Type ℓ`。Mostowski 的回答是：仅凭这个关系，就能用递归确定一个函数 `col : A → SV.S`，满足

`col p = { col r | r ≺ p }`，

即每个点被送到其前驱的塌缩值所成的集合。一条计算律刻画每个值中的隶属关系，而关系的传递性使每个塌缩值成为这里所说的序数，即自身传递且每个成员也传递。

一个有限的例子可以展示机制。取三点 `s`、`r`、`p`，有 `s ≺ r`、`r ≺ p`，以及传递性所要求的 `s ≺ p`，且无其他关系。递归没有强制 `col s` 的任何成员，`col r = { col s }`，`col p = { col s, col r }`，这正是 von Neumann 的 `0`、`1`、`2` 图景。递归从不检视点本身，只检视它们的前驱锥。

设定的三个特征决定其后的一切。其一，`A` 与每个纤维 `x ≺ y` 都在 `Type ℓ` 中，故对每个 `p`，前驱锥是小类型 `Σ[ r ∈ A ] (r ≺ p)`；层级 `V` 的 `sett` 构造子恰好把这样的小族变成 `SV.S` 中的集合。其二，`sett` 集合中的隶属按构造就是命题截断：`⟨ b ∈ˢ a ⟩` 说的是纯粹存在该族的某个索引，使族在该处的值等于 `b`，而非选定的索引可得。因此本章在一个方向上从给出的数据证明隶属 (`r ≺ p` 给出 `col r ∈ˢ col p`)，在另一方向上只得到纯粹存在的前驱加一条塌缩值等式。其三，之后消去的目标都是命题，如集合间的等式或 `isTransV x`，故向它们消去截断是合法的。这里没有对 `_≺_` 的外延性假设，前驱锥相同的两点不被区分：塌缩是典范的，但并不声称单射。整个构造只用良基递归与传输；这里没有假设任何经典原理。

塌缩落在累积层级的集合层载体中，因此其输出由真正的集合构成，而非 `A` 的点。该载体在下文记作 `SV.S`；它是 h-集合，也就是任意两元素之间的相等类型都是命题。其成员关系 `_∈ˢ_` 把每条隶属陈述打包成一个 `hProp`：底层类型 `⟨ b ∈ˢ a ⟩` 连同该类型为命题的证明。因此，隶属与传递性都可以直接用层级自身的关系陈述。

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

open import Base.Prelude

module L.Mostowski {ℓ : Level} where

open import FOL.ZFStructure using ( module hPropStructure )
```

构造由两个要素驱动。其一是层级的像运算 `sett`：从小索引类型 `X` 和族 `X → V ℓ` 造出该族取值的集合，隶属仅在某个索引命中目标时纯粹地成立。其二是良基性证书 `WellFounded _≺_`，即 `A` 的每个元素沿 `≺` 可及；其归纳原理构造递归定义的函数，配套的计算律记录该函数在每点的行为。命题截断经由 `∥ _ ∥₁` 与其引入 `∣ _ ∣₁` 进入，因为像中的隶属按设计就是截断的。序数目标 `IsOrd`、传递性 `isTransV` 及其命题性证明 `isPropIsTransV` 来自 `L` 的构造，只在最后定理需要它们时出现。

```agda
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ )
open import L.Constructible {ℓ} using ( IsOrd; isTransV; isPropIsTransV )

open import Cubical.HITs.CumulativeHierarchy.Base using ( sett )
open import Cubical.Induction.WellFounded using ( WellFounded; module WFI )
import Cubical.HITs.PropositionalTruncation as PT
```

层级结构的等词与隶属关系取值于层级 `ℓ-suc ℓ` 的 `hProp`。另一方面，`A` 与每个纤维 `x ≺ y` 都在 `Type ℓ` 中，所以每个前驱锥都是可供 `sett` 使用的小索引类型。构造只需要这些大小事实，不需要排中律。

```agda
open PT using ( ∣_∣₁; ∥_∥₁ )

module SV = hPropStructure 𝒮ᵥ
open SV using ( _∈ˢ_ )
```

下面完成两个任务。首先证明塌缩的两条隶属律：给定一个前驱即可构造相应成员，而从一个成员反推时，只能得到纯粹存在的前驱及其塌缩值等式。随后在良基归纳中使用这两条定律，证明每个 `p` 都满足 `IsOrd (col p)`。显式输入与截断输出之间的不对称在两步中都不可省略。

良基性为递归提供依据。由 `wf` 得到的归纳原理说：要在 `A` 上定义一族 `P`，只需对每个 `p`，从所有前驱 `r ≺ p` 处 `P` 的值构造 `P p`。传递性见证 `≺-trans` 不参与 `col` 的定义；它在随后证明所得集合传递时才使用。

```agda
module Mostowski (A : Type ℓ) (_≺_ : A → A → Type ℓ)
                 (wf : WellFounded _≺_)
                 (≺-trans : {x y z : A} → x ≺ y → y ≺ z → x ≺ z) where

  module W = WFI wf using ( induction; induction-compute )

  colStep : (p : A) → (∀ r → r ≺ p → SV.S) → SV.S
```

递归步就是前驱锥的像。给定 `p` 和已经知道每个 `r ≺ p` 的 `col r` 的递归调用 `rec`，该步造出 `sett (Σ[ r ∈ A ] (r ≺ p)) (λ z → rec (fst z) (snd z))`：索引类型是偶对 `(r , r ≺ p)` 的全空间，族把这样的偶对送到 `rec r`。抽象地说，这正是本章宣告的塌缩方程 `{ col r | r ≺ p }`。注意步型对任意的步函数 `rec` 做了量化，这使同一份数据既用于定义，也经由下面的计算律用于推理。

```agda
  colStep p rec = sett (Σ[ r ∈ A ] (r ≺ p)) (λ z → rec (fst z) (snd z))

  opaque
    col : A → SV.S
    col = W.induction {P = λ _ → SV.S} colStep

    col-eq : (p : A) → col p ≡ sett (Σ[ r ∈ A ] (r ≺ p)) (λ z → col (fst z))
```

函数 `col` 由良基归纳定义。其计算律 `col-eq` 把 `col p` 等同于前驱锥在 `col` 下的像。随后的隶属证明用这条等式在递归定义的值与显式像之间转换，而在显式像中，隶属具有 `sett` 给出的截断原像分类。

```agda
    col-eq = W.induction-compute colStep

  col-in : (p r : A) → r ≺ p → ⟨ col r ∈ˢ col p ⟩
  col-in p r rp =
    subst (λ v → ⟨ col r ∈ˢ v ⟩) (sym (col-eq p)) ∣ (r , rp) , refl ∣₁

  col-out : (p : A) (b : SV.S) → ⟨ b ∈ˢ col p ⟩
```

隶属在两个方向上各有一条计算律，且两者有意味深长的不对称。正向：若给定 `r ≺ p`，则 `col r` 是 `col p` 的成员。其见证是偶对 `(r , rp)` 连同记录 `col r` 在索引 `r` 处被命中的路径 `refl`；沿 `col-eq p` 传输 (取 `sym` 形式，因为方程是按另一方向证明的) 把这个显式像的成员移入类型 `⟨ col r ∈ˢ col p ⟩`。反向：任意的隶属 `⟨ b ∈ˢ col p ⟩` 只给出截断的陈述：纯粹地存在某个 `r ≺ p` 使 `col r ≡ b`。证明沿 `col-eq p` 把隶属传输回显式像中的隶属；该隶属按构造就是截断的原像，再把索引数据改写为带等式的前驱。这里没有任何一步选定具体的 `r`；截断 `∥ _ ∥₁` 忠实记录了隶属所能揭示的信息。

```agda
          → ∥ Σ[ r ∈ A ] ((r ≺ p) × (col r ≡ b)) ∥₁
  col-out p b b∈ =
    PT.map (λ z → fst (fst z) , snd (fst z) , snd z)
      (subst (λ v → ⟨ b ∈ˢ v ⟩) (col-eq p) b∈)

  col-ord : (p : A) → IsOrd (col p)
```

最后的定理说每个塌缩值都是序数，其中 `IsOrd (col p)` 展开为一对：`col p` 传递，且其每个成员都传递。证明对 `p` 做良基归纳，故归纳假设 `rec` 对每个前驱 `r ≺ p` 提供 `IsOrd (col r)`，目标由其两个分量组装。这是假设 `≺-trans` 发挥作用的地方；在阅读两个子句之前，先想象三点链 `s ≺ r ≺ p`：关系的传递性正是让关于 `col r` 的隶属事实能在 `col p` 内重演的关键。

```agda
  col-ord = W.induction {P = λ p → IsOrd (col p)} ih
    where
    ih : (p : A) → (∀ r → r ≺ p → IsOrd (col r)) → IsOrd (col p)
    ih p rec = tr , mem
      where
```

第一个子句说 `col p` 的每个成员都传递。证明从 `col-out p x x∈` 出发：成员 `x` 是某个纯粹存在的前驱 `r ≺ p` 的 `col r`，并带等式 `e : col r ≡ x`。归纳假设提供 `isTransV (col r)`，`subst isTransV e` 沿该等式把这一证明传送到类型 `isTransV x`。截断消去合法，因为目标 `isTransV x` 是命题，由 `isPropIsTransV x` 证明；这里没有抽取见证，只是从纯粹存在的情形分析中确立一个命题。

```agda
      mem : (x : SV.S) → ⟨ x ∈ˢ col p ⟩ → isTransV x
      mem x x∈ = PT.rec (isPropIsTransV x)
        (λ z → subst isTransV (snd (snd z)) (rec (fst z) (fst (snd z)) .fst))
        (col-out p x x∈)
      tr : isTransV (col p)
```

第二个子句证明 `col p` 自身传递：给定 `y ∈ x` 与 `x ∈ col p`，要证 `y ∈ col p`。先把 `x ∈ col p` 经 `col-out` 剥开，纯粹地得到某个 `r ≺ p` 使 `col r ≡ x`。该等式把已给的 `y ∈ x` 传输入 `⟨ y ∈ˢ col r ⟩`，运行示例中的中间环节 `r` 正是在这里把链条两端接了起来。

```agda
      tr {x} {y} y∈x x∈col = PT.rec (snd (y ∈ˢ col p)) outer (col-out p x x∈col)
        where
        outer : Σ[ r ∈ A ] ((r ≺ p) × (col r ≡ x)) → ⟨ y ∈ˢ col p ⟩
        outer (r , rp , e) =
          PT.rec (snd (y ∈ˢ col p)) inner
```

现在链条闭合。从 `y ∈ col r` 出发，在 `r` 处应用 `col-out` 纯粹地给出某个 `s ≺ r` 使 `col s ≡ y`；记其等式为 `e2`。关系传递性把 `s ≺ r` 与 `r ≺ p` 复合成 `s ≺ p`，`col-in p s` 把 `col s` 提升为 `col p` 的成员。最后沿 `e2` 用 `subst` 在隶属目标中把 `col s` 换成 `y`，得到 `⟨ y ∈ˢ col p ⟩`。两次截断消去都落在命题 `⟨ y ∈ˢ col p ⟩` 中，整个论证只用良基递归、传输和传递性假设：本章任何地方都没有经典原理进入。

```agda
            (col-out r y (subst (λ v → ⟨ y ∈ˢ v ⟩) (sym e) y∈x))
          where
          inner : Σ[ s ∈ A ] ((s ≺ r) × (col s ≡ y)) → ⟨ y ∈ˢ col p ⟩
          inner (s , sr , e2) =
            subst (λ v → ⟨ v ∈ˢ col p ⟩) e2 (col-in p s (≺-trans sr rp))
```