構成可能宇宙は ZFC のモデル

構成可能構造 𝒮ʟ は ZF のすべての公理を満たし、その標準的な整列順序から選択公理も得られます。得られる主張を L⊨ZF と L⊨ZFC と記します。いずれも cubical Agda の中で証明され、モデルの命題宇宙と同じレベルにある、明示された一つの排中律だけを用います。

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

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

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

open import FOL.ZFStructure using ( module hPropStructure )

これは意味論的な相対無矛盾性の結果です。宿主メタ理論の中で周囲の階層とその構成可能な部分構造を作り、後者において各公理を直接検証します。したがって、無条件の無矛盾性を主張するのではなく、形式化を担うメタ理論に相対して ZFC のモデルを与えます。

import FOL.ZFModel
open import L.Constructible {ℓ} using ( 𝒮ʟ )
open import L.Axioms.Basic {ℓ}
  using ( extensionalL; regularityL; hasEmptyL; hasPairL; hasUnionL )
open import L.Axioms.Numerals {ℓ}

基本的な集合演算と数項は構成的に得られます。無限、分出、置換、冪集合、および構成可能な選択定理の証明は、選んだ排中律の実例を用います。この区別により、古典的推論がモデルに入る箇所が正確に示されます。

  using ( numeralL; numeralL-zero; numeralL-suc )
open import L.Axioms.Infinity {ℓ} lem using ( hasInfinityL )
open import L.Axioms.Full {ℓ} lem using ( hasSeparationL; hasReplacementL )
open import L.Axioms.Power {ℓ} lem using ( hasPowerL )
open import L.Choice.Transversal {ℓ} lem using ( hasChoiceL )

ZF モデル

モデル構造は、検証済みの十二の条項をまとめます。外延性、正則性、空集合、対、和集合は L の構成的な性質です。分出と置換が二つの論理式図式を与え、冪集合と無限の章が対応する集合を与えます。三つの数項の条項は、モデル内部の自然数列を定めます。

open hPropStructure 𝒮ʟ

module ModelL = FOL.ZFModel 𝒮ʟ
open ModelL using ( isZFModel; isZFCModel )
L⊨ZF : isZFModel
L⊨ZF = record

レコードの最初の五つの欄は、基本的な構造上の性質と集合形成原理を述べます。各欄には同じ所属構造について証明された定理が入り、集合、所属、論理式はすべて同じ解釈を共有します。

  { extensional    = extensionalL
  ; regularity     = regularityL
  ; hasEmpty       = hasEmptyL
  ; hasPair        = hasPairL
  ; hasUnion       = hasUnionL

続く欄は、分出、置換、冪集合、および数項の零の条項を加えます。二つの公理図式は同じ構造で解釈される論理式にわたって量化し、冪集合の欄はモデル自身の冪集合演算を定めます。

  ; hasSeparation  = hasSeparationL
  ; hasReplacement = hasReplacementL
  ; hasPower       = hasPowerL
  ; numeral        = numeralL
  ; numeral-zero   = numeralL-zero

数項の後続方程式と無限集合の存在が最後の二つの欄を満たします。ここでレコードが閉じ、L⊨ZF は構成可能構造が ZF 全体を満たすことの証明となります。

  ; numeral-suc    = numeralL-suc
  ; hasInfinity    = hasInfinityL }

選択公理を加える

isZFCModel は、ZF モデルと、そのモデルで解釈された選択の主張からなります。構成可能な整列順序の定理が L⊨ZF に選択公理を与えます。とくに、その主張に現れる共通部分は、まさにこの ZF 構造から導かれる共通部分です。この証明を加えると L⊨ZFC が得られます。したがって、宣言した排中律の仮定のもとで、ZFC の各公理はすべて定理として確立されます。

L⊨ZFC : isZFCModel
L⊨ZFC = record { zf = L⊨ZF ; hasChoice = hasChoiceL L⊨ZF }