Recursion and Induction: The Ordinals

The ordinals are an extension of the naturals that captures an essential notion of ordering. They were invented by Georg Cantor in the late nineteen century. While controversial during Cantor's lifetime, ordinals are among the richest and deepest mines of mathematics. We only scratch the surface here.

Think of each natural number as denoted by a sequence of strokes, i.e.,

0 0 1 ∣ 2 ∣ ∣ 3 ∣ ∣ ∣ 4 ∣ ∣ ∣ ∣ … … ω ∣ ∣ ∣ ∣ ∣ …

The limit of that progression is the ordinal *ω*, an infinite sequence of
strokes.

Ordinal addition is just concatenation. Observe that adding one to the front
of *ω* produces *ω* again, which gives rise to a standard
definition of *ω*: the least ordinal such that adding another stroke at
the beginning does not change the ordinal.

We denote by *ω* + *ω* or *ω*×2 the “doubly infinite”
sequence that we might write as follows.

ω × 2 ∣ ∣ ∣ ∣ ∣ … ∣ ∣ ∣ ∣ ∣ …

One way to think of *ω*×2 is that it is obtained by replacing each
stroke in 2 (| |) by *ω*. Thus, one can imagine *ω*×3, *ω*×4, etc., which
leads ultimately to the idea of *ω*×*ω*, the ordinal obtained by
replacing each stroke in *ω* by *ω*. This is also written as *ω*^2.

ω^2 ∣ ∣ ∣ ∣ ∣ … ∣ ∣ ∣ ∣ ∣ … ∣ ∣ ∣ ∣ ∣ … ∣ ∣ ∣ ∣ ∣ … ∣ ∣ ∣ ∣ ∣ … …

We can analogously construct *ω*^3 by replacing each stroke in
*ω* by *ω*^2 (which, it turns out, is the same as replacing each
stroke in *ω*^2 by *ω*). That is, we can construct *ω*^3
as *ω* copies of *ω*^2, and so on. This ultimately suggests
*ω*^*ω*. We can then stack *ω*s, i.e.,
*ω*^(*ω*^*ω*), etc. Consider the limit of all of those stacks,

`
ω^(ω^(ω^(ω^(ω^(ω^(ω^ … )))))).
`

That limit is *ε_0*. (As the subscript suggests, there are lots
more ordinals! But ACL2 stops with *ε_0*.)

Despite the plethora of ordinals, we can represent all the ones below
*ε_0* in ACL2, using lists. Below we begin listing some ordinals up
to *ε_0*; the reader can fill in the gaps at his or her leisure. We
show in the left column the conventional notation and in the right column the
ACL2 object representing the corresponding ordinal.

ordinal | ACL2 representation | |

0 | 0 | |

1 | 1 | |

2 | 2 | |

3 | 3 | |

… | … | |

ω |
((1 . 1) . 0) | |

ω + 1 |
((1 . 1) . 1) | |

ω + 2 |
((1 . 1) . 2) | |

… | … | |

ω×2 |
((1 . 2) . 0) | |

(ω×2) + 1 |
((1 . 2) . 1) | |

… | … | |

ω×3 |
((1 . 3) . 0) | |

(ω×3) + 1 |
((1 . 3) . 1) | |

… | … | |

ω^2 |
((2 . 1) . 0) | |

… | … | |

ω^2 + ω×4 + 3 |
((2 . 1) (1 . 4) . 3) | |

… | … | |

ω^3 |
((3 . 1) . 0) | |

… | … | |

ω^ω |
((((1 . 1) . 0) . 1) . 0) | |

… | … | |

ω^ω + ω^99 + ω×4 + 3 |
((((1 . 1) . 0) . 1) (99 . 1) (1 . 4) . 3) | |

… | … | |

ω^(ω^2) |
((((2 . 1) . 0) . 1) . 0) | |

… | … | |

ω^(ω^ω) |
((((((1 . 1) . 0) . 1) . 0) . 1) . 0) | |

… | … |

We say an ordinal is “finite” if it is not a cons and we define
`(o-finp x)` to recognize finite ordinals. Of course, if `x` is an
ordinal and finite, it is a natural number. But by defining `o-finp`
this way we ensure that if an ordinal is not finite we can recur into it with
`cdr`.

To manipulate ordinals we define functions that access the first exponent, the first coefficient, and the rest of the ordinal:

(defun o-first-expt (x) (if (o-finp x) 0 (car (car x)))) (defun o-first-coeff (x) (if (o-finp x) x (cdr (car x)))) (defun o-rst (x) (cdr x))

For example, if `x` is the representation of *ω*^e×*c* + *r*
then `(o-first-expt x)` is *e*, `(o-first-coeff x)` is *c* and
`(o-rst x)` is *r*.

Here is the definition of `o-p`, the function that recognizes ordinals.

(defun o-p (x) (if (o-finp x) (natp x) (and (consp (car x)) (o-p (o-first-expt x)) (not (equal 0 (o-first-expt x))) (natp (o-first-coeff x)) (< 0 (o-first-coeff x)) (o-p (o-rst x)) (o< (o-first-expt (o-rst x)) (o-first-expt x)))))

(The ACL2 definition is syntactically different but equivalent.)

The function `o<` is the “less than” relation on ordinals. We show its
definition below. But study the definition of `o-p` first. It says that
an ordinal is a list of pairs, terminated by a natural number. Each pair
`(e . c)` consists of an exponent `e` and a coefficient `c` and
represents (*ω*^e)×*c*. The exponents are themselves ordinals
and the coefficients are non-0 naturals. Importantly, the exponents are
listed in strictly descending order. The list represents the ordinal
sum of its elements plus the final natural number. Thus, ordinals can be
viewed as polynomials.

By insisting on the ordering of exponents we can readily compare two
ordinals, using `o<` below, in much the same way we can compare
polynomials.

(defun o< (x y) (if (o-finp x) (or (not (o-finp y)) (< x y)) (if (o-finp y) nil (if (equal (o-first-expt x) (o-first-expt y)) (if (equal (o-first-coeff x) (o-first-coeff y)) (o< (o-rst x) (o-rst y)) (< (o-first-coeff x) (o-first-coeff y))) (o< (o-first-expt x) (o-first-expt y))))))

(The ACL2 definition is syntactically different but equivalent.)

**Problem 90. ** Which is smaller, ordinal a or ordinal b?

- a =
`23`, b =`100` - a =
`1000000`, b =`((1 . 1) . 0)` - a =
`((2 . 1) . 0)`, b =`((1 . 2) . 0)` - a =
`((3 . 5) (1 . 25) . 7)`, b =`((3 . 5) (2 . 1) . 3)` - a =
`((((2 . 1) . 0) . 5) . 3)`, b =`((((1 . 1) . 0) . 5) (1 . 25) . 7)`

**Problem 91. ** The

(implies (and (natp i1) (natp j1) (natp i2) (natp j2)) (and (o-p (m2 i1 j1)) (iff (o< (m2 i1 j1) (m2 i2 j2)) (if (equal i1 i2) (< j1 j2) (< i1 i2)))))

The crucial property of `o<` is that it is *well-founded on the
ordinals*. That is, there is no infinite sequence of ordinals, *x_i* such
that … *x_3* `o<` *x_2* `o<` *x_1* `o<` *x_0*.

**Problem 92. ** What is the longest decreasing chain of ordinals starting from the ordinal

**Problem 93. ** Construct an infinitely descending

**Problem 94. ** Prove that

Caution: Using the logical machinery we have developed here, it is not
possible to state that `o<` is well-founded on the ordinals: that
requires an existential quantifier and infinite sequences. However,
it can be done in a traditional set theoretic setting. That is, the
theorem that `o<` is well-founded is a “meta-theorem”, it can be
proved about our system but it cannot be proved within our system.

Our definitional and induction principles are built on the assumption that
`o<` is well-founded on the ordinals recognized by `o-p`. Thus, if
some ordinal measure of the arguments of a recursive function decreases
according to `o<` in every recursive call, the recursion cannot go on
forever.

The representation of ordinals described here is a version of Cantor's
Normal Form. See

Next: