Major Section: PROGRAMMING Using the nonnegative integers and
lists we can represent the ordinals up to epsilon-0. The ordinal
representation used in ACL2 has changed as of Version_2.8 from
that of Nqthm-1992, courtesy of Pete Manoilios and Daron Vroon;
additional discussion may be found in ``Ordinal Arithmetic in
ACL2'', proceedings of ACL2 Workshop 2003, ACL2's notion of
ordinal was 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 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 nu