[FOM] Fwd: invitation to comment

[William Tait]

On May 23, 2011, at 2:10 AM, Vaughan Pratt wrote:

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

That is a misunderstanding of what I wrote. It is Gentzen's finitist (or lets say quasi-finitist) argument that induction up to epsilon_0 is valid of which I am claiming that, spelled out, requires all of PA. That surely should not surprise you. 

Bill Tait