The axiom of infinity in L

The chain of numerals was built in the previous chapter and cost nothing. What is left is the axiom itself, which is one step and is where the whole classical price of infinity is paid.

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

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

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

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 )
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 )
open import Cubical.HITs.CumulativeHierarchy.Constructions
  using ( module InfinitySet )
open InfinitySet using ( sucV; ω )

open TruthAlgebra (hPropAlgebra (ℓ-suc ℓ))
open hPropStructure 𝒮ʟ

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

Collecting the chain

Now the axiom proper. A set whose members are exactly the numerals must be exhibited inside L, and the ambient hierarchy has the obvious candidate, namely ω. What has to be shown is that ω is constructible, and the previous chapter gives it in one line: ω is an ordinal, and an ordinal appears at the stage after itself.

This is the step that costs the excluded middle, and it is worth seeing where the cost went. Not into the chain, which was free; not into collecting a family, which no principle here does; but into knowing which ordinals live at which stage, and that is a comparison.

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

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

It remains to check that the members of ωʟ are exactly the numerals of the chain. Membership in ωʟ is membership in ω, which the library gives as "merely hit by some library numeral"; the chain's projection equation turns each of those into a member of the chain, and back. So ωʟ realises the numeral predicate, and extensionality makes it the unique such set.

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

ω-specL : (x : S) → (x ∈ˢ ωʟ) ≡ isNumeralL x
ω-specL x = ⇔toPath
  (PT.map (λ { (k , p) → lift (lower k)
             , (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 axiom of infinity is paid in full: the chain numeralL with its two pinning equations, and hasInfinityL collecting it into a set. Four fields leave the frontier, and the split between them is the chapter's lesson. Building the chain was free; collecting it cost one comparison of ordinals, and therefore the excluded middle. That is the whole classical content of infinity in L, and it is visible in this chapter's telescope.