構成可能宇宙は GCH を満たす

宇宙レベル ℓ を固定し、lem : LEM (ℓ-suc ℓ) を仮定する。この仮定は該当するレベルの各命題に判定を与え、以下の構成の明示的なパラメータとして保たれる。

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

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

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

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

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