L の内部における一般連続体仮説

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

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

L の内部における一般連続体仮説は、各無限な内部基数 κ に付随する二つの集合、すなわちその冪集合と内部の後続基数を比較する。本書では、大きさが等しいことを両方向の内部的に符号化された単射で表す。以下では、モデル自身が与える冪集合を用いてこの比較を定式化する。

内部基数、後続基数、符号化された単射はいずれも、ここで選んだ排中律の実例に相対して定義される。したがって、この主張は先に展開した基数論と同じ古典的な前提のもとにあり、それ以外の古典的仮定を加えない。

量化は構成可能構造の領域にわたる。その要素は、周囲の集合と構成可能性の証明からなる。ω への所属は周囲の所属関係によって解釈され、その否定が基数の無限性を表す。

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

ZF モデルはそれ自身の冪集合演算を備える。モデルの証明 zf に対して、𝒫 κ はそのモデルの冪集合公理が κ に与える集合を表す。したがって、この比較に現れる集合と所属の主張は、すべて構成可能構造の内部にとどまる。

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

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

κ に対する仮定は順に読める。その基礎となる集合は順序数である。また κ は内部基数であり、各 δ ∈ κ に対して κ から δ への内部的に符号化された単射は存在しない。最後に κ ∉ ω である。これらを合わせると、κ が無限な内部基数であることを表す。

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

結論は、κ の内部の後続基数 δ が単に存在し、さらに 𝒫 κ から δ へ、また δ から 𝒫 κ への内部的に符号化された単射が存在することを述べる。本書では、この両方向の比較によって二つの集合の大きさが等しいことを表す。外側の切り詰めは特定の δ を選ばず、各 InjL も適切な構成可能な単射の符号の存在だけを保つ。

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