[FOM] comment on the video of the lecture by Voevodsky at IAS
pratt at cs.stanford.edu
Tue May 17 02:42:45 EDT 2011
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.
More information about the FOM