[FOM] Fwd: invitation to comment

[Jeffrey Sarnat]

On Mon, May 23, 2011 at 9:10 AM, Vaughan Pratt <pratt at cs.stanford.edu>wrote:
>
> [...]
> Epsilon_0 has various representations.  Here's one, due to Lev Beklemishev,
> that should appeal to computer programmers because the only datatypes
> involved are integers and strings, no trees or other such representations of
> Cantor normal form.
>
>
As a computer scientist, I found Cantor normal form for epsilon_0 to be easy
to understand once I realized that exponentiation at base omega is exactly
the multiset ordering from term rewriting theory. If we choose to implement
multisets as lists sorted in descending order, then this becomes even more
straightforward: the empty list is smaller than all non-empty lists, and
non-empty lists are ordered lexicographically by their heads followed by
their tails. Moreover, ordinal addition and multiplication are easy to
explain in terms of their type-theoretic analogs, which makes it easy to
visualize how data structures built up from these three primitives would be
ordered, and why the resulting ordering should be well founded (although
multiplication is technically unnecessary, it is pedagogically helpful to
consider).

My experiences with introducing other computer scientists to the dark art of
ordinal analysis have led me to believe that this approach works well: I can
usually get people to count at least as high as Gamma_0 in about an hours
worth of hand-waiving along these lines. For those who are interested, a
(slightly) more detailed account of this approach can be found in Section
3.1 of my dissertation.

        Jeff Sarnat
        http://www.pps.jussieu.fr/~sarnat/






> Let w be a word over the alphabet N = {0,1,2,...}
> At stage m, beginning from m = 1:
> If w is empty then halt;
> else if the last character of w is 0 then delete it;
> else {
> 1.  Identify the longest suffix of w all of whose characters are at
>    least as large as the last character of w.
> 2.  Decrement the last character of w (and hence of the suffix).
> 3.  Append m copies of the suffix to w.
> }
>
> So for example if initially w = 2102031 then w evolves as follows.
>
> 1: 210203030
> 2: 21020303
> 3: 21020302222
> 4: 21020302221(2221)^4
> 5: 210203022212221222122212220(22212221222122212220)^5
> and so on.
>
> Those for whom C is clearer than English can find further disambiguation at
> http://boole.stanford.edu/bek.c
>
> In http://www.phil.uu.nl/preprints/preprints/PREPRINTS/preprint219.ps.gz
> Beklemishev argues that termination of this process for all words w is
> equivalent to 1-consistency of PA in Elementary Arithmetic as defined there.
>  (I'd say "shows" instead of "argues" were his argument not well above my
> pay grade.)  Separately he also proves its termination by induction on
> epsilon_0.
>
> I would have thought termination of the above process for all w was an
> entirely finitistic matter, so if it isn't then you have my full attention.
>
> I'd be interested to know whether his equivalence result still holds when
> "m copies" is replaced by "2 copies," or even "1 copy," in step 3.
>
> Vaughan Pratt
>
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/fom
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20110524/e2aea472/attachment-0001.html>