Landmarks

The trophy case, and it stands at the entrance on purpose. Each landmark below restates a milestone theorem of the book in one self-contained signature, with its full bill of assumptions on display, and names the chapter that proves it. On a first reading nothing here is expected to make sense yet: these signatures are the destination, and learning to read them, symbol by symbol and assumption by assumption, is what the rest of the book is for. Come back after each part lands. For the returning reader the landmarks are stable anchors: a paper can cite one without caring where inside the book its proof lives.

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

module Landmarks where

open import Base.Prelude
open import Base.Impredicativity using ( Impredicativity )
open import Base.Classical using ( LEM )
open import Base.Choice using ( SetChoice )
open import V.Hierarchy using ( 𝒮ᵥ )
open import FOL.ZFModel using ( isZFModel; isZFCModel )
open import L.Constructible using ( 𝒮ʟ )
import V.Model
import L.Model

The hierarchy models ZF(C)

The headline is classical: granted one instance of the excluded middle, at the model's own truth level, the cumulative hierarchy is a model of ZF (chapter

V.Model). Its exact-price form carries the hypothesis as a suffix, charging only Part 0's impredicativity packing; and by Diaconescu's theorem (chapter Base.Choice), one instance of set-level choice funds the upgrade all the way to ZFC.

V⊨ZF : ∀ {ℓ : Level} → LEM (ℓ-suc ℓ) → isZFModel (𝒮ᵥ {ℓ})
V⊨ZF = V.Model.V⊨ZF

V⊨ZF-impredicative : ∀ {ℓ : Level} → Impredicativity ℓ → isZFModel (𝒮ᵥ {ℓ})
V⊨ZF-impredicative = V.Model.VModel.V⊨ZF-impredicative

V⊨ZFC : ∀ {ℓ : Level} → SetChoice (ℓ-suc ℓ) → isZFCModel (𝒮ᵥ {ℓ})
V⊨ZFC = V.Model.V⊨ZFC

The constructible universe models ZFC

The book's main theorem (chapter L.Model): given one instance of the excluded middle at the model's truth level, the constructible structure models ZFC. One hypothesis, and it is the same one the previous landmark pays. This signature carried a second parameter for most of the book's life, a registry of statements the remaining parts still owed; the registry is empty and the parameter is gone. Read with the previous landmark, it is the semantic form of the relative consistency of choice: a ZF universe carries a ZFC sub-universe inside it.

L⊨ZFC : ∀ {ℓ : Level} (lem : LEM (ℓ-suc ℓ)) → isZFCModel (𝒮ʟ {ℓ})
L⊨ZFC = L.Model.L⊨ZFC