## E0-ORDINALP

a recognizer for the ordinals up to epsilon-0
```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
w
```
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-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.