---
title: "The axiom of infinity in L"
module: L.Axioms.Infinity
lang: en
site: "Bedrock"
description: "The axiom of infinity in L"
stage: "Constructible stages and the axioms"
reading_order: 39
canonical: https://bedrock.institute/en/L.Axioms.Infinity.html
html: L.Axioms.Infinity.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/Axioms/Infinity.lagda.md
prerequisites: [Base.Prelude, Base.Classical, FOL.ZFStructure, FOL.ZFModel, L.Constructible, L.Ordinal, L.Ordinal.Stages, L.Axioms.Basic, L.Axioms.Numerals]
routes: [constructible-axioms]
translations: [https://bedrock.institute/zh/L.Axioms.Infinity.md, https://bedrock.institute/ja/L.Axioms.Infinity.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
# 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.

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

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

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

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

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

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

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

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