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.
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 omegas,
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 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-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.