L 中的幂集

可以直接阅读本章，也可以通过阅读指南和依赖地图选择其他路线。

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

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

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

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

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 经四条路径进入证明：命题降级、外围幂集所需的小分类器、典范层函数，以及完整分离所用的反射。这里没有引入其他经典假设。

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

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

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 α 及其严格单调性：若 α ∈ β，早期层中的成员可提升到后期层。对每个可构造候选，层函数给出一个典范序数索引，其对应层包含该候选；上界引理再把这一小族序数索引严格界于同一个序数之下。层函数还证明最小性，但本章只使用序数性与层成员这两条事实。

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。

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

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

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 ℓ。因此后面的大小问题针对索引类型，不针对模型载体。

open hPropStructure 𝒮ʟ

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

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

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

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

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

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 只遍历可构造模型元素。该公式是 Δ₀，尽管后面的证明把它交给一般的分离接口。

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 并不是模型中最终返回的幂集。

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 之间的等价。这只改变真值所在的宇宙层级，既不消去命题截断，也不选定任何序数层。

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

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

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

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

  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，不用其最小性。

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

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

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

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

  β : V ℓ
  β = b .fst

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

  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 为什么存在并具有所需性质。

  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。这是由唯一性许可的截断消去，不是选择公理的应用。

    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 的结论。

    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 再把可缩包运输到幂集字段所需的谓词上。

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 ℓ) 经命题降级、小分类器、从命题截断的可构造性中选出典范层，以及完整分离所用的反射，传递到这一构造。

  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 ℓ) 分别支持小分类器、命题降级、典范层构造与完整分离所用的公式反射。本证明不使用任何形式的选择、替换字段或凝聚。