[FOM] Fwd: invitation to comment

[Andreas Weiermann]

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

Dear Vaughan,

I think it is fairly easy to show that the equivalence does not hold
when "m copies" is replaced by "2 copies," or even "1 copy," in step
3.

It is even known what happens if one replaces
"m copies" by "f(m) copies" for sublinear functions f.
This is a classical and well known example for a provability
phase transition.

[For the sake of completeness let me mention
the result in full detail. For alpha not exceeding
epsilon_0 let f_alpha(i) be
log^{H_alpha^{-1}(i)}(i) where H_alpha^{-1} stands for the functional
inverse of the Hardy function of level alpha and
log^n denotes the n-th iterate of the log function.
Then (PA proves Termination of the
worm principle with respect to f_alpha) iff alpha< epsilon_0.]

Best,
Andreas Weiermann



----------------------------------------------------------------
This message was sent using IMP, the Internet Messaging Program.