この章を読むか、対話型目次と依存グラフで別のルートを選べます。

対話型目次 · 依存グラフ

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

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

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

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

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

ZF モデル

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

open hPropView 𝒮ʟ

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 }