[FOM] Fwd: invitation to comment

[Vaughan Pratt]

On 5/22/2011 10:02 AM, William Tait wrote:
> Vaughan points out that we can prove Con_{PA} in ordinary mathematics,
> for example using no more than PRA with the addition of a certain
> quantifier-free version of induction up to epsilon_0 (using some
> `standard' ordering of the natural numbers to represent the ordinals
> epsilon_0). But I think it unlikely that Voevodsky is unaware of this.

On the basis of what VAV said in his lecture I inferred the opposite. 
He would need to go into considerably more detail to dissuade me of this.

> But, like many other 'intuitive' arguments in the finitist literature,
> examination shows it to be just an incomplete proof in the ordinary
> sense, and one such that, when the details are filled in, is seen to
> involve non-finitist mathematics--- in Gentzen's case full PA.

I'd be very interested to see how T + Con(PA) entails full PA where T is 
less than PA, e.g. PRA.

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