I'm annoyed by the careless use of the word "proof" in Voevodsky's lecture. Of course, in the context of everyday mathematical discussions, it is normally sufficiently clear what one means by "proof" (it usually means something like "argument that is formalizable in ZFC"; even though I agree with Timothy Chow that most mathematicians wouldn't be able to explain exactly what ZFC is, they are nevertheless trained to recognize certain things as being "proofs" and I believe that those things that mathematicians normally recognize as proofs correspond to "proofs in ZFC"). But in the context of a discussion about foundations, it is far from clear what "proof" means and it is good practice to be more precise (proof in PRA? proof in PA? proof in ZFC? what?). There is no absolute notion of proof that, once presented, eliminates any possibility of doubt forever.

There doesn't seem to be anything new/interesting about Voevodsky's lecture. Anyone that is mildly educated about foundations has already entertained the question "what if ZFC is inconsistent?" or "what if PA is inconsistent?"; questions like that come around, from time to time, in any forum that discusses foundations of mathematics.

As Voevodsky mentioned, it is possible to present a constructive proof that an inconsistency in PA leads to an ever decreasing sequence in epsilon_0 (he mentioned a proof by Gentzen; there is also one by Gödel himself). Such proof convinces me that PA is consistent, as I find the idea of constructing an ever decreasing sequence in epsilon_0 rather crazy. But, of course, one can say "so what? I'm skeptical" (of course, one could also say that about any proof).

Sadly, Voevodsky's proposal about what to do if PA turns out to be inconsistent seems to me somewhat silly. If I understand him correctly, what he proposes is that we should have a system which is inconsistent, but we should also have some algorithm which separates "unreliable proofs" from "reliable proofs" (in such a way, I suppose, that there shouldn't be a "reliable proof" of both P and not(P); otherwise, I cannot understand what "reliable" could possibly mean). This "two step" scheme doesn't help at all. Instead of having "proofs" that can prove both P and not(P) and "reliable proofs" that do not prove both P and not(P), we could just restrict the term "proof" to the "reliable proofs". But, if one assumes the existence of an algorithm that decides whether something is or isn't a proof, and if the system is sufficiently complex to allow for interesting mathematics to be done within it, then Gödel's arguments would again present the usual obstruction for the existence of finitary proofs of consistency.

19more comments