The constructible universe satisfies GCH

The preceding chapters established the three estimates needed to compare an infinite internal cardinal's power set with its successor. Together with the ZF model structure on L, they prove that the constructible universe satisfies the generalized continuum hypothesis. The only classical assumption is the same instance of excluded middle used throughout the construction of the model and its internal cardinal theory.

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

The target is GCHStatement L⊨ZF. It quantifies over κ in L whose underlying set is an ordinal, which is an internal cardinal, and which does not belong to ω. It asks merely for a successor cardinal δ and for internal coded injections in both directions between 𝒫 κ and δ; the power set here is the one determined by L⊨ZF.

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 )

Fix such a κ. The general implication first obtains its internal successor cardinal δ. For every y ∈ 𝒫 κ, the bounded-subset theorem supplies an ordinal β such that y ∈ Lset β and β injects into κ. The fact that δ is an internal cardinal and that κ ∈ δ, together with ordinal trichotomy, forces β ∈ δ; hence y ∈ Lset δ. Thus the whole power set injects into Lset δ, and the stage-counting theorem injects that stage into δ, yielding InjL (𝒫 κ) δ. Finally, succ-into-power, using the infinitude of κ and the successor-cardinal facts for δ, turns this comparison into InjL δ (𝒫 κ). These two injections establish the required instance of GCH, recorded as 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)