[FOM] "Salvaging" Voevodsky's talk

[Timothy Y. Chow]

Though Martin has decided to end the recent discussion about Voevodsky's 
talk, the consistency of PA, etc., I have what I think are a couple of 
fresh comments on the subject.

I thought it would be a good exercise to listen to Voevodsky's lecture 
with as charitable a posture as possible, so I did that just now.

If we screen out all the mistakes and misleading statements, then I think 
there is still some reasonable content that remains.  For example, I would 
paraphrase Voevodsky as saying the following: Adopting the assumption that 
PA is inconsistent doesn't immediately lead to disaster.  One has to 
reject some things, e.g., the claim that every first-order formula defines 
a set of integers, and the claim that induction holds up to epsilon_0, but 
these are things that one can learn to live with.  (Once Voevodsky digests 
Harvey's Bolzano-Weierstrass statement, I think he will respond by saying 
that an inconsistency in PA would force us to give up belief in 
"arbitrarily complicated" sequences of rationals, but again this is 
something he would be prepared to live with.)

This much I think is true, but not necessarily well known, so it's not so 
unreasonable for Voevodsky to try to convey this to a general audience 
(though the manner in which he did so was unfortunate in many ways).

The last part of his lecture argues that constructive type theory is a 
better approach to foundations than traditional approaches are, because it 
is more robust to possible contradictions.  I had trouble trying to 
"salvage" this part of the talk.  I can agree that type theory has some 
potential practical advantages, and indeed we see that the modern proof 
assistants that are based on type theory seem to be overtaking Mizar.  
However, I don't see how type theory is any better suited to a situation 
where there might be some unknown, infeasibly large contradiction lurking 
somewhere.  Voevodsky still wants to draw some lines in the sand, saying 
that certain fragments of reasoning are "reliable," and I don't see how 
type theory is any better or worse than first-order logic from this point 
of view.  If someone sees a plausible argument here, based on what 
Voevodsky said or otherwise, I'd be interested in hearing it.  It seems 
that some of the work that has been done on paraconsistent logic should be 
relevant here, but I'm not too familiar with that subject.

Tim