Major Section: MISCELLANEOUS

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:
2 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 `omega`

s,
i.e., `(w^w)^w`

etc. Consider the ``limit'' of all of those stacks,
which we might display as follows.
. . . w w w w wThat 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 representationObserve that the sequence of0 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) ... ...

`e0-ordinalp`

s 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 `car`

s are compared recursively and determines which
is smaller unless the `car`

s are equal, in which case the ordinals in
their `cdr`

s 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.