a recognizer for the ordinals up to epsilon-0

Using the nonnegative integers and lists we can represent the ordinals up to epsilon-0. The ACL2 notion of ordinal is the same as that found in nqthm-1992 and both are very similar to the development given in ``New Version of the Consistency Proof for Elementary Number Theory'' in The Collected Papers of Gerhard Gentzen, ed. M.E. Szabo, North-Holland Publishing Company, Amsterdam, 1969, pp 132-213.

The following essay is intended to provide intuition about ordinals. The truth, of course, lies simply in the ACL2 definitions of e0-ordinalp and e0-ord-<.

Very intuitively, think of each non-zero natural number as by being denoted by a series of the appropriate number of strokes, i.e.,

0             0
1             |
2             ||
3             |||
4             ||||
...           ...
Then ``omega,'' here written as w, is the ordinal that might be written as
w             |||||...,
i.e., an infinite number of strokes. Addition here is just concatenation. Observe that adding one to the front of w in the picture above produces w again, which gives rise to a standard definition of w: w is the least ordinal such that adding another stroke at the beginning does not change the ordinal.

We denote by w+w or w*2 the ``doubly infinite'' sequence that we might write as follows.

w*2           |||||... |||||... 
One way to think of w*2 is that it is obtained by replacing each stroke in 2 (||) by w. Thus, one can imagine w*3, w*4, etc., which leads ultimately to the idea of ``w*w,'' the ordinal obtained by replacing each stroke in w by w. This is also written as ``omega squared'' or w^2, or:
w             |||||... |||||... |||||... |||||... |||||... ...
We can analogously construct w^3 by replacing each stroke in w by w^2 (which, it turns out, is the same as replacing each stroke in w^2 by w). That is, we can construct w^3 as w copies of w^2,
 3              2       2       2       2
w              w  ...  w  ...  w  ...  w ... ...
Then we can construct w^4 as w copies of w^3, w^5 as w copies of w^4, etc., ultimately suggesting w^w. We can then stack omegas, i.e., (w^w)^w etc. Consider the ``limit'' of all of those stacks, which we might display as follows.
That is epsilon-0.

Below we begin listing some ordinals up to epsilon-0; the reader can fill in the gaps at his or her leisure. We show in the left column the conventional notation, using w as ``omega,'' and in the right column the ACL2 object representing the corresponding ordinal.

  ordinal            ACL2 representation

0 0 1 1 2 2 3 3 ... ... w '(1 . 0) w+1 '(1 . 1) w+2 '(1 . 2) ... ... w*2 '(1 1 . 0) (w*2)+1 '(1 1 . 1) ... ... w*3 '(1 1 1 . 0) (w*3)+1 '(1 1 1 . 1) ... ...

2 w '(2 . 0) ... ...

2 w +w*4+3 '(2 1 1 1 1 . 3) ... ...

3 w '(3 . 0) ... ...

w w '((1 . 0) . 0) ... ...

w 99 w +w +4w+3 '((1 . 0) 99 1 1 1 1 . 3) ... ...

2 w w '((2 . 0) . 0)

... ...

w w w '(((1 . 0) . 0) . 0) ... ...

Observe that the sequence of e0-ordinalps starts with the nonnegative integers. This is convenient because it means that if a term, such as a measure expression for justifying a recursive function (see e0-ord-<) must produce an e0-ordinalp it suffices for it to produce a nonnegative integer.

The ordinals listed above are listed in ascending order. This is the ordering tested by e0-ord-<.

The ``epsilon-0 ordinals'' of ACL2 are recognized by the recursively defined function e0-ordinalp. The base case of the recursion tells us that nonnegative integers are epsilon-0 ordinals. Otherwise, an epsilon-0 ordinal is a cons pair (o1 . o2), where o1 is a non-0 epsilon-0 ordinal, o2 is an epsilon-0 ordinal, and if o2 is not an integer then its car (which, by the foregoing, must be an epsilon-0 ordinal) is no greater than o1. Thus, if you think of a (non-integer) epsilon-0 ordinal as a list, each element is an non-0 epsilon-0 ordinal, the ordinals are listed in weakly descending order, and the final cdr of the list is an integer.

The function e0-ord-< compares two epsilon-0 ordinals, x and y. If both are integers, e0-ord-< is just x<y. If one is an integer and the other is a cons, the integer is the smaller. Otherwise, the ordinals in their cars are compared recursively and determines which is smaller unless the cars are equal, in which case the ordinals in their cdrs are compared.

Fundamental to ACL2 is the fact that e0-ord-< is well-founded on epsilon-0 ordinals. That is, there is no ``infinitely descending chain'' of such ordinals. See proof-of-well-foundedness.