Tuesday, 17 May 2011

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.


  1. Is PRA+induction up to eptsilon_0 consistent?

  2. Interesting discussion. In an adjacent problem stepping on the fields of Metaphysics (Philosophy of Mind, specially) known as 'gödelian arguments' computabilists tend to echo Voevodsky's spirit by denying that we can even know PA's consistency. This gives them a shot declaring Gödelian Arguments invalid formally. Most detractors of Gödelian Arguments use Gödel's Incompleteness results as their only evidence to the impossibility of PA's consistency being true. (Hayes, LaForte and Ford, clearly do this, but it is a commonplace even between those who hold at least some version of a Gödelian Argument, but criticize others such as Selmer Bringsjord, H. Putnam, ...)

    Well, anyway, it is a delicate thing to state that it is a metaphysical fact and maybe a natural fact, if not a physical one, that THERE IS actually a phenomenon (the cognitive features of the mind doing/contemplating Arithmetic) that is not or has some access to non-finitary resources. Cognitive Sciences hold computabilism which implies that there's not any higher Turing Computability going on the in brain and mind. Turing Computability imposes certain restrictions on what infinities can be legitimately presupposed.

    So, by a long trip, I think that there's a case for those thinking that PA CAN be inconsistent.


  3. Corrections:

    "Cognitive Sciences hold computabilism which implies that there's not any MORE POWERFUL THAN Turing Computability going on IN THE brain and mind. Turing Computability imposes certain restrictions on what infinities can be legitimately presupposed to hold any mathematical truth ACCEPTABLE EVEN TO INTUITIONISTS."

  4. Franklin,
    Good question! And I'd add: is PRA+induction up to epsilon_0 *sound*? (It may be consistent but not sound.) Ultimately, if Voevodsky wants to dismiss Gentzen's proof, he would have to have arguments to question the soundness of PRA+induction up to epsilon_0. From what I gather, mathematicians by and large trust the soundness of the system, but as philosophers we are allowed to ask such questions... (speaking for myself, I don't know whether you are a philosopher).

    Anonymous, thanks for mentioning the connection with debates in phil mind regarding Godel's theorem. Certainly relevant in this context too.

  5. I find it bizarre that Voevodksy would be expected to give a precise formal statement of a well-known result like Goedel's 2nd incompleteness theorem or risk people thinking he "displayed a complete lack of understanding" of the subject, or is "dismissing Gentzen's proof".

    Voevodsky is a great mathematician, and if you go to talks by great mathematicians you'll find they often run roughshod over well-known details in their pursuit of challenging new ideas. They don't feel the need to prove their ability to parrot standard results. They've got bigger things in mind.

    Voevodsky is working on integrating ideas from homotopy theory into mathematical logic. This gives rise to a new subject that some people are now starting to call "homotopy type theory". It's part of the switch from set theory towards infinity-category theory, since homotopy types are essentially the same as infinity-groupoids.

    Anyone who wants to understand where mathematical logic is heading in the 21st century needs to pay attention to this stuff.

  6. @John,

    Indeed, in the end my conclusion was that Voevodsky's comment concerning PA was for the most part tangential within the bigger picture of the homotopy project. My third post on the 'affair' elaborates on this point:


  7. By the way, I've been feeling sorry that I came across as a bit fierce in my comment above. When I saw the phrase "he seems to display a complete lack of understanding of Goedel's incompleteness results," it made me see red, despite all the qualifiers it was couched in, such as "at least according to some". I got the feeling that "some" - I'm not sure who - were criticizing minutia while ignoring the amazing developments occuring right before their eyes.

    This of course is common in academia, but also elsewhere. I just watched a great video documentary about Thelonious Monk on YouTube. It's blisteringly clear that he was smarter than all the journalists commenting on him, who seemed to see him mainly as an eccentric who wore funny hats.

    Your June 6 post makes me much happier.

    There are huge and fascinating philosophical questions involved in the homotopification of logic, and I hope philosophers get in there and explore them.