The generalized continuum hypothesis inside L

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.

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

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

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

open import FOL.ZFStructure using ( module hPropStructure )

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.

import FOL.ZFModel
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ )
open import L.Constructible {ℓ} using ( 𝒮ʟ; IsOrd )
open import L.Cardinal {ℓ} lem using ( IsCardinalL; InjL; SuccCardL )
open import Cubical.HITs.CumulativeHierarchy.Base using ( _∈_ )

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 ( ω )
import Cubical.Data.Empty as Empty
import Cubical.HITs.PropositionalTruncation as PT

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 PT using ( ∥_∥₁ )

open hPropStructure 𝒮ᵥ using ( _∈ˢ_ )
open hPropStructure 𝒮ʟ 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 κ ∈ˢ ω ⟩ → Empty.⊥)

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 ( 𝒫 )