The generalized continuum hypothesis inside L

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 {ℓ : Level} (lem : LEM (ℓ-suc ℓ)) where

Inside L, the generalized continuum hypothesis compares two sets attached to every infinite internal cardinal κ: its power set and its internal successor cardinal. In this development, having the same size is expressed by internal coded injections in both directions. The statement below formulates this comparison using the power set supplied by the model itself.

The notions of internal cardinal, successor cardinal, and coded injection are all formed relative to the chosen instance of excluded middle. Thus the statement belongs to the same classical context as the cardinal theory developed earlier, with no additional classical assumption.

The quantifier ranges over the carrier of the constructible structure. Such an element consists of an ambient set together with a proof of constructibility. Membership in ω is read through the ambient membership relation; its negation supplies the condition that the cardinal is infinite.

open import Cubical.HITs.CumulativeHierarchy.Constructions
  using ( module InfinitySet )
open InfinitySet {ℓ} using ( ω )

A ZF model supplies its own power-set operation. For a model proof zf, the notation 𝒫 κ denotes the set that the power-set axiom of that model assigns to κ. Consequently, every set and every membership assertion in the comparison remains internal to the constructible structure.

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

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

The hypotheses on κ can be read in order. Its underlying set is an ordinal. It is an internal cardinal, meaning that for every δ ∈ κ there is no internal coded injection from κ into δ. Finally, κ ∉ ω. Together these conditions say that κ is an infinite internal cardinal.

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

The conclusion says, merely, that an internal successor cardinal δ of κ exists together with internal coded injections from 𝒫 κ to δ and from δ to 𝒫 κ. This pair of comparisons is the form in which this development states that the two sets have the same size. The outer truncation does not choose a particular δ, while each occurrence of InjL in turn retains only the existence of a suitable constructible injection code.

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