Models

Part 1 built a language, gave it worlds to talk about, and pinned down meaning. But nothing so far deserves the name set theory: a bare structure believes nothing. Its membership relation need not admit an empty set, need not pair two elements, need not gather the subsets of anything. What a universe of sets must provide is exactly what the axioms of ZF say, and this chapter states them. Not as postulates, though: the book never extends its metatheory, and its structures are many, not one chosen universe. A model of ZF is a record whose fields are the axioms, so "𝒮 satisfies ZF" means nothing more mysterious than "this record has an inhabitant at 𝒮".

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

open import Base.Prelude
open import Base.Truth
open import FOL.ZFStructure using ( ZFStructure; module hPropStructure )

module FOL.ZFModel {ℓ} (𝒮 : ZFStructure (hPropAlgebra ℓ)) where

Two standing choices, both announced in earlier chapters and both exercised here for the first time. The truth algebra is the canonical hPropAlgebra: axioms assert facts, and the book's mathematical facts live in hProp (per the scope discipline, opening the algebra is what brings the logic symbols into scope). And the constant interpretation is the canonical one from the semantics chapter: the constant domain is the carrier itself and the interpretation is

id, so a parameter appearing in a formula simply is the set it names.

open import FOL.Syntax using ( Formula; var; con; _∈̇_ )
open import FOL.Semantics (hPropAlgebra ℓ) 𝒮 using ( module At )
open import Cubical.Foundations.Prelude using ( isPropIsContr )
open import Cubical.Data.Sigma using ( Σ≡Prop )
open import Cubical.Induction.WellFounded using ( WellFounded; wf→x≮x )
import Cubical.Data.Empty as Empty
import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∥_∥₁ )

open TruthAlgebra (hPropAlgebra ℓ)
open hPropStructure 𝒮

open At S id using ( _⊨_ )

Realizing a class as a set

Nearly every axiom to come has the same shape: there is a set whose members are exactly the so-and-so. Pin down the "so-and-so" first. A class is a propositional predicate on the carrier, S → Ω: something whose membership can be stated, with no promise that any set collects it. (Classes have already appeared in disguise: the restriction 𝒮 ↾ M of the structure chapter cuts along exactly such an M.) IsSetOf Q b then says the set b realizes the class Q, membership for membership. Realization is pointwise equality in hProp, hence a proposition, and SetOf Q packages a realizer with its evidence.

IsSetOf : (S → Ω) → S → Type (ℓ-suc ℓ)
IsSetOf Q b = (x : S) → (x ∈ˢ b) ≡ Q x

isPropIsSetOf : (Q : S → Ω) (b : S) → isProp (IsSetOf Q b)
isPropIsSetOf Q b = isPropΠ (λ x → isSetHProp _ _)

SetOf : (S → Ω) → Type (ℓ-suc ℓ)
SetOf Q = Σ[ b ∈ S ] IsSetOf Q b

How many realizers can one class have? Under extensionality (sets with the same members are equal; it will be the first field of the record) the answer is at most one, in the strong, structural sense: any single realizer makes the whole type of realizers contractible. The lemma takes extensionality as an explicit input, because the record that will provide it has not been defined yet.

setOf-unique : ({a b : S} → ((x : S) → (x ∈ˢ a) ≡ (x ∈ˢ b)) → a ≡ b)
             → (Q : S → Ω) → SetOf Q → isContr (SetOf Q)
setOf-unique ext Q (b , sp) = (b , sp) , λ { (b' , sp') →
  Σ≡Prop (isPropIsSetOf Q) (ext (λ x → sp x ∙ sym (sp' x))) }

The description operator

isContr is the host's unique existence, so isContr (SetOf Q) reads: there is exactly one set of the Qs. Every existence axiom below takes this form, and the payoff is immediate: given unique existence, "the set such that" is a projection. The operator ℩ (a rotated iota, Russell's notation, read "that") extracts the centre of contraction, and its specification is the second projection. Where a classical treatment must adopt a description axiom to pass from unique existence to a term, here the passage is two fsts.

℩ : {Q : S → Ω} → isContr (SetOf Q) → S
℩ c = c .fst .fst

℩-spec : {Q : S → Ω} (c : isContr (SetOf Q)) → IsSetOf Q (℩ c)
℩-spec c = c .fst .snd

Subsets

One derived relation completes the vocabulary: a ⊆ˢ b when every member of a is a member of b. The superscript is the structure-layer mark, as always.

_⊆ˢ_ : S → S → Ω
a ⊆ˢ b = ⋀ S (λ x → (x ∈ˢ a) ⇒ (x ∈ˢ b))

infix  _⊆ˢ_

The axioms, as a record

Here is the heart of the chapter. The fields are the familiar list: extensionality, regularity, empty set, pairing, union, separation, replacement, power set (infinity joins below). Three of them repay a closer look before the code.

Separation and replacement consume the book's own formulas. A textbook writes "for every formula φ"; these two fields take a Formula S 1 or

Formula S 2 and interpret it with the satisfaction relation of the semantics chapter. The language built in Part 1 stops being an object of contemplation here and starts bearing weight. Why formulas, and not arbitrary host predicates S → Ω? Because that stronger schema is a different, second-order theory: the point of ZF's separation is that only first-order describable properties are guaranteed to cut sets out of sets. The gap between "predicate" and "formula" is mathematical content, and Part 4's protagonist lives inside exactly that gap.

Regularity is stated at the meta level (some books call it foundation): the membership relation is well-founded, with WellFounded taken from the host library rather than from any object-language sentence. The next section explains why no sentence could do the job.

Everything else takes the unique-existence form just prepared, and will hand its set over through ℩.

record isZFModel : Type (ℓ-suc ℓ) where
  field
    extensional    : {a b : S} → ((x : S) → (x ∈ˢ a) ≡ (x ∈ˢ b)) → a ≡ b
    regularity     : WellFounded _∈ᵗ_
    hasEmpty       : isContr (SetOf (λ _ → ⊥))
    hasPair        : (a b : S) → isContr (SetOf (λ x → (x ≈ˢ a) ⊔ (x ≈ˢ b)))
    hasUnion       : (a : S) → isContr (SetOf (λ x → ⋁ S (λ y → (y ∈ˢ a) ⊓ (x ∈ˢ y))))
    hasSeparation  : (a : S) (φ : Formula S )
                   → isContr (SetOf (λ x → (x ∈ˢ a) ⊓ ((x ∷ []) ⊨ φ)))
    hasReplacement : (a : S) (φ : Formula S )
                   → ((x : S) → ⟨ x ∈ˢ a ⟩ → isContr (Σ[ y ∈ S ] ⟨ (y ∷ x ∷ []) ⊨ φ ⟩))
                   → isContr (SetOf (λ y → ⋁ S (λ x → (x ∈ˢ a) ⊓ ((y ∷ x ∷ []) ⊨ φ))))
    hasPower       : (a : S) → isContr (SetOf (λ x → x ⊆ˢ a))

Read each λ back into words and the familiar statements reappear. Nothing realizes ⊥, so hasEmpty is the empty set. The pair's members are whatever equals a or b; the union's members are the members of members. Separation keeps those members of a that satisfy φ (the environment x ∷ [] plugs the sole free variable). Replacement first asks φ to be functional on a, one output per input in the isContr sense, then collects the outputs. The power set's members are the subsets.

Why regularity lives at the meta level

Every other axiom speaks either the object language or plain membership; regularity alone reaches for the host's notion of well-foundedness. It has to: no first-order sentence expresses external well-foundedness. The classical argument deserves telling, though the book only tells it; nothing below depends on it, and compactness is not developed here. Suppose some sentence held in exactly the well-founded structures. Extend the language with fresh constants

$a_0, a_1, a_2, \dots$ and the axioms $a_{n+1} \in a_n$. Finitely many of these axioms ask only for a descending chain of some finite length, which well-founded structures supply; so every finite fragment of the extended theory has a model. The compactness theorem of classical model theory then yields one structure satisfying all of it at once: it satisfies the sentence, yet the constants trace an infinite descending ∈-chain through it. So the sentence never captured well-foundedness in the first place.

Compactness is a property of first-order logic itself; no choice of host system moves this line, and a formalization can only choose where to be honest about it. Here the choice is: regularity lives at the meta level, as a field. The ceiling also has a productive face. It shows that the first-order shadow of a structure is strictly coarser than the structure, so restricting attention to "what first-order formulas can see" is a genuine restriction. Part 4 builds its universe out of precisely that restriction; were the shadow lossless, the construction would return everything and prove nothing.

The derived operations

Now ℩ discharges each unique existence into an operation, and ℩-spec into its specification; every specification below is literally one projection. The union of a pair gives binary union, and binary union gives the successor a ⁺ = a ∪ {a} (the pair of a with itself is the singleton): von Neumann's step from a set to the next, the ladder the axiom of infinity will climb.

  ∅ : S
  ∅ = ℩ hasEmpty

  ∅-spec : IsSetOf (λ _ → ⊥) ∅
  ∅-spec = ℩-spec hasEmpty

  pair : S → S → S
  pair a b = ℩ (hasPair a b)

  pair-spec : ∀ a b → IsSetOf (λ x → (x ≈ˢ a) ⊔ (x ≈ˢ b)) (pair a b)
  pair-spec a b = ℩-spec (hasPair a b)

  ⋃ : S → S
  ⋃ a = ℩ (hasUnion a)

  ⋃-spec : ∀ a → IsSetOf (λ x → ⋁ S (λ y → (y ∈ˢ a) ⊓ (x ∈ˢ y))) (⋃ a)
  ⋃-spec a = ℩-spec (hasUnion a)

  _∪_ : S → S → S
  a ∪ b = ⋃ (pair a b)

  _⁺ : S → S
  a ⁺ = a ∪ pair a a

  separate : (a : S) → Formula S  → S
  separate a φ = ℩ (hasSeparation a φ)

  separate-spec : ∀ a φ → IsSetOf (λ x → (x ∈ˢ a) ⊓ ((x ∷ []) ⊨ φ)) (separate a φ)
  separate-spec a φ = ℩-spec (hasSeparation a φ)

  𝒫 : S → S
  𝒫 a = ℩ (hasPower a)

  𝒫-spec : ∀ a → IsSetOf (λ x → x ⊆ˢ a) (𝒫 a)
  𝒫-spec a = ℩-spec (hasPower a)

First dividend: intersection without an axiom

Binary intersection is deliberately not a field. The two-symbol formula

var zero ∈̇ con b says "the variable is a member of b"; hand it to

separate at a and the axioms hand back a ∩ b. Better: its specification is the separation specification, verbatim, because satisfaction of that formula computes to x ∈ˢ b by the defining clauses of ⊨. The faithfulness the semantics chapter promised is now paying out in sets, not just in logic.

This is also the chapter's honest confession. One formula was cheap to write by hand. But the book will need a formula for every predicate it ever wants to separate or replace along, each with a proof that the formula means that predicate, and hand-assembling syntax at that scale is out of the question. Turning host predicates into formulas, certificate included, is a craft of its own, the reification framework catalogued at the book's tail; the witnesses it runs on, the Levy grades and their travel theorems, are already in hand from the close of Part 1.

  _∩_ : S → S → S
  a ∩ b = separate a (var zero ∈̇ con b)

  ∩-spec : ∀ a b x → (x ∈ˢ (a ∩ b)) ≡ ((x ∈ˢ a) ⊓ (x ∈ˢ b))
  ∩-spec a b x = separate-spec a (var zero ∈̇ con b) x

Infinity

One axiom remains, the one that forces a genuinely infinite set into existence. The numerals are the von Neumann naturals: ∅, ∅ ⁺, (∅ ⁺) ⁺, and so on. The record takes the chain itself as a field, pinned down by two propositional equations phrased in raw membership and equality: the zeroth numeral has no members, and the members of a successor numeral are exactly the previous numeral and its members. By extensionality the two equations say precisely numeral zero ≡ ∅ and numeral (suc n) ≡ numeral n ⁺, so nothing is weaker than defining the chain outright. What is gained is room: the equations never mention the derived ∅ and _⁺, so a concrete model may present the chain in whatever form its carrier computes best and discharge them without ever unfolding the description operator.

  field
    numeral      : ℕ → S
    numeral-zero : (z : S) → ⟨ z ∈ˢ numeral zero ⟩ → Empty.⊥
    numeral-suc  : (n : ℕ) (z : S)
                 → (⟨ z ∈ˢ numeral (suc n) ⟩ → ⟨ (z ∈ˢ numeral n) ⊔ (z ≈ˢ numeral n) ⟩)
                 × (⟨ (z ∈ˢ numeral n) ⊔ (z ≈ˢ numeral n) ⟩ → ⟨ z ∈ˢ numeral (suc n) ⟩)

isNumeral is the class this chain sweeps out: equal to some numeral. The quantification runs over ℕ lifted to the working level, since the book's indexing data lives at the bottom universe. The axiom of infinity, in the strong form this book uses, then says: that class is a set. Stated this way it is strictly stronger than the usual "some set contains ∅ and is closed under successor", and it is the version that makes ω directly usable as the set of naturals: every member of ω is a numeral, not merely every numeral a member.

  isNumeral : S → Ω
  isNumeral x = ⋁ (Lift {ℓ-zero} {ℓ} ℕ) (λ n → x ≈ˢ numeral (lower n))

  field
    hasInfinity : isContr (SetOf isNumeral)

  ω : S
  ω = ℩ hasInfinity

  ω-spec : IsSetOf isNumeral ω
  ω-spec = ℩-spec hasInfinity

First theorems

Extensionality upgrades the whole existence apparatus once and for all. Any realizer is the unique realizer (uniqueSetOf); and even a merely existing realizer, hidden under propositional truncation, reproduces unique existence (mereSetOf→isContr). The pattern of the classical description axiom recurs here as a theorem: to build "the set of the Qs" it will always suffice to show some set of the Qs merely exists. Regularity draws first blood too: no set is a member of itself.

  uniqueSetOf : (Q : S → Ω) → SetOf Q → isContr (SetOf Q)
  uniqueSetOf = setOf-unique extensional

  mereSetOf→isContr : (Q : S → Ω) → ∥ SetOf Q ∥₁ → isContr (SetOf Q)
  mereSetOf→isContr Q = PT.rec isPropIsContr (uniqueSetOf Q)

  x∉x : (x : S) → ⟨ x ∈ˢ x ⟩ → Empty.⊥
  x∉x x h = wf→x≮x regularity h

ZFC: choice as an extension

The line between ZF and ZFC is drawn as a record boundary, because the book's capstone lives on that line: Part 4 constructs, inside any model of ZF, a sub-universe satisfying choice, and folding choice into the base record would erase the very distinction that construction is about. The axiom of choice is taken in choice-set form: given a set a whose members are nonempty and pairwise disjoint, some set meets each member of a in exactly one point. This form is stated with membership and the derived intersection alone; its equivalence with the other formulations is model-internal mathematics, deferred until needed. Note that the hypotheses and the conclusion all wear the truncation ∥_∥₁: choice asserts bare existence, promising no canonical choice set, and that reticence is exactly its force.

record isZFCModel : Type (ℓ-suc ℓ) where
  field
    zf : isZFModel
  open isZFModel zf public
  field
    hasChoice :
      (a : S)
      → ((x : S) → ⟨ x ∈ˢ a ⟩ → ∥ Σ[ y ∈ S ] ⟨ y ∈ˢ x ⟩ ∥₁)
      → ((x y : S) → ⟨ x ∈ˢ a ⟩ → ⟨ y ∈ˢ a ⟩
           → ∥ Σ[ z ∈ S ] (⟨ z ∈ˢ x ⟩ × ⟨ z ∈ˢ y ⟩) ∥₁ → x ≡ y)
      → ∥ Σ[ c ∈ S ] ((x : S) → ⟨ x ∈ˢ a ⟩
           → isContr (Σ[ z ∈ S ] ⟨ z ∈ˢ (c ∩ x) ⟩)) ∥₁

Recap

A model of ZF is a record: extensionality, meta-level regularity (the compactness ceiling makes any other placement dishonest), unique-existence fields for the constructions, separation and replacement consuming the book's own formulas, and strong infinity through the numeral chain. ℩ turns fields into operations whose specifications are projections; intersection fell out of separation and a two-symbol formula, the first set built by feeding the framework its own language.

isZFCModel adds choice on top. The record's appetite for formulas is now the book's outstanding debt; the reification framework at the book's tail is the factory that will pay it, running on the Levy witnesses Part 1 already forged.