The axiom of infinity in L

Inside L, the constructively defined chain numeralL provides one internal numeral for each natural number. A chain of separate sets is not yet an infinite set: the axiom of infinity asks for one constructible set whose members are exactly the numerals. This chapter exhibits that set and, in the same stroke, identifies the classical dependency used to place the candidate set in the constructible hierarchy: knowing at which stage of the constructible hierarchy an ordinal such as ω appears is a comparison of ordinals, the imported stage theorem receives the module parameter lem because its proof uses that comparison.

The module takes a single assumption, lem : LEM (ℓ-suc ℓ), a decision procedure for propositions at one level above the working level ℓ. Everything the chapter needs is either constructive or derived from this one parameter, so the later proofs can be read with a precise account of which steps are classical.

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

open import Base.Prelude
open import Base.Classical using ( LEM )

module L.Axioms.Infinity {ℓ : Level} (lem : LEM (ℓ-suc ℓ)) where

The ambient hierarchy supplies ω and its successor sucV, while numeralL-fst relates each internal numeral to the corresponding member of ω. The stage theorem ord∈Lset-suc, instantiated with lem, places an ordinal at its successor stage. This is the sole point at which the proof below invokes a result parameterized by excluded middle.

open import FOL.ZFStructure using ( module hPropStructure )
import FOL.ZFModel
open import L.Constructible {ℓ} using ( 𝒮ʟ; isL )
open import L.Ordinal {ℓ} using ( suc-ord; ω-ord )
open import L.Ordinal.Stages {ℓ} lem using ( ord∈Lset-suc )

Propositional truncation expresses mere existence: ∣_∣₁ places a given witness inside that truncation. The operation ⇔toPath converts two implications between truth values into a path between those truth values, which is the form required by the set specification.

open import L.Axioms.Basic {ℓ} using ( uniqueL )
open import L.Axioms.Numerals {ℓ} using ( numeralL; numeralL-fst )

import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∣_∣₁ )
open import Cubical.Functions.Logic using ( ⇔toPath )

Truth values here are hProp packages, and their indexed disjunction ∃[ x ] P x expresses mere existence over a carrier. For the constructible structure 𝒮ʟ, ∈ˢ denotes membership and ≈ˢ denotes structural equality, whose underlying equality is equality of the ambient sets.

open import Cubical.HITs.CumulativeHierarchy.Constructions
  using ( module InfinitySet )
open InfinitySet using ( sucV; ω )

open hPropStructure 𝒮ʟ

Finally SetOf names the type of realizers of a class: a constructible set together with a proof that, for every element, its membership truth value equals the class's value. The infinity field of the model record will ask for contractibility of this type, and uniqueL will supply that from a single realizer.

module ModelL = FOL.ZFModel 𝒮ʟ
open ModelL using ( SetOf )

Collecting the chain

The ambient ω, whose members are the library numerals, is the natural candidate. The proof that it is constructible applies ord∈Lset-suc to ω; this imported stage theorem is instantiated with the module parameter lem. The definitions of the numeral chain and its membership specification do not themselves invoke that parameter.

The statement ω∈L has the truncated form prescribed by the definition of isL. A witness before truncation is the stage sucV ω: ω-ord says that ω is an ordinal, suc-ord says that sucV ω is again an ordinal, and ord∈Lset-suc places ω at that stage. The element ωʟ pairs the ambient set ω with this constructibility proof, so x ∈ˢ ωʟ is membership in its underlying ambient set.

ω∈L : ⟨ isL ω ⟩
ω∈L = ∣ sucV ω , (suc-ord ω-ord , ord∈Lset-suc ω ω-ord) ∣₁

ωʟ : S
ωʟ = ω , ω∈L

It remains to verify that the members of ωʟ are exactly the internal numerals. The class isNumeralL says of an element x that it is structurally equal to the chain's n-th link for some natural number n; as an indexed disjunction it merely asserts that some index works, without choosing one. The specification ω-specL then proves that membership in ωʟ and isNumeralL agree pointwise as truth values, and hasInfinityL promotes the realizer to the contractibility the axiom field requires. Both directions of the specification run through the same two ingredients: the ambient characterization of membership in ω, and the chain's projection equation numeralL-fst.

The class isNumeralL disjoins, over the carrier Lift ℕ, the family of propositions x ≈ˢ numeralL (lower n). The Lift deserves a word: ∃[ x ] P x requires its carrier to live at the working level, while ℕ lives at ℓ-zero, and lifting is a pure level adjustment carrying exactly the same elements, with lower recovering the plain index. The specification ω-specL states the goal as a path between truth values, (x ∈ˢ ωʟ) ≡ isNumeralL x, and ⇔toPath reduces proving that path to proving the two implications.

isNumeralL : S → hProp (ℓ-suc ℓ)
isNumeralL x = ∃[ n ∶ Lift {ℓ-zero} {ℓ-suc ℓ} ℕ ] x ≈ˢ numeralL (lower n)

ω-specL : (x : S) → (x ∈ˢ ωʟ) ≡ isNumeralL x
ω-specL x = ⇔toPath
  (PT.map (λ { (k , p) → lift (lower k)

Each direction maps witnesses while they remain inside propositional truncation. Forward, write the lifted index as k : Lift ℕ and set n = lower k. Ambient membership in ω supplies p : # n ≡ fst x; then sym p ∙ sym (numeralL-fst n) proves x ≈ˢ numeralL n. Backward, from q : fst x ≡ fst (numeralL n), the path sym (q ∙ numeralL-fst n) : # n ≡ fst x gives the required ambient membership witness. Thus ωʟ has exactly the internal numerals as members. Finally, uniqueL makes the explicit realizer (ωʟ , ω-specL) the center of a contraction and gives a path from that center to every other realizer, proving SetOf isNumeralL contractible.

             , (sym p ∙ sym (numeralL-fst (lower k))) }))
  (PT.map (λ { (n , q) → lift (lower n)
             , (sym (q ∙ numeralL-fst (lower n))) }))

hasInfinityL : isContr (SetOf isNumeralL)
hasInfinityL = uniqueL isNumeralL (ωʟ , ω-specL)

Recap

The constructible set ωʟ collects exactly the chain numeralL. The explicit realizer and extensional uniqueness give the contractibility required by the infinity field. The proof uses the excluded-middle parameter through ord∈Lset-suc when establishing the constructibility of ω; the membership specification itself follows from the two projection paths above.