The root: L ⊨ ZFC

这里是本书的根，其余每一章都为它服务的那一章。请仔细读它的陈述，因为这份仔细本身就是内容。

证了什么。在 cubical Agda 之内，可构造结构 𝒮ʟ 是 ZFC 的模型：下文的 L⊨ZFC。与第三部 (环境层级满足 ZF) 合观，这就是语义形式的选择公理相对一致性：满足 ZF 的宇宙内部含有满足 ZFC 的子宇宙，故 ZFC 的任何矛盾都早已是 ZF 的矛盾。

相对于什么。相对于宿主。整个构造住在带宇宙塔的 cubical Agda 里，这个元理论的强度非形式地约当于 ZFC 加一个不可达基数。本书从不宣称无条件的「Con (ZFC)」；此处的一致性永远是相对于申明的宿主的一致性，宿主的强度是印在标签上的价格，不是藏在机器里的暗账。这并非机械化的缺陷：任何地方的任何一致性证明都相对于承载它的元理论，可选的只是说不说出来。

假设了什么。一份排中律实例，取模型自己的真值层级。账单全在这里了。本模块在全书大半光景里还收第二个参数，即前沿，尚未证明的陈述之登记簿；上一章还清最后一笔时登记簿清空，那个参数连同持有它的那一章一并消失。剩下的是一条通常意义上的定理，只带一个假设，而这个假设的两半都印在本页上。

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

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

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

open import FOL.ZFStructure using ( module hPropStructure )
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 )

open hPropStructure 𝒮ʟ

module ModelL = FOL.ZFModel 𝒮ʟ
open ModelL using ( isZFModel; isZFCModel )

定理

合龙，而如今每一行都出自某一章公理。isZFModel 的十二个字段来自第四部诸公理章，选择字段来自 L.Choice.Transversal，作用于正被装配的这个模型自身：选择相对于此载体上的一个 ZF 模型陈述，因为它所点名的交是那个模型的派生运算，而它所作用的那个模型，正是上一行造出来的那个。

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
  ; numeral-suc    = numeralL-suc
  ; hasInfinity    = hasInfinityL }

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

小结

根已立起，且是无条件地立起：L⊨ZFC，可构造结构满足 ZFC，只由排中律接口证得，别无其他。读者该带走的是这个论断的形状：一条语义的、相对的一致性定理，价格摆在明处。ZFC 的每个字段都是定理而非假设，选择在内，而再没有登记簿可缩了。