[FOM] "Salvaging" Voevodsky's talk
Timothy Y. Chow
tchow at alum.mit.edu
Sat Jun 4 18:51:22 EDT 2011
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.
More information about the FOM