Voevodsky: "The consistency of PA is an open problem"

UPDATE: This is the first post in a series of three on the same topic; the second one is here and the third one is here.

Those of you who subscribe to the FOM list have certainly noticed that it's been "a lot more interesting than usual", in the terms of Archean Toby Meadows. For those of you who do not subscribe to the list (perhaps precisely for the reasons implicated in Toby's remark!), here's a summary (but you can read the messages yourself at the FOM archives for this month). There are some videos of lectures by Fields medalist Voevodsky made available on the internet, where (at least according to some) he seems to display a complete lack of understanding of Goedel's incompleteness results (here and here). In Neil Tennant's words:

He stated the theorem as follows (written version, projected on the screen):

It is impossible to prove the consistency of any formal reasoning system which is at least as strong as the standard axiomatization of elementary number theory ("first order arithmetic").

So he failed to inform his audience that the impossibility that Goedel actually established was the impossibility of proof-in-S of a sentence expressing the consistency of S, for any consistent and sufficiently strong system S.

As we know, Gentzen's proofs of the consistency of PA are among the most important results in proof-theory, second only to Goedel's results themselves and perhaps Prawitz' normalization results. (For a great overview of Gentzen's proofs, see von Plato's SEP entry.) What I find most astonishing about Gentzen's proofs, based on transfinite induction, is that the theory obtained by adding quantifier free transfinite induction to primitive recursive arithmetic is not stronger than PA, and yet it can prove the consistency of PA (it is not weaker either, obviously; they just prove different things altogether). One may raise eyebrows concerning transfinite induction (and apparently this is what lies behind Voevodsky's dismissal of Gentzen's results), but apparently most mathematicians and logicians seem quite convinced of the cogency of the proof. In Vaughan Pratt's words (he's my favorite regular contributor to FOM, and we've corresponded on a number of interesting topics):

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?

So Voevodsky seems to seriously entertain the possibility of PA's inconsistency. Is it because he doesn't understand Goedels' results, or Gentzen's results, or both? Or is there something else going on? Even granting that a great mathematician is not necessarily savvy on such hair-splitting foundational issues, as pointed out by Juliette Kennedy, "that Voevodsky's coworkers in Univalent Foundations are Awodey and Coquand seals the deal for me." In other words, we have reasons to believe that Voevodsky should know his way around even in foundational issues (his website linked above says that "he is working on new foundations of mathematics based on homotopy-theoretic semantics of Martin-Lof type theories.")

H. Friedman reports having sent him a letter asking for clarifications, in particular "how you view the usual mathematical proof that Peano Arithmetic is consistent, and to what extent and in what sense is "the consistency of Peano Arithmetic" a genuine open problem in mathematics." So the debate is likely to continue, and (needless to say) it clearly has all kinds of important philosophical implications.