可构造宇宙是 ZFC 的模型

可构造结构 𝒮ʟ 满足 ZF 的全部公理，而它的典范良序进一步给出选择公理。所得陈述分别记作 L⊨ZF 与 L⊨ZFC。两者都在立方 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 }