The power set in L

L 的集合在 L 之内取的幂集，是它可构造子集之集，而这正是模型那个字段所索取的：它所量化的包含关系跑遍模型自己的载体，故不可构造的子集根本不是候选。任务是把可构造的那些收集起来。

论证是先界住、再雕出，与它之前诸公理所用的是同样两步。一个集合的每个子集都是层级幂集的成员，而后者由小类型索引；其中可构造的那些也构成小族，故它们的阶段有公共上界，而每个可构造子集都现身于其下。用「此物的每个成员都是 a 的成员」这条公式雕出那个阶段，得到的恰是诸可构造子集，因为那个上界使条件中隶属的那一半自动成立。

有两件事使证明变短。L 中的分离如今接受任意公式，故那个条件可以照它读起来的样子写。而层级幂集所需的小性、与「把一条无界的可构造性陈述降层」所需的小性，是本书早已从排中律赎回的那个非直谓性打包的两半：没有新原则进场，也没有新层级的排中律进场；后者值得核对而非假定，因为那两半相隔一个宇宙。

凝聚不属于这里。它是更锐的陈述：某阶段的子集现身于一个「按该阶段而非按诸子集本身」界住的阶段处，而那是基数算术会想要的东西。公理不想要。

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

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

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 ( 𝒮ᵥ )
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 )
open import L.Axioms.Basic {ℓ} using ( LsetS )
open import L.Axioms.Full {ℓ} lem using ( hasSeparationL )

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; ⟪_⟫; ⟪_⟫↪ )

open TruthAlgebra (hPropAlgebra (ℓ-suc ℓ))
open hPropStructure 𝒮ʟ

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

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

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

作为公式的条件

「此物之中的一切都在 a 之中」，其中 a 以常元点名，而它可以，因为它是模型的元素。它的含义恰是模型自己的包含关系，一分不差：对象语言的有界全称就是真值代数在载体上、由隶属设防的交，而包含关系当初正是这么定义的。

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

subFo-is-⊆ : (a x : S) → ((x ∷ []) ⊨ subFo a) ≡ (x ⊆ˢ a)
subFo-is-⊆ a x = refl

界住诸可构造子集

层级的幂集由小类型索引，而其中可构造的成员由一条可构造性陈述切出，那条陈述高出一个宇宙，无法保持索引为小。降层把它拉回来，而降层正是排中律早已买下的东西。索引一小，诸阶段便构成小族，界层引理随即适用。

然后是满射性：每个可构造子集确实现身于那个上界之下。它的底集在层级的意义上是子集，因为可构造集的成员可构造，故被模型自己的包含关系覆盖；层级的幂集因而含有它，它的索引给出小族的一个点，而它自己的最早阶段落在上界之下。

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

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

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

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

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

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

  β : V ℓ
  β = b .fst

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

  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
    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 = fib .snd
    i : Ix
    i = fib .fst
      , equivFun (rsz (⟪ P ⟫↪ (fib .fst)) .snd)
          (subst (λ w → ⟨ isL w ⟩) (sym pa) (x .snd))

字段

用那个条件雕出界层阶段。出来的东西以「在该阶段中，且包含于 a」这一合取为索引，而第二个合取项蕴含第一个，故两个谓词逐点一致，答案随之搬运过去。

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
  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))

小结

hasPowerL 是模型的幂集字段，经「界住诸可构造子集、雕出一个阶段」证得。前沿只剩选择。

这个证明用了什么、没用什么，才是该带走的那一点。它两次使用了那个经典接口，一次为把无界的可构造性陈述降层，一次为层级自己的幂集；它还用了任意公式的分离，那是上一部付过的账。它没有用凝聚，也不需要：公理索取的是「诸可构造子集构成一个集合」，而非「它们现身得早」。