The root: L ⊨ ZFC

This is the root of the book, the chapter every other chapter exists to serve. Read its statement with care, because the care is the content.

What is proven. Within cubical Agda, the constructible structure 𝒮ʟ is a model of ZFC: L⊨ZFC below. Together with Part 3, where the ambient hierarchy models ZF, this is the relative consistency of choice in semantic form: a universe satisfying ZF contains a sub-universe satisfying ZFC, so any inconsistency of ZFC would already be an inconsistency of ZF.

Relative to what. To the host. The construction lives inside cubical Agda with its universe tower, a metatheory informally about as strong as ZFC plus an inaccessible cardinal. The book never claims an unconditional "Con(ZFC)"; consistency here is always consistency relative to the declared host, and the host's strength is a price printed on the label, not hidden in the machinery. This is no defect of mechanization: every consistency proof anywhere is relative to the metatheory that carries it, and the only choice is whether to say so.

What is assumed. One instance of the excluded middle, at the model's own truth level. That is the whole bill. The module took a second parameter for most of the book's life, the frontier, a registry of statements not yet proven; the registry emptied when the previous chapter paid the last of them, and the parameter, together with the chapter that held it, is gone. What is left is a theorem in the ordinary sense, with one hypothesis, both of whose halves are printed on this page.

{-# 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 )

The theorem

Assembly, and every line of it is now an axiom chapter. The twelve fields of

isZFModel come from Parts 4's axiom chapters, and the choice field comes from L.Choice.Transversal, applied to the very model being assembled: choice is stated relative to a ZF model on this carrier, because the intersection it names is that model's derived operation, and the model it is applied to is the one built on the line above.

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 }

Recap

The root stands, and it stands unconditionally: L⊨ZFC, the constructible structure models ZFC, from the excluded-middle interface and nothing else. What the reader should carry away is the shape of the claim: a semantic, relative consistency theorem, priced in the open. Every field of ZFC is a theorem rather than a hypothesis, choice included, and there is no registry left to shrink.