{-# OPTIONS --cubical-compatible #-}
module Padova2025.Explorations.Ordinals where

Numbers larger than infinity#

open import Padova2025.ProgrammingBasics.Naturals.Base
open import Padova2025.ProvingBasics.Negation
open import Padova2025.ProvingBasics.Connectives.Disjunction
open import Padova2025.ProvingBasics.Connectives.Existential
open import Padova2025.ProvingBasics.Connectives.Conjunction
open import Padova2025.ProvingBasics.Termination.Gas using (𝟙; tt)

Rough sketch, bring into shape. And add lots of praise for https://arxiv.org/abs/2208.03844 which this account is based on.

A key motto in set theory is: Never stop, always continue. This motto is nicely exemplified by the ordinal numbers, one of several flavors of numbering systems which support infinitely large numbers (other prominent flavors are the cardinal numbers and the surreal numbers).

The ordinal numbers start like this:

0, 1, 2, 3, 4, …

However, unlike the natural numbers, we then don’t stop. Instead we continue:

0, 1, 2, 3, 4, …, ω

So ω is the first infinite number. But it is not the last one, as we continue:

0, 1, 2, 3, 4, …, ω, ω + 1, ω + 2, …

Should there be a number larger than all of those? Following the motto, of course there should:

0, 1, 2, 3, 4, …, ω, ω + 1, ω + 2, …, ω + ω = ω · 2

Now increasing our cruise speed and skipping over infinitely many numbers, we eventually obtain the following creatures:

ω · ω = ω², ω³, ω⁴, ω^ω, ω^{^ω}, ω^{ω^{ω^⋰}} = ε₀, ε₀^{ε₀^{ε₀^⋰}} = ε₁, ε₁^{ε₁^{ε₁^⋰}} = ε₂

In this way we obtain more and more epsilon numbers. After having obtained ε₀, ε₁, ε₂ and so on we keep going to obtain ε_ω, ε_ε₀, ε_{ε_ε₀}, and so on; still not stopping, we eventually obtain the number

ε_{ε_{ε_⋱}} = ζ₀

and still have a long way to go. Armed with just the operations “add one” and “keep going”, starting with zero we have thereby obtained quite a few numbers. (Which, by the way, are still considered puny by seasoned set theorists: All the displayed numbers have only countably many predecessors.)

For a tour of a longer initial segment of the ordinals, we recommend an account by John Baez .

Picture of ω: :-) I I I I I …

Picture of ω + 1: +——————+ :-) |I I I I I …| I +——————+

Picture of ω + ω + 1: +————-+ +————-+ :-) |I I I … | |I I I … | I +————-+ +————-+

Picture of 1 + ω: :-) I I I I I I …

What do we know about ω + 1 vs. 1 + ω? A: succ ω = ω + 1 > ω; 1 + ω = ω.

The three fundamental convictions regarding (countable) ordinals numbers are:

Zero should exist.
Every number should have a successor.
Every (strictly ascending) sequence should have a limit.

For instance, ω is the limit of the sequence

0, 1, 2, 3, … || || || f 0 f 1 f 2

Note: ω is also the limit of the sequence

0, 1, 2, 4, 8, 16, 32, … || || || || || g 0 g 1 g 2 g 3 g 4

We simultaneously define, in a mutual manner, a type O of (representations of) ordinal numbers, types x < y of witnesses that x is strictly smaller than y, types x ≤ y of witnesses that x is at most y, and for each function f : ℕ → O a type Monotonic f of witnesses that f is a strictly increasing sequence.

infix 4 _≤_ _<_
data O : Set
data _≤_ : O → O → Set
_<_ : O → O → Set
Monotonic : (ℕ → O) → Set

Monotonic f = (n : ℕ) → f n < f (succ n)

data O where
  zer : O
  suc : O → O
  lim : (f : ℕ → O) → Monotonic f → O

x < y = suc x ≤ y

data _≤_ where
  ≤-zer      : {x : O} → zer ≤ x
  ≤-suc-mon  : {x y : O} → x ≤ y → suc x ≤ suc y
  ≤-trans    : {x y z : O} → x ≤ y → y ≤ z → x ≤ z
  ≤-cocone   : {f : ℕ → O} {fmon : Monotonic f} {x : O} {n : ℕ}
             → x ≤ f n → x ≤ lim f fmon
  ≤-limiting : {f : ℕ → O} {fmon : Monotonic f} {x : O}
             → ((n : ℕ) → f n ≤ x) → lim f fmon ≤ x

We will see below that the ≤-trans constructor is not needed, however the proof is not particularly short.

Exercise: Basic properties#

If the terms of f are all at most the corresponding term in g, then the limit of f is at most the limit of g.

Exercise 1lim-mon

lim-mon
  : {f g : ℕ → O} {fmon : Monotonic f} {gmon : Monotonic g}
  → ((n : ℕ) → f n ≤ g n)
  → lim f fmon ≤ lim g gmon
lim-mon = {!!}

The reference solution uses: ≤-limiting ≤-cocone

Your solution

Reference solution

lim-mon
  : {f g : ℕ → O} {fmon : Monotonic f} {gmon : Monotonic g}
  → ((n : ℕ) → f n ≤ g n)
  → lim f fmon ≤ lim g gmon
lim-mon p = ≤-limiting (λ n → ≤-cocone (p n))

Exercise 2≤-refl

≤-refl : {x : O} → x ≤ x
≤-refl = {!!}

The reference solution uses: zer ≤-zer suc ≤-suc-mon lim

Your solution

Reference solution

≤-refl : {x : O} → x ≤ x
≤-refl {zer}        = ≤-zer
≤-refl {suc x}      = ≤-suc-mon ≤-refl
≤-refl {lim f fmon} = lim-mon (λ a → ≤-refl)

Exercise 3id≤suc

id≤suc : {x : O} → x ≤ suc x
id≤suc = {!!}

The reference solution uses: zer ≤-zer ≤-suc-mon lim ≤-limiting ≤-trans ≤-cocone ≤-refl

Your solution

Reference solution

id≤suc : {x : O} → x ≤ suc x
id≤suc {zer}     = ≤-zer
id≤suc {suc x}   = ≤-suc-mon id≤suc
id≤suc {lim f x} = ≤-limiting (λ n → ≤-trans id≤suc (≤-suc-mon (≤-cocone ≤-refl)))

Exercise: Defining infinity#

fromℕ : ℕ → O
fromℕ zero     = zer
fromℕ (succ n) = suc (fromℕ n)

Exercise 4fromℕ-mon

fromℕ-mon : Monotonic fromℕ
fromℕ-mon = {!!}

The reference solution uses: ≤-refl

Your solution

Reference solution

fromℕ-mon : Monotonic fromℕ
fromℕ-mon n = ≤-refl

uno : O
uno = suc zer

ω : O
ω = lim fromℕ fromℕ-mon

Exercise 5ω'

ω' : O
ω' = lim (λ n → fromℕ (succ n)) {!!}

The reference solution uses: ≤-refl

Your solution

Reference solution

ω' : O
ω' = lim (λ n → fromℕ (succ n)) (λ n → ≤-refl)

Exercise 6example₀

example₀ : ω ≤ ω'
example₀ = {!!}

The reference solution uses: id≤suc

Your solution

Reference solution

example₀ : ω ≤ ω'
example₀ = lim-mon (λ n → id≤suc)

Exercise 7example₁

example₁ : ω' ≤ ω
example₁ = {!!}

The reference solution uses: ≤-limiting ≤-cocone succ ≤-refl

Your solution

Reference solution

example₁ : ω' ≤ ω
example₁ = ≤-limiting (λ n → ≤-cocone {n = succ n} ≤-refl)

Ordinal addition#

In a mutual manner, we simultaneously define ordinal addition and prove a monotonicity result for ordinal addition.

infixl 6 _+_
_+_ : O → O → O
+-mon : {x a b : O} → a ≤ b → (x + a) ≤ (x + b)

Here is the definition of ordinal addition.

a + zer        = a
a + suc b      = suc (a + b)
a + lim f fmon = lim (λ n → a + f n) (λ n → +-mon (fmon n))

Now you are asked to fill in the required lemma.

Exercise 8+-mon

+-mon {b = zer} ≤-zer        = {!!}
+-mon {b = suc b} ≤-zer      = {!!}
+-mon {b = lim f fmon} ≤-zer = {!!}
+-mon (≤-trans p q)          = {!!}
+-mon (≤-suc-mon p)          = {!!}
+-mon (≤-cocone p)           = {!!}
+-mon (≤-limiting p)         = {!!}

The reference solution uses: ≤-refl id≤suc zero

Your solution

Reference solution

+-mon {b = zer} ≤-zer        = ≤-refl
+-mon {b = suc b} ≤-zer      = ≤-trans id≤suc (≤-suc-mon (+-mon ≤-zer))
+-mon {b = lim f fmon} ≤-zer = ≤-cocone (+-mon (≤-zer {f zero}))
+-mon (≤-trans p q)          = ≤-trans (+-mon p) (+-mon q)
+-mon (≤-suc-mon p)          = ≤-suc-mon (+-mon p)
+-mon (≤-cocone p)           = ≤-cocone (+-mon p)
+-mon (≤-limiting p)         = ≤-limiting (λ b → +-mon (p b))

Exercise: Infinity plus one and one plus infinity#

Exercise 9example₂

example₂ : ω < ω + uno
example₂ = {!!}

The reference solution uses: ≤-refl

Your solution

Reference solution

example₂ : ω < ω + uno
example₂ = ≤-refl

Exercise 10example₃

example₃ : uno + ω ≤ ω
example₃ = {!!}

The reference solution uses: ≤-limiting ≤-cocone succ ℕ suc zer fromℕ zero ≤-refl ≤-suc-mon

Your solution

Reference solution

example₃ : uno + ω ≤ ω
example₃ = ≤-limiting (λ n → ≤-cocone {n = succ n} (lemma n))
  where
  lemma : (n : ℕ) → suc zer + fromℕ n ≤ suc (fromℕ n)
  lemma zero     = ≤-refl
  lemma (succ n) = ≤-suc-mon (lemma n)

Exercise: Adding zero#

Exercise 11+-zer

+-zer : (x : O) → zer + x ≤ x
+-zer = {!!}

The reference solution uses: ≤-zer suc ≤-suc-mon lim

Your solution

Reference solution

+-zer : (x : O) → zer + x ≤ x
+-zer zer       = ≤-zer
+-zer (suc x)   = ≤-suc-mon (+-zer x)
+-zer (lim f x) = lim-mon (λ n → +-zer (f n))

Exercise: A more general comparison lemma#

The type f simulates g defined below contains witnesses of the assertion that every term in the sequence g is dominated by some term in the sequence f. For instance, the sequence 0, 1, 2, … simulates the sequence 0, 1, 2, 4, 8, 16, … (and vice versa).

_simulates_ : (ℕ → O) → (ℕ → O) → Set
f simulates g = (a : ℕ) → ∃[ b ] g a ≤ f b

Exercise 12comparison-lemma

comparison-lemma
  : {f g : ℕ → O} {fmon : Monotonic f} {gmon : Monotonic g}
  → f simulates g → lim g gmon ≤ lim f fmon
comparison-lemma = {!!}

The reference solution uses: ≤-limiting ≤-cocone snd

Your solution

Reference solution

comparison-lemma
  : {f g : ℕ → O} {fmon : Monotonic f} {gmon : Monotonic g}
  → f simulates g → lim g gmon ≤ lim f fmon
comparison-lemma sim = ≤-limiting (λ n → ≤-cocone (snd (sim n)))

With this comparison lemma in place, we can reprove lim-mon from above:

Exercise 13lim-mon'

lim-mon'
  : {f g : ℕ → O} {fmon : Monotonic f} {gmon : Monotonic g}
  → ((n : ℕ) → f n ≤ g n)
  → lim f fmon ≤ lim g gmon
lim-mon' p = comparison-lemma {!!}

The reference solution uses: _,_

Your solution

Reference solution

lim-mon'
  : {f g : ℕ → O} {fmon : Monotonic f} {gmon : Monotonic g}
  → ((n : ℕ) → f n ≤ g n)
  → lim f fmon ≤ lim g gmon
lim-mon' p = comparison-lemma (λ n → n , p n)

Exercise: Equality of ordinal numbers#

The elements of type O are not ordinal numbers, but (mostly non-unique) representations of ordinal numbers. Hence for many purposes a custom equivalence relation is more appropriate than the standard equality type of O:

infix 4 _≈_
_≈_ : O → O → Set
x ≈ y = x ≤ y × y ≤ x

Exercise: A direct description of inequality#

Above, we have defined _≤_ in an inductive fashion. This makes it easy to construct witnesses, but hard to assess whether for given ordinal number (representations) x and y a witness of type x ≤ y exists. For this task, a direct description is more useful.

Code : O → O → Set
Code zer          y            = 𝟙
Code (suc x)      zer          = ⊥
Code (suc x)      (suc y)      = Code x y
Code (suc x)      (lim f fmon) = ∃[ n ] Code (suc x) (f n)
Code (lim f fmon) zer          = ⊥
Code (lim f fmon) (suc y)      = (k : ℕ) → Code (f k) (suc y)
Code (lim f fmon) (lim g gmon) = (k : ℕ) → ∃[ n ] Code (f k) (g n)

Exercise 14Code-refl

Code-refl : {x : O} → Code x x
Code-refl = {!!}

The reference solution uses: zer tt suc lim _,_

Your solution

Reference solution

Code-refl : {x : O} → Code x x
Code-refl {zer}        = tt
Code-refl {suc x}      = Code-refl {x}
Code-refl {lim f fmon} = λ k → k , Code-refl {f k}

Exercise 15Code-suc

Code-suc : {x y : O} → Code x y → Code (suc x) (suc y)
Code-suc = {!!}

Your solution

Reference solution

Code-suc : {x y : O} → Code x y → Code (suc x) (suc y)
Code-suc p = p

The following three auxiliary functions need to be defined mutually. None of the following definitions is particularly pretty. We need to power through.

Code-trans         : {x y z : O} → Code x y → Code y z → Code x z
Code-cocone        : {f : ℕ → O} {fmon : Monotonic f} {x : O} {n : ℕ} → Code x (f n) → Code x (lim f fmon)
Code-cocone-simple : {f : ℕ → O} {fmon : Monotonic f} {n : ℕ} → Code (f n) (lim f fmon)

Exercise 16Code-trans

Code-trans {zer}        {y}          {z}          p q       = {!!}
Code-trans {suc x}      {suc y}      {suc z}      p q       = {!!}
Code-trans {suc x}      {suc y}      {lim f fmon} p (n , q) = {!!}
Code-trans {suc x}      {lim f fmon} {suc z}      (n , p) q = {!!}
Code-trans {suc x}      {lim f fmon} {lim g gmon} (n , p) q = {!!}
Code-trans {lim f fmon} {suc y}      {suc z}      p q       = {!!}
Code-trans {lim f fmon} {suc y}      {lim g gmon} p (n , q) = {!!}
Code-trans {lim f fmon} {lim g gmon} {suc z}      p q       = {!!}
Code-trans {lim f fmon} {lim g gmon} {lim h hmon} p q       = {!!}

The reference solution uses: tt fst snd

Your solution

Reference solution

Code-trans {zer}        {y}          {z}          p q       = tt
Code-trans {suc x}      {suc y}      {suc z}      p q       = Code-trans {x} {y} {z} p q
Code-trans {suc x}      {suc y}      {lim f fmon} p (n , q) = n , Code-trans {suc x} {suc y} {f n} p q
Code-trans {suc x}      {lim f fmon} {suc z}      (n , p) q = Code-trans {suc x} {f n} {suc z} p (q n)
Code-trans {suc x}      {lim f fmon} {lim g gmon} (n , p) q = fst (q n) , Code-trans {suc x} {f n} {g (fst (q n))} p (snd (q n))
Code-trans {lim f fmon} {suc y}      {suc z}      p q       = λ k → Code-trans {f k} {suc y} {suc z} (p k) q
Code-trans {lim f fmon} {suc y}      {lim g gmon} p (n , q) = λ k → n , Code-trans {f k} {suc y} {g n} (p k) q
Code-trans {lim f fmon} {lim g gmon} {suc z}      p q       = λ k → Code-trans {f k} {g (fst (p k))} {suc z} (snd (p k)) (q (fst (p k)))
Code-trans {lim f fmon} {lim g gmon} {lim h hmon} p q       = λ k → fst (q (fst (p k))) , Code-trans {f k} (snd (p k)) (snd (q _))

Exercise 17Code-cocone

Code-cocone {x = zer}                p = {!!}
Code-cocone {x = suc x}              p = {!!}
Code-cocone {x = lim f fmon} {n = n} p = {!!}

The reference solution uses: tt _,_ Code-trans Code-cocone-simple

Your solution

Reference solution

Code-cocone {x = zer}                p = tt
Code-cocone {x = suc x}              p = _ , p
Code-cocone {x = lim f fmon} {n = n} p = λ k → n , Code-trans {x = f k} (Code-cocone-simple {f} {fmon} {k}) p

Code-cocone-simple {f} {fmon} {n} = Code-cocone {f} {fmon} {f n} (Code-refl {f n})

Exercise 18Code-suc-inc-simple

Code-suc-inc-simple : {x : O} → Code x (suc x)
Code-suc-inc-simple {zer}        = {!!}
Code-suc-inc-simple {suc x}      = {!!}
Code-suc-inc-simple {lim f fmon} = {!!}

The reference solution uses: tt Code-trans Code-cocone-simple

Your solution

Reference solution

Code-suc-inc-simple : {x : O} → Code x (suc x)
Code-suc-inc-simple {zer}        = tt
Code-suc-inc-simple {suc x}      = Code-suc-inc-simple {x}
Code-suc-inc-simple {lim f fmon} = λ k → Code-trans {f k} {suc (f k)} {suc (lim f fmon)}
  (Code-suc-inc-simple {f k}) (Code-cocone-simple {f} {fmon} {k})

Exercise 19toCode

toCode : {x y : O} → x ≤ y → Code x y
toCode ≤-zer = {!!}
toCode (≤-suc-mon p) = {!!}
toCode {x} (≤-trans p q) = {!!}
toCode {x} (≤-cocone p) = {!!}
toCode {x} {zer} (≤-limiting {f} {fmon} p) = {!!}
toCode {x} {suc y} (≤-limiting {f} p) = {!!}
toCode {x} {lim f fmon} (≤-limiting {g} {gmon} p) k with Code-trans {suc (g k)} {g (succ k)} (toCode (gmon k)) (toCode {g (succ k)} {lim f fmon} (p (succ k)))
... | (n , q) = {!!}

The reference solution uses: tt Code-cocone zero one Code-suc-inc-simple

Your solution

Reference solution

toCode : {x y : O} → x ≤ y → Code x y
toCode ≤-zer = tt
toCode (≤-suc-mon p) = toCode p
toCode {x} (≤-trans p q) = Code-trans {x} (toCode p) (toCode q)
toCode {x} (≤-cocone p) = Code-cocone {x = x} (toCode p)
toCode {x} {zer} (≤-limiting {f} {fmon} p) = Code-trans {suc (f zero)} {f one} (toCode (fmon zero)) (toCode (p one))
toCode {x} {suc y} (≤-limiting {f} p) = λ k → toCode {f k} {suc y} (p k)
toCode {x} {lim f fmon} (≤-limiting {g} {gmon} p) k with Code-trans {suc (g k)} {g (succ k)} (toCode (gmon k)) (toCode {g (succ k)} {lim f fmon} (p (succ k)))
... | (n , q) = n , Code-trans {g k} {suc (g k)} (Code-suc-inc-simple {g k}) q

Exercise 20fromCode

fromCode : {x y : O} → Code x y → x ≤ y
fromCode {zer}        {y}          p       = {!!}
fromCode {suc x}      {suc y}      p       = {!!}
fromCode {suc x}      {lim f fmon} (n , p) = {!!}
fromCode {lim f fmon} {suc y} p            = {!!}
fromCode {lim f fmon} {lim g gmon} p       = {!!}

The reference solution uses: ≤-zer ≤-suc-mon ≤-cocone ≤-limiting fst snd

Your solution

Reference solution

fromCode : {x y : O} → Code x y → x ≤ y
fromCode {zer}        {y}          p       = ≤-zer
fromCode {suc x}      {suc y}      p       = ≤-suc-mon (fromCode p)
fromCode {suc x}      {lim f fmon} (n , p) = ≤-cocone (fromCode p)
fromCode {lim f fmon} {suc y} p            = ≤-limiting λ n → fromCode (p n)
fromCode {lim f fmon} {lim g gmon} p       = comparison-lemma (λ k → fst (p k) , fromCode (snd (p k)))

Exercise 21zer?

zer? : (x : O) → x ≈ zer ⊎ ¬ x ≈ zer
zer? zer          = {!!}
zer? (suc x)      = {!!}
zer? (lim f fmon) = {!!}

The reference solution uses: left ≤-zer _,_ right toCode fst

Your solution

Reference solution

zer? : (x : O) → x ≈ zer ⊎ ¬ x ≈ zer
zer? zer          = left  (≤-zer , ≤-zer)
zer? (suc x)      = right λ p → toCode (fst p)
zer? (lim f fmon) = right λ p → toCode (fst p)

Multiplication with natural numbers and with ω#

The purpose of this operation is to help get to ε₀ with fewer proof obligations than when properly setting up full multiplication.

infixl 7 _·ₙ_
_·ₙ_ : O → ℕ → O
x ·ₙ zero   = zer
x ·ₙ succ n = x ·ₙ n + x

Exercise 22≰0⇒≥1

≰0⇒≥1 : {x : O} → ¬ x ≤ zer → uno ≤ x
≰0⇒≥1 = {!!}

The reference solution uses: ≤-zer suc ≤-suc-mon lim ≤-trans ≤-cocone zero

Your solution

Reference solution

≰0⇒≥1 : {x : O} → ¬ x ≤ zer → uno ≤ x
≰0⇒≥1 {zer}        p with p ≤-zer
... | ()
≰0⇒≥1 {suc x}      p = ≤-suc-mon ≤-zer
≰0⇒≥1 {lim f fmon} p = ≤-trans (≤-suc-mon ≤-zer) (≤-cocone (fmon zero))

·ₙ-mon : (x : O) → ¬ x ≤ zer → (n : ℕ) → x ·ₙ n < x ·ₙ succ n
·ₙ-mon x p n = +-mon {x ·ₙ n} {uno} {x} (≰0⇒≥1 p)

_·ω : O → O
x ·ω with zer? x
... | left  x≈zer = zer
... | right x≉zer = lim (λ n → x ·ₙ n) (·ₙ-mon x λ p → x≉zer (p , ≤-zer))

Exponentiation by ω#

Write.

Outlook#

Beyond these first steps with ordinals, the following projects might be interesting.

Defining ordinal multiplication and exponentiation, by implementing the rules listed on the Wikipedia page on ordinal arithmetic
Defining the ordinal number ε₀
Stating and proving that ω ^ ε₀ is the same as ε₀
Defining the numbers ε₁, ε₂, …

Do not expect these exercises to have short solutions—the monotonicity requirement in the lim constructor entails quite a few proof obligations. However, we cannot drop this requirement as else exponentiation is no longer definable: The definition requires a case distinction which is possible only because of the monotonicity requirement.

An extensive discussion is included in the following landmark papers by Tom de Jong, Nicolai Kraus, Fredrik Nordvall Forsberg and Chuangjie Xu: