可以直接阅读本章，也可以通过交互式目录和依赖图选择其他路线。

交互式目录 · 依赖图

固定宇宙层级 ℓ，并假设 lem : LEM (ℓ-suc ℓ)。这个假设为相应层级的每个命题提供判定，并始终作为下文构造的显式参数。

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

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