---
title: "L 中的幂集"
module: L.Axioms.Power
lang: zh
site: "Bedrock"
description: "L 中的幂集"
stage: "可构造层与公理"
reading_order: 36
canonical: https://bedrock.institute/zh/L.Axioms.Power.html
html: L.Axioms.Power.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/Axioms/Power.lagda.md
prerequisites: [Base.Prelude, Base.Classical, Base.Impredicativity, FOL.ZFStructure, FOL.Syntax, FOL.Absoluteness, FOL.ZFModel, V.Hierarchy, V.Model, L.Constructible, L.Ordinal, L.Stage, L.Axioms.Basic, L.Axioms.Full]
routes: [constructible-axioms]
translations: [https://bedrock.institute/en/L.Axioms.Power.md, https://bedrock.institute/ja/L.Axioms.Power.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
# L 中的幂集

对可构造集 `a`，`L` 内的幂集究竟应当收集什么？模型的量词遍历其载体 `S`，所以所求幂集的成员是满足内部包含 `x ⊆ˢ a` 的可构造模型元素 `x`。外围层级能对底层集 `A = fst a` 构造幂集，但其成员条件遍历整个`V ℓ`，不附加可构造性要求。因此，这个外围幂集可以提供索引，却不能直接作为`L` 内的幂集返回。

证明分三步进行。先由外围幂集取得全部候选者的小表现，再保留其中呈现可构造候选者的索引，并用同一个序数 `β` 界住它们的诸层；最后在 `Lset β` 中作分离，恰好收集内部包含于`a` 的模型元素。宿主层的构造负责给出上界；最终的集合本身则在可构造模型中形成。

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

构造需要两种小性。命题降级把模型真值层级上的命题换成小索引层级上的等价命题；非直谓性包还为小命题提供一个小分类器，使外围层级能够构成幂集。两者都由排中律推出，却解决不同的大小问题：命题降级使可构造性能够进入小索引类型，分类器则构造提供这些索引的外围幂集。

```agda
open import Base.Prelude
open import Base.Classical using ( LEM; lem→resizing; lem→impredicativity )
open import Base.Impredicativity using ( module Impredicativity )
```

固定宇宙层级 `ℓ` 与唯一的假设 `lem : LEM (ℓ-suc ℓ)`。目标模型字段断言：对 `L` 中每个 `a`，恰有一个模型元素，其成员正是内部包含于 `a` 的模型元素。唯一性由宿主类型 `isContr` 打包；对象理论内容是幂集公理，而唯一性来自外延性。同一个 `lem` 经四条路径进入证明：命题降级、外围幂集所需的小分类器、典范层函数，以及完整分离所用的反射。这里没有引入其他经典假设。

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

证明同时涉及三个层面。宿主类型组织索引与证明；外围结构 `𝒮ᵥ` 的元素是累积层级中的全部集合；限制结构 `𝒮ʟ` 的元素则是外围集合与其可构造性证据组成的对。公式语言提供在 `𝒮ʟ` 内表达包含关系所需的有界全称量词。因此，外围结构可以枚举可能的子集，而对象理论的幂集公理必须在限制结构中成立。

```agda
open import FOL.ZFStructure using ( module hPropStructure )
open import FOL.Syntax using ( Formula; var; con; _∈̇_; ∀̇∈ )
import FOL.Absoluteness
import FOL.ZFModel
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ )
```

外围层级给出集合 `𝒫V A`，它包含 `A` 的每个外围子集，并带有相应的隶属规格。可构造层级给出诸层 `Lset α` 及其严格单调性：若 `α ∈ β`，早期层中的成员可提升到后期层。对每个可构造候选，层函数给出一个典范序数索引，其对应层包含该候选；上界引理再把这一小族序数索引严格界于同一个序数之下。层函数还证明最小性，但本章只使用序数性与层成员这两条事实。

```agda
open import V.Model {ℓ} using ( module Power )
open import L.Constructible {ℓ}
  using ( 𝒮ʟ; isL; isL-trans; IsOrd; Lset; Lset-mono )
open import L.Ordinal {ℓ} using ( boundingOrd )
open import L.Stage {ℓ} lem using ( stage; stage-ord; stage-mem )
```

得到序数上界 `β` 后，`LsetS β oβ` 是一个模型元素，并且已知它包含所有正在考虑的内部子集。因此，余下的数学操作是按一元包含公式作分离。通用定理 `hasSeparationL`接受任意公式：它先找到反射层，在该层上用公式的有界相对化取代原公式，再应用有界分离。本章的公式本来就是 Δ₀，但这次调用仍经由上述通用路径。因而，即使在这个有界特例中，公式反射以及为参数构造层的步骤，也确实使用了同一个 `lem`。

```agda
open import L.Axioms.Basic {ℓ} using ( LsetS )
open import L.Axioms.Full {ℓ} lem using ( hasSeparationL )
```

层级中的每个集合都有小表现：索引类型 `⟪P⟫` 与呈现其成员的嵌入 `⟪P⟫↪`。属于 `P` 被定义为该嵌入某个纤维的命题截断。由于此映射是嵌入，每个纤维本来就是命题，故 `∈-asFiber` 可以恢复索引及识别它的路径，而无须使用选择公理。等价的两个方向还让证明在降级命题与原命题之间往返。最后，命题外延性把两个方向的蕴含变成真值之间的路径。

```agda
open import Cubical.Foundations.Equiv using ( _≃_; invEq; equivFun )
open import Cubical.Functions.Logic using ( ⇔toPath )
open import Cubical.HITs.CumulativeHierarchy.Base using ( V; _∈_ )
open import Cubical.HITs.CumulativeHierarchy.Properties
  using ( ∈-asFiber; ⟪_⟫; ⟪_⟫↪ )
```

打开 `𝒮ʟ` 后，下文无修饰的载体 `S` 与隶属关系都指可构造模型。`S` 的元素由一个可构造集合及其可构造性证据组成；`fst` 忘去证据，返回对应的外围集合。参数 `ℓ` 控制 `⟪P⟫` 一类小表现类型，而 `V ℓ`、载体 `S` 与两套结构的真值都位于 `ℓ-suc ℓ`。因此后面的大小问题针对索引类型，不针对模型载体。

```agda
open hPropStructure 𝒮ʟ
```

两个模型接口给出记号相同而量化域不同的两种子集关系。在 `ModelL` 中，`x ⊆ˢ a` 量化 `S`，所以只检验可构造元素；在 `ModelV` 中，对应关系量化 `V ℓ` 中的每个集合。对任意左端而言，后一条件更强。若左端本身可构造，则 `L` 的传递性把它的每个外围成员变成 `S` 的元素，从而给出下文所用的精确桥梁：把内部包含提升为外围包含。

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

这里的记号 `_⊨_` 是载体 `S` 上公式的内层满足关系，公式在限制结构 `𝒮ʟ` 中求值。常元表示它所指名的模型元素，而限制结构的隶属关系在外围层级中读取这些元素的第一投影。同一模块也提供外层读法，但本章没有应用绝对性定理；此处唯一使用的满足陈述，只是有界包含公式在模型内部的直接含义。

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

外围幂集构造以 `lem→impredicativity lem` 给出的小分类器实例化。这里仅使用 `hPropSmallness` 分量：特征函数被表示为一个取值于小真值码类型的函数，再由此形成层级中的集合。对 `isL` 作命题降级是另一项独立操作，并不进入这次实例化。区分这两种作用，才能看清稍后的小索引是怎样形成的。

```agda
module Pow = Power (Impredicativity.hPropSmallness (lem→impredicativity lem))
```

## 作为公式的条件

对 `a : S`，公式 `subFo a` 留有一个自由槽位给候选 `x`，读作

「对每个 `y ∈ x`，都有 `y ∈ a`」。

`var zero` 的两次出现位于不同语境。有界全称量词之外的那个表示候选 `x`，量词主体中的那个表示新束缚的成员 `y`。常元域就是模型载体，所以 `con a` 可以直接指名 `a`。在环境 `x ∷ []` 中，有界全称的语义直接化归为 `x ⊆ˢ a`。这是内部包含，其中 `y` 只遍历可构造模型元素。该公式是 Δ₀，尽管后面的证明把它交给一般的分离接口。

```agda
subFo : S → Formula S 1
subFo a = ∀̇∈ (var zero) (var zero ∈̇ con a)
```

## 界住诸可构造子集

固定 `a : S`。它的第一投影 `A` 是忘去可构造性证据后，在外围层级中看到的同一个集合。集合 `P = Pow.𝒫V A` 满足完整的外围幂集规格：属于 `P` 只要求在外围意义下包含于 `A`，不带可构造性前提。因此，若有不可构造的外围子集，`P` 也会收纳它们。而且，这个构造没有给出`P` 本身可构造的证明。本证明只使用小表现 `⟪P⟫`，随后以可构造性筛选其索引；`P` 并不是模型中最终返回的幂集。

```agda
module Bound (a : S) where
  private
    A P : V ℓ
    A = fst a
    P = Pow.𝒫V A
```

对外围集合 `v`，可构造性 `isL v` 是层级 `ℓ-suc ℓ` 上的命题；具体而言，它是「存在一个包含 `v` 的序数层」这一存在式的命题截断。这个命题太大，不能充当层级 `ℓ` 上类型的第二分量。因此，`rsz` 选出小命题 `Q : hProp ℓ`，并给出其底层类型与 `isL v` 之间的等价。这只改变真值所在的宇宙层级，既不消去命题截断，也不选定任何序数层。

```agda
    rsz : (v : V ℓ) → Σ[ Q ∈ hProp ℓ ] (⟨ isL v ⟩ ≃ ⟨ Q ⟩)
    rsz v = lem→resizing lem (isL v)
```

宿主类型 `Ix` 恰好索引外围幂集中的可构造成员。它的元素由两部分组成：一个索引 `m : ⟪P⟫`，呈现 `A` 的某个外围子集；以及该被呈现集合之降级后可构造性命题的证明。两个分量都是小的，所以 `Ix : Type ℓ`，序数上界引理可以对它量化。`Ix` 只是宿主层的索引类型，既不是 `L` 的元素，也不是对象语言公式定义的类，更不会成为最终的幂集。

```agda
  Ix : Type ℓ
  Ix = Σ[ m ∈ ⟪ P ⟫ ] ⟨ rsz (⟪ P ⟫↪ m) .fst ⟩
```

要为 `i : Ix` 找到一个层，证明先恢复原来的可构造性命题。降级等价的逆向映射把 `i.snd` 从小命题送回 `isL (⟪P⟫↪ i.fst)`。所得结论仍只在命题截断下断言：某个序数层包含该被呈现集合。因此，`unres` 只逆转宇宙层级的改变，并未从截断中抽取见证；取得确定层索引所需的额外工作由下一个定义完成。

```agda
  private
    unres : (i : Ix) → ⟨ isL (⟪ P ⟫↪ (i .fst)) ⟩
    unres i = invEq (rsz (⟪ P ⟫↪ (i .fst)) .snd) (i .snd)
```

函数 `stg` 为 `Ix` 的每个条目指定典范层索引，即使被呈现集合属于 `Lset σ` 的最小序数 `σ`。这是与命题降级不同的另一处经典步骤。在内部，`stage` 作良基下降，并用排中律判定是否存在更小的见证。命题截断只被消去到 `LeastOrd`；该类型的命题性由序数三歧与其余证据的唯一性证明。因此，所得结果是一个确定的序数索引，却没有提供从任意截断见证中抽取数据的一般规则。本章只使用 `stage-ord` 与 `stage-mem`，不用其最小性。

```agda
    stg : Ix → V ℓ
    stg i = stage (⟪ P ⟫↪ (i .fst)) (unres i)
```

此时 `stg : Ix → V ℓ` 是真正的小族，而 `stage-ord` 证明每个取值都是序数。引理 `boundingOrd` 返回显式数据：一个序数 `β`，以及每个 `stg i` 都属于 `β` 的证明。其构造在宿主理论中完成，先取给定诸序数的后继，再对它们取并。这不是在 `L` 内应用替换，本章任何地方都没有使用替换字段。所得严格上界恰是稍后 `Lset-mono` 所要求的形式。

```agda
    b = boundingOrd Ix stg (λ i → stage-ord (⟪ P ⟫↪ (i .fst)) (unres i))
```

上界数据的第一投影记作 `β`。它是在宿主层构造出的外围层级集合，随后的证明表明它是序数。稍后被包装为模型元素的是层 `Lset β`，即 `LsetS β oβ`；本证明不需要把 `β` 自身包装进模型。此外，`β` 依赖 `A` 的全部可构造外围子集之层，而不只依赖 `a` 自己所在的层。这样一个随整个候选族而定的上界已经足以证明幂集公理，因此不需要凝聚给出的精细估计。

```agda
  β : V ℓ
  β = b .fst
```

证明 `oβ` 记录上界是序数。`b.snd` 的另一分量稍后写作 `b.snd.snd i`，它对每个 `i : Ix` 断言 `stg i ∈ β`。这是序数索引之间的严格隶属。给定 `stage-mem : presented-set ∈ Lset (stg i)`，`Lset-mono` 恰好利用这条隶属把被呈现集合提升到 `Lset β`。序数性与严格上界性质，就是后续对 `β` 所需的两项事实。

```agda
  oβ : IsOrd β
  oβ = b .snd .fst
```

引理 `below` 陈述上界的关键覆盖性质：若 `x : S` 内部包含于 `a`，则其底层外围集合 `fst x` 属于 `Lset β`。证明先把 `fst x` 认同为 `P` 的某个小索引 `i : Ix` 所呈现的成员。由 `stage-mem`，该候选属于 `Lset (stg i)`；再由 `stg i ∈ β`，`Lset-mono` 把这条隶属提升到 `Lset β`。最后的 `subst` 沿呈现路径把结论搬到 `fst x`。下面的局部定义说明这个特定索引 `i` 为什么存在并具有所需性质。

```agda
  below : (x : S) → ⟨ x ⊆ˢ a ⟩ → ⟨ fst x ∈ Lset β ⟩
  below x x⊆a =
    subst (λ w → ⟨ w ∈ Lset β ⟩) pa
      (Lset-mono {α = β} {β = stg i} (b .snd .snd i) (stage-mem _ (unres i)))
    where
```

为取得索引，先把内部包含转成外围包含。任取外围成员 `v ∈ fst x`，可构造性的传递性从 `x.snd` 推出 `isL v`；于是对 `(v , proof)` 这个模型元素应用 `x⊆a`，便得 `v ∈ A`。因此 `fst x` 是 `A` 的外围子集，而 `Pow.power-spec` 的逆向把这条包含变成 `fst x ∈ P`。`P` 的隶属是表现纤维的命题截断，但表现映射是嵌入，所以该纤维本身是命题。因此，`∈-asFiber` 可以返回实际的表现索引及路径 `pa`，后者把其像认同为 `fst x`。这是由唯一性许可的截断消去，不是选择公理的应用。

```agda
    vsub : ⟨ ModelV._⊆ˢ_ (fst x) A ⟩
    vsub v v∈ = x⊆a (v , isL-trans {x = fst x} {y = v} v∈ (x .snd)) v∈
    fib = ∈-asFiber {a = fst x} {b = P}
            (subst ⟨_⟩ (sym (Pow.power-spec A (fst x))) vsub)
    pa : ⟪ P ⟫↪ (fib .fst) ≡ fst x
```

路径 `pa` 把恢复出的表现索引补全为 `Ix` 的元素。第一分量是 `fib.fst`。为构造第二分量，先沿 `sym pa` 把 `x.snd : isL (fst x)` 搬到该索引所呈现集合的可构造性，再用降级等价的正向映射把这个命题编码到层级 `ℓ`。因此，`i` 确实索引与 `x` 底层集合相同的候选，其层也属于被 `β` 界住的族。把 `stage-mem`、`b.snd.snd i` 与 `Lset-mono` 组合起来，再沿 `pa` 运输，就得到 `below` 的结论。

```agda
    pa = fib .snd
    i : Ix
    i = fib .fst
      , equivFun (rsz (⟪ P ⟫↪ (fib .fst)) .snd)
          (subst (λ w → ⟨ isL w ⟩) (sym pa) (x .snd))
```

## 字段

`hasPowerL` 的类型就是要证明的精确模型论陈述。它要求由实现者 `p : S` 组成的类型可缩，而对每个 `x : S`，`p` 的成员谓词都是 `x ⊆ˢ a`。此时外围集合 `P` 已完成它的作用：它提供了用于构造 `Bound.β a` 的索引族，却不出现在结论中。

先把 `hasSeparationL` 应用于模型元素`LsetS (Bound.β a) (Bound.oβ a)`，就得到一个可缩的 `SetOf`，它实现的谓词看上去更强：`x` 属于该层，并且满足 `subFo a`。余下只须证这个谓词等于内部包含。局部等式 `Q≡`给出这个识别，最外层的 `subst` 再把可缩包运输到幂集字段所需的谓词上。

```agda
hasPowerL : (a : S) → isContr (SetOf (λ x → x ⊆ˢ a))
hasPowerL a =
  subst (λ Q → isContr (SetOf Q)) Q≡
    (hasSeparationL (LsetS (Bound.β a) (Bound.oβ a)) (subFo a))
  where
```

余下的等式比较分离切出的类与幂集字段要求的类。左端说 `x` 属于作为上界的层，并且 `x` 满足 `subFo a`；后一个满足命题化为内部包含 `x ⊆ˢ a`。正向证明因而舍去层成员这一分量。反向证明则由 `x ⊆ˢ a` 应用 `Bound.below` 补出该分量。命题外延性把两个方向的蕴含变成每个 `x` 处的路径，函数外延性再把这些路径合成为谓词等式 `Q≡`。最外层的 `subst` 沿这个等式运输分离所得的可缩实现者类型。`Q≡` 本身不使用集合外延性；分离所打包的一意性已经用过集合外延性。

因此，`hasPowerL a` 以精确的模型论形式证明对象理论的幂集公理。它给出由元素 `p : S` 组成的可缩类型，并且对每个 `x : S`，成员命题 `x ∈ˢ p` 恰与内部陈述 `x ⊆ˢ a` 等价。`p` 与每个候选 `x` 都量化于可构造模型的载体。此前使用的宿主层幂集只提供候选者的小索引，并不是此处得到的集合。唯一的假设 `LEM (ℓ-suc ℓ)` 经命题降级、小分类器、从命题截断的可构造性中选出典范层，以及完整分离所用的反射，传递到这一构造。

```agda
  Q≡ : (λ x → (x ∈ˢ LsetS (Bound.β a) (Bound.oβ a)) ⊓ ((x ∷ []) ⊨ subFo a))
     ≡ (λ x → x ⊆ˢ a)
  Q≡ = funExt (λ x → ⇔toPath
    (λ { (_ , x⊆a) → x⊆a })
    (λ x⊆a → Bound.below a x x⊆a , x⊆a))
```

## 小结

这个构造中的三种作用彼此分明：外围幂集提供小表现，宿主理论界住其可构造成员的诸层，内部分离则从该上界中切出所求集合。`L.Model` 把 `hasPowerL` 装入 `L⊨ZF` 的 `hasPower`字段，随后由这个 record 定义内部运算 `𝒫`。后续 GCH 论证使用此运算与规格`℩-spec (hasPower κ)`，在成员关系与内部包含之间往返；它们从不使用辅助的外围 `Pow.𝒫V`。

逻辑依赖也可以精确列清。唯一的假设 `LEM (ℓ-suc ℓ)` 分别支持小分类器、命题降级、典范层构造与完整分离所用的公式反射。本证明不使用任何形式的选择、替换字段或凝聚。