[FOM] comment on the video of the lecture by Voevodsky at IAS

[Vaughan Pratt]

On 5/16/2011 2:52 PM, William Messing wrote:
> Unlike Neil Tennant, I was not unhappy with Voevodsky's lecture. His
> point was not to give an expository lecture on Goedel's work of 80 years
> ago. It is clear to me that he could have stated Goedel's second
> incompleteness theorem in a completely rigorous manner. This was not the
> point of his lecture. Rather it was to address the question of how
> mathematics can and will survive if it is found that first order
> arithmetic is not consistent. [...]
> Voevodsky is not a fool

I watched the video and landed on Neil's (et al) side here.  Voevodsky 
dismissed Gentzen's proof of the consistency of PA with nothing more 
than a wave of one hand, and immediately proceeded to wring both hands 
over the supposedly likely prospect of its inconsistency.

One can only imagine that he arrived at this position by mistaking PA 
for some extremely powerful system of mathematics, when the reality is 
that it can't even prove the existence of busy beaver functions (and 
much less) that any computer scientist would have no trouble believing in.

Since Gentzen's proof is a reasonably straightforward induction on 
epsilon_0 in a system tailored to reasoning not about numbers under 
addition and multiplication but about proofs, one can only imagine 
Voevodsky rejects Gentzen's argument on the ground that Goedel's result 
must surely show that no plausible proof of the consistency of PA can 
exist, hence why bother thinking about any such proof?

I confess that my confidence in Gentzen's proof is enhanced by the 
representation of epsilon_0 as the set of finite trees linearly ordered 
in two natural ways, one giving it the order type omega (witnessing its 
countability) and the other the order type epsilon_0.

Paraphrasing Oscar Wilde's Lady Bracknell, to lose ZF to inconsistency 
may be regarded as a misfortune; to lose PA as well looks like carelessness.

Vaughan Pratt