[FOM] Voevodsky

[Robert Black]

I only watched this once, and I didn’t bother with the questions. but I 
do think FOMers have been too quick to jump at his (surely 
deliberately!) outrageous misstatement of Gödel’s results and too 
unwilling to think what he might mean.

There is an old tradition according to which mathematics has to be 
*absolutely indubitable*. *We* can make mistakes in thinking we have a 
proof when we haven’t really got one, but *mathematics* can’t make 
mistakes: if we do have a proof then what we have proved is true (and 
known by us a priori). (I go no further into the problems this raises.) 
Genuine mathematical results have to be in some sense absolutely 
indubitable.

Now think of the Hilbert programme in this context. Disputably 
simplifying: Pi_1 statements are capable of truth or falsity 
(‘truth-apt’ in the ugly philosophical jargon). They are true/false iff 
provable to be such with finitary reasoning (which we can, simplifying, 
take to be PRA, supposed to be indubitable). A proof in PRA that some 
infinitary system is consistent would (by a familiar argument) show its 
Pi_1 theorems to be (indubitably) true. So if we have it, for PA say, we 
will thereby guarantee the indubitable truth of all the pi_1 theorems of 
PA. Gödel shows us that we *can’t* have it.

Now what I take Voevodsky to be saying: we can coherently doubt the 
consistency of PA. This seems obviously true, since if it weren’t, the 
Hilbert programme for PA would have been incoherent. Further, although 
there are proofs of the consistency of PA, for each such proof we can 
doubt its cogency. (The examples Voevodsky considers are firstly the 
obvious proof that the axioms of PA are true and the proof rules 
preserve truth (formalized, this is the proof of Con(PA) in second-order 
arithmetic) where it is possible to doubt whether we really understand 
induction over arithmetically definable but non-recursive properties, or 
Gentzen-style proofs where it is possible to doubt whether the ordinals 
less than epsilon_0 (modulo some suitable notation) are really 
well-ordered. This seems to me correct. (I don’t mean I *do* doubt these 
things - I don’t - but one *can* coherently doubt them.) The consistency 
of PA is not absolutely indubitable.

But of course if PA is inconsistent then anything is provable from it, 
so it follows that proving something from PA doesn’t make it absolutely 
indubitable.

Now that doesn’t worry *me* at all, because I don’t think that 
mathematical theorems have to be indubitable. I’m confident (without 
certainly) that PA (or for that matter ZF) is consistent (indeed true!), 
and I’m happy to let my mathematical knowledge be fallible. But suppose 
you’re more of a traditionalist, and you’re *not* happy with that.

I don’t think the point is that PA *might turn out* to be inconsistent. 
Of course it might, and if it did, we would look at the induction axioms 
used, try to establish what was peculiar about them, and then weaken PA 
accordingly. That’s fantasy land, and is not going to happen.

Rather the point is that we want to know now with *absolute certainty* 
that the results we’ve deduced from PA have to be true *even if PA is 
inconsistent*. And then the claim was (and here I lost him) that by 
considering rules of deduction other than the usual ones we could show 
in some cases (not all) that the theorems would have to be true even if 
the axioms were inconsistent. We would get a sort of Hilbert programme 
bypassing consistency.

I’d be amazed if such a programme were to go through, and we need to be 
told exactly which sentences are truth-apt, and what their truth 
consists in, but is there any reason why it’s obviously silly?

Robert
-- 
Robert Black