---
title: "L 内部的广义连续统假设"
module: L.GCH
lang: zh
site: "Bedrock"
description: "L 内部的广义连续统假设"
stage: "序数、单射与基数"
reading_order: 92
canonical: https://bedrock.institute/zh/L.GCH.html
html: L.GCH.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/GCH.lagda.md
prerequisites: [Base.Prelude, Base.Classical, FOL.ZFStructure, FOL.ZFModel, V.Hierarchy, L.Constructible, L.Cardinal]
routes: [cardinal-tools]
translations: [https://bedrock.institute/en/L.GCH.md, https://bedrock.institute/ja/L.GCH.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
# L 内部的广义连续统假设

在 `L` 内部，广义连续统假设比较与每个无穷内部基数 `κ` 相联系的两个集合：它的幂集与内部后继基数。本书用两个方向的内部编码单射表示二者大小相同。下面的陈述采用模型自身给出的幂集来表述这一比较。

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

open import Base.Prelude
open import Base.Classical using ( LEM )

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

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

内部基数、后继基数和编码单射都相对于这里选定的排中律实例而定义。因此，这一陈述沿用此前基数理论的经典背景，不再加入其他经典假设。

```agda
import FOL.ZFModel
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ )
open import L.Constructible {ℓ} using ( 𝒮ʟ; IsOrd )
open import L.Cardinal {ℓ} lem using ( IsCardinalL; InjL; SuccCardL )
open import Cubical.HITs.CumulativeHierarchy.Base using ( _∈_ )
```

量词遍历可构造结构的论域。论域中的元素由一个外围集合及其可构造性证明组成。是否属于 `ω` 通过外围成员关系来解释；其否定给出基数为无穷的条件。

```agda
open import Cubical.HITs.CumulativeHierarchy.Constructions
  using ( module InfinitySet )
open InfinitySet {ℓ} using ( ω )
import Cubical.Data.Empty as Empty
import Cubical.HITs.PropositionalTruncation as PT
```

ZF 模型带有自身的幂集运算。给定模型证明 `zf`，记号 `𝒫 κ` 表示该模型的幂集公理为 `κ` 给出的集合。因此，这一比较中的集合与成员陈述都留在可构造结构内部。

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

open hPropStructure 𝒮ᵥ using ( _∈ˢ_ )
open hPropStructure 𝒮ʟ using ( S )

module ModelL = FOL.ZFModel 𝒮ʟ
GCHStatement : ModelL.isZFModel → Type (ℓ-suc ℓ)
```

关于 `κ` 的假设可以依次读出。它的底层集合是序数。它是内部基数，也就是说，对每个 `δ ∈ κ`，都不存在从 `κ` 到 `δ` 的内部编码单射。最后，`κ ∉ ω`。这些条件合在一起说明 `κ` 是无穷内部基数。

```agda
GCHStatement zf =
  (κ : S)
  → IsOrd (fst κ)
  → IsCardinalL κ
  → (⟨ fst κ ∈ˢ ω ⟩ → Empty.⊥)
```

结论仅仅断言：存在 `κ` 的内部后继基数 `δ`，并且存在从 `𝒫 κ` 到 `δ` 以及从 `δ` 到 `𝒫 κ` 的内部编码单射。本书用这两个方向的比较表达两集合大小相同。最外层截断不选定某个特定的 `δ`；其中每个 `InjL` 又只保留合适的可构造单射码的存在性。

```agda
  → ∥ Σ[ δ ∈ S ]
       ( SuccCardL δ κ
       × InjL (𝒫 κ) δ
       × InjL δ (𝒫 κ) ) ∥₁
  where open ModelL.isZFModel zf using ( 𝒫 )
```