---
title: "構成可能宇宙は GCH を満たす"
module: L.GCH.Theorem
lang: ja
site: "Bedrock"
description: "構成可能宇宙は GCH を満たす"
stage: "GCH の証明"
reading_order: 120
canonical: https://bedrock.institute/ja/L.GCH.Theorem.html
html: L.GCH.Theorem.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/GCH/Theorem.lagda.md
prerequisites: [Base.Prelude, Base.Classical, L.Model, L.GCH, L.GCH.Assembly, L.GCH.StageInjection, L.GCH.SuccessorIntoPowerSet, L.GCH.BoundedSubset]
routes: [hulls-and-counting]
translations: [https://bedrock.institute/en/L.GCH.Theorem.md, https://bedrock.institute/zh/L.GCH.Theorem.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
# 構成可能宇宙は GCH を満たす

前章までに、無限な内部基数の冪集合をその後続基数と比較するための三つの評価を確立しました。それらを `L` 上の ZF モデル構造と合わせると、構成可能宇宙が一般連続体仮説を満たすことが従います。古典的仮定は、モデルとその内部基数論の構成を通して用いてきた同じ排中律の実例だけです。

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

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

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

open import L.Model {ℓ} lem using ( L⊨ZF )
```

目標は `GCHStatement L⊨ZF` です。これは、基礎となる集合が順序数であり、内部基数であり、かつ `ω` に属さない `L` の要素 `κ` にわたって量化します。結論は、後続基数 `δ` と、`𝒫 κ` と `δ` の間の両方向の内部的に符号化された単射が単に存在することを求めます。ここで冪集合を定めるのは `L⊨ZF` です。

```agda
open import L.GCH {ℓ} lem using ( GCHStatement )
open import L.GCH.Assembly {ℓ} lem using ( gch-from-internal-bill )
open import L.GCH.StageInjection {ℓ} lem using ( stage-counted )
open import L.GCH.SuccessorIntoPowerSet {ℓ} lem using ( succ-into-power )
open import L.GCH.BoundedSubset {ℓ} lem using ( internal-bounded-subset )
```

このような `κ` を固定します。一般の含意は、まずその内部の後続基数 `δ` を得ます。各 `y ∈ 𝒫 κ` に対して、有界部分集合定理は、`y ∈ Lset β` かつ `β` が `κ` へ単射するような順序数 `β` を与えます。`δ` が内部基数であることと `κ ∈ δ` を順序数の三分法と合わせると `β ∈ δ` が従い、したがって `y ∈ Lset δ` です。これにより冪集合全体が `Lset δ` へ単射し、段階計数定理がこの段階を `δ` へ単射するので、`InjL (𝒫 κ) δ` を得ます。最後に `succ-into-power` は、`κ` の無限性と `δ` の後続基数としての性質を用いて、この比較を `InjL δ (𝒫 κ)` へ移します。両方向の単射が必要な GCH の実例を与え、これを `L⊨GCH` と記します。

```agda
L⊨GCH : GCHStatement L⊨ZF
L⊨GCH = gch-from-internal-bill L⊨ZF stage-counted internal-bounded-subset
          (succ-into-power L⊨ZF)
```