The constructible universe models ZFC

The constructible structure 𝒮ʟ satisfies every axiom of ZF, and its canonical well-order supplies the axiom of choice. The resulting statements are L⊨ZF and L⊨ZFC. Both are proved in cubical Agda from one explicitly stated instance of excluded middle at the truth-value level of the model.

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

This is a semantic relative-consistency result. The host metatheory constructs both the ambient hierarchy and its constructible substructure, then verifies the axioms directly in the latter. Accordingly, the theorem does not assert an unqualified consistency statement: it exhibits a model of ZFC relative to the metatheory in which the formalization is carried out.

import FOL.ZFModel
open import L.Constructible {ℓ} using ( 𝒮ʟ )
open import L.Axioms.Basic {ℓ}
  using ( extensionalL; regularityL; hasEmptyL; hasPairL; hasUnionL )
open import L.Axioms.Numerals {ℓ}

The elementary set operations and numerals are obtained constructively. The proofs of infinity, separation, replacement, power set, and the constructible choice theorem use the selected excluded-middle instance. This distinction records exactly where classical reasoning enters the model.

  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 )

The ZF model

The model structure collects twelve verified clauses. Extensionality, regularity, the empty set, pairing, and union are constructive properties of L. Separation and replacement provide the two formula schemes, while the power-set and infinity chapters supply the corresponding sets. The numeral clauses identify the internal natural-number sequence.

open hPropStructure 𝒮ʟ

module ModelL = FOL.ZFModel 𝒮ʟ
open ModelL using ( isZFModel; isZFCModel )
L⊨ZF : isZFModel
L⊨ZF = record

The first five fields state the elementary structural and set-forming principles. Each field receives a theorem already proved for the same membership structure, so their conclusions share one interpretation of sets, membership, and formulas.

  { extensional    = extensionalL
  ; regularity     = regularityL
  ; hasEmpty       = hasEmptyL
  ; hasPair        = hasPairL
  ; hasUnion       = hasUnionL

The next fields add separation, replacement, power sets, and the zero clause for numerals. The two schemes quantify over formulas interpreted in the same structure, while the power-set field fixes the model’s own power-set operation.

  ; hasSeparation  = hasSeparationL
  ; hasReplacement = hasReplacementL
  ; hasPower       = hasPowerL
  ; numeral        = numeralL
  ; numeral-zero   = numeralL-zero

The successor equation for numerals and the existence of infinity complete the twelve fields. At this point the record is closed, and L⊨ZF is a proof that the constructible structure satisfies all of ZF.

  ; numeral-suc    = numeralL-suc
  ; hasInfinity    = hasInfinityL }

Adding choice

An isZFCModel consists of a ZF model together with the choice statement interpreted by that model. The constructible well-order theorem supplies choice for L⊨ZF; in particular, the intersections appearing in that statement are the intersections derived from this very ZF structure. Adding this proof yields L⊨ZFC. Thus every ZFC axiom is established as a theorem under the declared excluded-middle hypothesis.

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