The constructible universe satisfies GCH

Fix a universe level ℓ and assume lem : LEM (ℓ-suc ℓ). This hypothesis supplies a decision for each proposition at that level; it remains an explicit parameter of the constructions below.

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

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.

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.

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)