从四条内部界装配 GCH

我们把这一假设固定在证明所需的唯一宇宙层级上。因此下文所有构造，包括最小候选者论证，都只依赖同一个显式实例 LEM (ℓ-suc ℓ)。

module L.GCH.Assembly {ℓ : Level} (lem : LEM (ℓ-suc ℓ)) where

本章完成 L 内部所采用的 GCH 陈述。对每个无穷内部序数基数 κ，它在最外层的命题截断下证明：存在一个后继基数 δ，并有两条编码单射 𝒫κ ↪ δ 与 δ ↪ 𝒫κ。证明可以在截断的局部分支内使用见证，但最终既不选定一个 δ，也不交出任何一张单射图。

装配过程使用的唯一经典原则是排中律。一旦把候选者放进一个小良序中，排中律便可把仅仅非空的候选族化为其唯一最小元。

这里汇合了两个集合论视角。外围累积层级提供成员关系与小呈现，可构造子宇宙提供谓词 isL 和各层 Lset α；随后由 ZF 模型结构解释内部幂集。

极小化论证使用序数的三项事实：序数中的成员关系具有传递性，任意两个序数满足三分律，并且序数的小呈现上的成员关系次序是良序。这些事实使有界搜索所得的最小候选者能够控制任意竞争基数。

内部大小比较由 InjL 表达，即「存在一个编码单射的可构造图」的命题截断。IsCardinalL 据此定义内部基数，SuccCardL 刻画严格大于给定基数的最小内部序数基数；CardAboveL 只在命题截断下提供某个更大的基数。

最终的 GCH 陈述要求：仅仅存在一个后继基数，并有它与模型幂集之间两个方向的编码单射。为构造从幂集出发的比较，证明先把包含关系编码成单射，再与计数可构造层的单射复合。

有界搜索通过序数 sucV (θ .fst) 的小呈现变成一个小类型。其索引表示 sucV (θ .fst) 的元素，也就是不大于 θ 的序数；ω 则另用于表达所研究的基数不是有限序数。若两个可构造对的底层集合相等，可构造性的命题性会把这一相等提升为这两个配对的相等。

open import Cubical.HITs.CumulativeHierarchy.Properties using ( ⟪_⟫; ⟪_⟫↪ )
open import Cubical.HITs.CumulativeHierarchy.Constructions
  using ( module InfinitySet )
open InfinitySet {ℓ} using ( ω; sucV )

三分律将通过余积的三个分支来分析。不可能的分支落入空类型，而命题截断只记录存在而不暴露选定见证；因此下文对它的消去总是以成员关系或另一个截断存在陈述等命题为目标。

记作 _∈ˢ_ 的成员关系是累积层级中的外围成员关系。逐点包含使用这一关系，特别是「κ 的一个可构造子集的每个外围元素也属于 κ」这一陈述。

open hPropView 𝒮ᵥ using ( _∈ˢ_ )

记外围的命题值集合论结构为 SV。它的载体包含逐点子集前提所量化的全部集合。

module SV = hPropView 𝒮ᵥ

记限制在可构造集合上的相应结构为 SL。它的元素把一个外围底层集合与该集合属于 L 的证明配成一对。

module SL = hPropView 𝒮ʟ

SL 上的 ZF 模型结构提供指定的内部幂集 𝒫κ。因此后文提到的幂集都指可构造模型的幂集，而不是整个累积层级中的外围幂集。

module ModelL = FOL.ZFModel 𝒮ʟ

四条内部估计

第一个接口陈述「层被计数」的含义：对每对「可构造序数 δ 与底层集合恰为层 Lset δ 的集合 Lδ」，若 δ 非有限，则该层单射入该序数。该类型排除有限序数，且只产出编码单射的截断存在。

StageCountedCoded : Type (ℓ-suc ℓ)
StageCountedCoded =
    (δ Lδ : SL.S) → IsOrd (δ .fst) → (⟨ δ .fst ∈ˢ ω ⟩ → ⊥₀)
  → Lδ .fst ≡ Lset (δ .fst) → InjL Lδ δ

第二个接口陈述有界子集定理。对非有限、序数、内部基数的 κ，以及任一「其外围元素都属于 κ」的可构造集合 y，都仅仅地存在序数 β，使 y 落在层 Lset β 中且 β 单射入 κ。子集前提量化外围集合，从而覆盖那些自身不带可构造性证明的元素。

InternalBoundedSubset : Type (ℓ-suc ℓ)
InternalBoundedSubset =
    (κ : SL.S) → IsOrd (κ .fst) → IsCardinalL κ → (⟨ κ .fst ∈ˢ ω ⟩ → ⊥₀)
  → (y : SL.S) → ((z : SV.S) → ⟨ z ∈ˢ y .fst ⟩ → ⟨ z ∈ˢ κ .fst ⟩)
  → ∥ Σ[ β ∶ SL.S ]

产出的记录包含 β 的序数性、y 在层中的落位，以及 β 到 κ 的编码单射。

       (IsOrd (β .fst) × ⟨ y .fst ∈ˢ Lset (β .fst) ⟩ × InjL β κ) ∥₁

第三个接口是条件性的反向比较：给定 κ 的内部幂集单射入 κ 的后继基数 δ，它返回 δ 到幂集的反向单射。该假设是真正条件性的；仅凭后继基数记录无法调用此接口。

SuccIntoPower : ModelL.isZFModel → Type (ℓ-suc ℓ)
SuccIntoPower zf =
    (κ δ : SL.S) → (⟨ κ .fst ∈ˢ ω ⟩ → ⊥₀) → SuccCardL δ κ
  → InjL (𝒫 κ) δ → InjL δ (𝒫 κ)
  where open ModelL.isZFModel zf using ( 𝒫 )

第四个接口陈述后继基数的仅仅存在：对每个无穷内部序数基数，存在某个后继基数。结论是截断的，调用者不能从中选定全局代表。

SuccCardExists : Type (ℓ-suc ℓ)
SuccCardExists =
    (κ : SL.S) → IsOrd (κ .fst) → IsCardinalL κ
  → (⟨ κ .fst ∈ˢ ω ⟩ → ⊥₀)
  → ∥ Σ[ δ ∶ SL.S ] SuccCardL δ κ ∥₁

更大的内部基数存在

约简模块固定严格大于 κ 的序数内部基数 θ，并证明：在 θ 的后继所决定的小搜索空间内，存在 κ 之上的最小基数。这是本章的核心：先固定显式上界，再在其内最小化。

module Reduce (κ : SL.S) (oκ : IsOrd (κ .fst))
              (θ : SL.S) (oθ : IsOrd (θ .fst))
              (cθ : IsCardinalL θ) (κ∈θ : ⟨ κ .fst ∈ˢ θ .fst ⟩) where

open LeastCardInjL θ oθ using ( up; self; self-eq )

A : Type ℓ
A = ⟪ sucV (θ .fst) ⟫

opaque
  w : SWO A
  w = ordSWO (sucV (θ .fst)) (suc-ord oθ)

opaque
  unfolding w
  w-lt : (m n : A) → let module W = SWO w in (m W.<∙ n)
       ≡ ⟨ ⟪ sucV (θ .fst) ⟫↪ m ∈ˢ ⟪ sucV (θ .fst) ⟫↪ n ⟩
  w-lt m n = refl

isPropIsCardinalL : (x : SL.S) → isProp (IsCardinalL x)
isPropIsCardinalL x =
  isPropΠ (λ _ → isPropΠ (λ _ → isPropΠ (λ _ → isProp⊥)))

Good : A → hProp (ℓ-suc ℓ)
Good b = (IsCardinalL (up b) × ⟨ κ .fst ∈ˢ (up b) .fst ⟩)
       , isProp× (isPropIsCardinalL (up b)) ((κ .fst ∈ˢ (up b) .fst) .snd)

definedGood : FOL.Semantics.FormulaPredicate 𝒮ʟ A SL.S id Good
definedGood = FOL.Semantics.presented 
  (cardinalAt zero ∧̇ (var (suc zero) ∈̇ var zero)) (λ b → up b ∷ κ ∷ [])
  (λ b → ⇔toPath
    (λ { (card , mem) → CardinalAt.fill zero (up b ∷ κ ∷ []) card , mem })
    (λ { (sat , mem) → CardinalAt.read zero (up b ∷ κ ∷ []) sat , mem }))

upSelf : up self ≡ θ
upSelf = Σ≡Prop (λ x → (isL x) .snd) self-eq

nonempty : ∥ Σ[ b ∶ A ] ⟨ Good b ⟩ ∥₁
nonempty = ∣ self
          , subst (λ z → IsCardinalL z × ⟨ κ .fst ∈ˢ z .fst ⟩)
              (sym upSelf) (cθ , κ∈θ) ∣₁

least : Σ[ b ∶ A ] IsLeast w Good b
least = leastOfFormula w definedGood lem nonempty

δ : SL.S
δ = up (least .fst)

δ∈sθ : ⟨ δ .fst ∈ˢ sucV (θ .fst) ⟩
δ∈sθ = member (sucV (θ .fst)) (least .fst)

oδ : IsOrd (δ .fst)
oδ = mem-ord {A = sucV (θ .fst)} (suc-ord oθ) (δ .fst) δ∈sθ

cδ : IsCardinalL δ
cδ = ((least .snd) .fst) .fst

κ∈δ : ⟨ κ .fst ∈ˢ δ .fst ⟩
κ∈δ = ((least .snd) .fst) .snd

δ-min : (b : A) → ⟨ Good b ⟩ → let module W = SWO w in (b W.<∙ least .fst → ⊥₀)
δ-min = (least .snd) .snd

leastness : (c : SL.S) → IsOrd (c .fst) → IsCardinalL c
          → ⟨ κ .fst ∈ˢ c .fst ⟩
          → (x : SL.S) → ⟨ x .fst ∈ˢ δ .fst ⟩ → ⟨ x .fst ∈ˢ c .fst ⟩
leastness c oc cc κ∈c = go (ord-tri (δ .fst) oδ (c .fst) oc)
  where

  go : Tri (δ .fst) (c .fst)
     → (x : SL.S) → ⟨ x .fst ∈ˢ δ .fst ⟩ → ⟨ x .fst ∈ˢ c .fst ⟩
  go (inl δ∈c)       x x∈δ = oc .fst x∈δ δ∈c
  go (inr (inl e))   x x∈δ = subst (λ v → ⟨ x .fst ∈ˢ v ⟩) e x∈δ
  go (inr (inr c∈δ)) x x∈δ = ⊥₀-rec (δ-min b bGood b<δ)

    where
    c∈sθ : ⟨ c .fst ∈ˢ sucV (θ .fst) ⟩
    c∈sθ = suc-ord oθ .fst c∈δ δ∈sθ
    b : A
    b = fiber (sucV (θ .fst)) c∈sθ .fst

    be : ⟪ sucV (θ .fst) ⟫↪ b ≡ c .fst
    be = fiber (sucV (θ .fst)) c∈sθ .snd
    upb : up b ≡ c
    upb = Σ≡Prop (λ v → (isL v) .snd) be
    bGood : ⟨ Good b ⟩

    bGood = subst (λ z → IsCardinalL z × ⟨ κ .fst ∈ˢ z .fst ⟩)
              (sym upb) (cc , κ∈c)
    b<δ : let module W = SWO w in b W.<∙ least .fst
    b<δ = transport (λ i → sym (w-lt b (least .fst)) i)
            (subst (λ v → ⟨ v ∈ˢ δ .fst ⟩) (sym be) c∈δ)

CardAboveL 只在命题截断下给出某个序数内部基数 θ，满足 κ ∈ θ；它既不提供最小性，也不选定 θ。证明把每个局部见证送入 Reduce，并在那里于 sucV (θ .fst) 的呈现中完成极小化。因此，所得后继基数仍处在命题截断之下。

succCardExists : SuccCardExists
succCardExists κ oκ cκ κ∉ω = map₁ build (CardAboveL κ oκ cκ κ∉ω)
  where
  build : Σ[ θ ∶ SL.S ]
            (IsOrd (θ .fst) × IsCardinalL θ × ⟨ κ .fst ∈ˢ θ .fst ⟩)

在一个局部分支内，build 把选出的 δ 与 SuccCardL δ κ 的四个条款打包：δ 是序数，是内部基数，满足 κ ∈ δ，并且包含于每个严格大于 κ 的序数内部基数。

        → Σ[ δ ∶ SL.S ] SuccCardL δ κ
  build (θ , oθ , cθ , κ∈θ) = R.δ , R.oδ , R.cδ , R.κ∈δ , R.leastness
    where module R = Reduce κ oκ θ oθ cθ κ∈θ

兑现结构性估计

指数为序数的层是可构造的，依据联系层与可构造性的公理。

stage-is-L : (δ : SL.S) → IsOrd (δ .fst) → ⟨ isL (Lset (δ .fst)) ⟩
stage-is-L δ ordδ = isL-Lset (δ .fst) ordδ

幂集的桥接谓词陈述其内容：对可构造集合 κ 与 y，其中 κ 是序数且 y 属于模型幂集 𝒫κ，y 的每个外围元素 z 都可构造、属于 κ，且是序数。

zStrongest : ModelL.isZFModel → Type (ℓ-suc ℓ)
zStrongest zf =
    (κ y : SL.S) → IsOrd (κ .fst) → ⟨ y .fst ∈ˢ (𝒫 κ) .fst ⟩
  → (z : SV.S) → ⟨ z ∈ˢ y .fst ⟩
  → (⟨ isL z ⟩ × ⟨ z ∈ˢ κ .fst ⟩ × IsOrd z)

这座桥依赖所给的 ZF 模型，因为其前提涉及该模型指定的幂集。因此，在整个论证中，𝒫κ 始终是 L 的内部幂集。

  where open ModelL.isZFModel zf using ( 𝒫 )

这里的细节在于量化域发生了转换。幂集成员关系给出的子集陈述量化可构造集合，而 z 起初量化整个外围层级。先用 L 的传递性证明 z 可构造，才能把内部子集陈述施用于它；随后由 z ∈ κ 与 κ 的序数性得到 z 的序数性。

z-strongest : (zf : ModelL.isZFModel) → zStrongest zf
z-strongest zf κ y ordκ y∈𝒫κ z z∈y = isLz , z∈κ , mem-ord {A = κ .fst} ordκ z z∈κ
  where
  open ModelL.isZFModel zf using ( 𝒫; hasPower )

z 的可构造性由传递性得出：z 属于可构造集合 y，而 y 自身可构造。

  isLz : ⟨ isL z ⟩
  isLz = isL-trans z∈y (y .snd)

模型幂集的定义规格把 y ∈ 𝒫κ 认同为内部子集关系 y ⊆ κ。这一关系量化 SL 的元素，因此上一步所得的可构造性不可缺少。

  y⊆κ : ⟨ y ModelL.⊆ˢ κ ⟩
  y⊆κ = subst ⟨_⟩ (ModelL.℩-spec (hasPower κ) y) y∈𝒫κ

内部子集关系随即施加于「z 连同其可构造性」的配对，得到 z 属于 κ。

  z∈κ : ⟨ z ∈ˢ κ .fst ⟩
  z∈κ = y⊆κ (z , isLz) z∈y

每个子集都在后继之前落定

落位引理就模型、有界子集接口与 κ 的固定后继基数 δ 陈述：模型幂集 𝒫κ 的每个元素都落在层 Lset δ 中。

stage-landing :
    (zf : ModelL.isZFModel) → InternalBoundedSubset
  → (κ : SL.S) → IsOrd (κ .fst) → IsCardinalL κ → (⟨ κ .fst ∈ˢ ω ⟩ → ⊥₀)
  → (δ : SL.S) → SuccCardL δ κ
  → (y : SL.S) → ⟨ y .fst ∈ˢ (ModelL.isZFModel.𝒫 zf κ) .fst ⟩

对每个固定的 y，有界子集定理只在命题截断下返回一个合适的层索引 β。目标结论 y ∈ Lset δ 本身是命题，所以证明可以使用局部的 β 推理，而无需为所有 y 一致地选择层索引。该定理所需的外围逐点子集前提，正是刚才建立的桥。

  → ⟨ y .fst ∈ˢ Lset (δ .fst) ⟩
stage-landing zf ibs κ ordκ cardκ κ∉ω δ (ordδ , cardδ , κ∈δ , _) y y∈𝒫κ =
  rec₁ ((y .fst ∈ˢ Lset (δ .fst)) .snd) place (ibs κ ordκ cardκ κ∉ω y y⊆κ)
  where
  y⊆κ : (z : SV.S) → ⟨ z ∈ˢ y .fst ⟩ → ⟨ z ∈ˢ κ .fst ⟩

由 y ∈ 𝒫κ 与 z ∈ y，最强成员关系引理得到 z ∈ κ。其证明先利用 L 的传递性认出外围元素 z 是可构造的，从而能把幂集成员关系所表达的内部子集关系施用于 z。

  y⊆κ z z∈y = z-strongest zf κ y ordκ y∈𝒫κ z z∈y .snd .fst

从 δ 到 κ 的单射不可能存在，因为 δ 是内部基数且 κ 是 δ 的元素。这条反驳是下文排除不可能三歧分支的工具。

  no-δ↪κ : InjL δ κ → ⊥₀
  no-δ↪κ = cardδ κ κ∈δ

对固定的子集 y，有界子集估计在命题截断下给出一个序数 β，使得 y ∈ Lset β，并且存在内部编码单射 β ↪ κ。在局部展开这样一个见证后，place 用序数三歧性比较 β 与 δ，并证明 y 已属于 Lset δ。

  place : Σ[ β ∶ SL.S ]
            (IsOrd (β .fst) × ⟨ y .fst ∈ˢ Lset (β .fst) ⟩ × InjL β κ)
        → ⟨ y .fst ∈ˢ Lset (δ .fst) ⟩
  place (β , ordβ , y∈Lβ , β↪κ) = go (ord-tri (β .fst) ordβ (δ .fst) ordδ)
    where

若 β 低于 δ，塔的单调性直接把较低层中的元素放进较高层。若 β 等于 δ，则注入 β ↪ κ 会变成注入 δ ↪ κ，与 δ 的基数性矛盾。

    go : Tri (β .fst) (δ .fst) → ⟨ y .fst ∈ˢ Lset (δ .fst) ⟩
    go (inl β∈δ)       = Lset-mono β∈δ y∈Lβ
    go (inr (inl e))   = ⊥₀-rec (no-δ↪κ (subst (λ b → InjL b κ) β≡δ β↪κ))
      where
      β≡δ : β ≡ δ

在相等分支中，因为可构造性取命题值，底层集合的相等可提升为相应 L 元素的相等。在余下的 δ ∈ β 分支中，先取包含给出的 δ ↪ β，再接上已有的编码单射 β ↪ κ，便会产生被排除的编码单射 δ ↪ κ。

      β≡δ = Σ≡Prop (λ x → (isL x) .snd) e
    go (inr (inr δ∈β)) = ⊥₀-rec (no-δ↪κ
      (injl-trans δ β κ (inclusion-coded δ β δ⊆β) β↪κ))
      where
      δ⊆β : (z : SV.S) → ⟨ z ∈ˢ δ .fst ⟩ → ⟨ z ∈ˢ β .fst ⟩

包含是序数 β 的传递性施于两条成员关系的结果。

      δ⊆β z z∈δ = ordβ .fst z∈δ δ∈β

把幂集编码到后继以下

幂集比较现在来自复合链 𝒫κ ↪ Lset δ ↪ δ。第一条箭头来自「内部幂集的每个元素都属于 Lset δ」，第二条则用 δ 计数这一可构造层。证明没有为 𝒫κ 的各个元素一致地选择层索引。

power-into-succ :
    (zf : ModelL.isZFModel) → StageCountedCoded → InternalBoundedSubset
  → (κ : SL.S) → IsOrd (κ .fst) → IsCardinalL κ → (⟨ κ .fst ∈ˢ ω ⟩ → ⊥₀)
  → (δ : SL.S) → SuccCardL δ κ
  → InjL (ModelL.isZFModel.𝒫 zf κ) δ

逐点包含先由 inclusion-coded 转换为编码单射 𝒫κ ↪ Lset δ。层计数假设给出 Lset δ ↪ δ，再由 injl-trans 复合两者。由于两项比较都用 InjL 表达，见证它们的图仍处于命题截断之下。

power-into-succ zf scc ibs κ ordκ cardκ κ∉ω δ sc@(ordδ , _ , κ∈δ , _) =
  injl-trans (𝒫 κ) Lδ δ (inclusion-coded (𝒫 κ) Lδ into)
    (scc δ Lδ ordδ δ∉ω refl)
  where
  open ModelL.isZFModel zf using ( 𝒫 )

δ 处的层通过把层集合与其可构造性证书配对而呈现为 L 的元素，证书由 δ 的序数性得来。

  Lδ : SL.S
  Lδ = Lset (δ .fst) , stage-is-L δ ordδ

后继基数 δ 落在 ω 之外：若它在 ω 内，则成员关系 κ ∈ δ 经 ω 的传递性将迫使 κ ∈ ω，与假设矛盾。

  δ∉ω : ⟨ δ .fst ∈ˢ ω ⟩ → ⊥₀
  δ∉ω δ∈ω = κ∉ω (ω-ord .fst {x = δ .fst} {y = κ .fst} κ∈δ δ∈ω)

幂集的每个元素由安放引理落入 Lset δ 之内，其可构造性经 L 的传递性从幂集成员关系供给。

  into : (z : SV.S) → ⟨ z ∈ˢ (𝒫 κ) .fst ⟩ → ⟨ z ∈ˢ Lδ .fst ⟩
  into z z∈ =
    stage-landing zf ibs κ ordκ cardκ κ∉ω δ sc (z , isL-trans z∈ ((𝒫 κ) .snd)) z∈

广义连续统假设

最终定理把两个方向的职责明确分开。层计数与有界子集定理建立 𝒫κ ↪ δ。只有取得这条单射之后，独立的条件定理 SuccIntoPower 才能把它与后继基数事实一同使用，建立 δ ↪ 𝒫κ。

gch-from-internal-bill :
    (zf : ModelL.isZFModel)
  → StageCountedCoded → InternalBoundedSubset → SuccIntoPower zf
  → GCHStatement zf
gch-from-internal-bill zf scc ibs sip κ ordκ cardκ κ∉ω =

定理 succCardExists 只给出后继基数 δ 的命题截断存在。因此映射在每个局部见证内工作：step 保留后继基数证明，用落层论证构造命题截断下的编码单射 𝒫κ ↪ δ，再把该结果交给独立的条件接口，得到命题截断下的编码单射 δ ↪ 𝒫κ。

  map₁ step (succCardExists κ ordκ cardκ κ∉ω)
  where
  open ModelL.isZFModel zf using ( 𝒫 )
  step : Σ[ δ ∶ SL.S ] SuccCardL δ κ
       → Σ[ δ ∶ SL.S ] (SuccCardL δ κ × InjL (𝒫 κ) δ × InjL δ (𝒫 κ))

落层论证给出 pis : InjL (𝒫 κ) δ，独立的条件接口再以 pis 为前提给出 InjL δ (𝒫 κ)。每个 InjL 都是「存在可构造单射码」的命题截断，所以结果恰好记录两个相反方向的编码单射存在性；它没有选定任何一张图，也没有构造双射、集合相等或基数算术等式。

  step (δ , sc) = δ , sc , pis , sip κ δ κ∉ω sc pis
    where
    pis : InjL (𝒫 κ) δ
    pis = power-into-succ zf scc ibs κ ordκ cardκ κ∉ω δ sc