---
title: "The constructible universe models ZFC"
module: L.Model
lang: en
site: "Bedrock"
description: "The constructible universe models ZFC"
stage: "The canonical well-order and Choice"
reading_order: 85
canonical: https://bedrock.institute/en/L.Model.html
html: L.Model.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/Model.lagda.md
prerequisites: [Base.Prelude, Base.Classical, FOL.ZFStructure, FOL.ZFModel, L.Constructible, L.Axioms.Basic, L.Axioms.Numerals, L.Axioms.Infinity, L.Axioms.Full, L.Axioms.Power, L.Choice.Transversal]
routes: [choice-completion]
translations: [https://bedrock.institute/zh/L.Model.md, https://bedrock.institute/ja/L.Model.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
# 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.

```agda
{-# 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.

```agda
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.

```agda
  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.

```agda
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.

```agda
  { 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.

```agda
  ; 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.

```agda
  ; 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.

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