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

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

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

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

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 ( _∈_ )

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

open import Cubical.HITs.CumulativeHierarchy.Constructions
  using ( module InfinitySet )
open InfinitySet {ℓ} using ( ω )
import Cubical.Data.Empty as Empty
import Cubical.HITs.PropositionalTruncation as PT

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

open PT using ( ∥_∥₁ )

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

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

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

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

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

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