Thursday, 9 June 2011

Latest news on the 'inconsistency of PA' affair

UPDATE: I'm adding a few small changes to the original post, which were suggested by Steve Awodey.

(Cross-posted at NewAPPS.)

As previously reported (here and here), over the last few weeks there has been a heated debate within the foundations of mathematics community on what appeared to be a controversial statement by Fields medalist V. Voevodsky: the inconsistency of PA is an open problem. But what seemed at first instance a rather astonishing statement has become more transparent over the last couple of days, in particular thanks to posts by Bill Tait and Steve Awodey over at the FOM list. (Moreover, I’ve had the pleasure of discussing the matter with Steve Awodey in person here in Munich, in conversations which have been most informative.)

First, it might be useful to clarify some of the basic points of the program Voevodsky and others are engaged in. A few years back, Awodey established a neat correspondence between homotopy theory (Voevodsky’s main topic of research) and Martin-Löf’s constructive type theory. The result then led to the project of providing foundations for mathematics within the newly founded framework of Homotopy Type Theory and Univalent Foundations. One of the distinctive characteristics of the framework is that it is based on the notion of a continuum (homotopy is a branch of topology), while the more familiar set-theoretical framework is based on the notion of discrete elements (sets). Moreover, constructive type-theory is, well, constructive, so it is much more straightforward to maintain ‘epistemic control’ over proofs. At the time that Awodey’s correspondence results became known, independently, Voevodsky had also been interested in related ideas, and they are now actively collaborating on it (Martin-Löf is also involved, as is Thierry Coquand). Crucially, given its very distinctive starting point (continuity vs. discreteness) and its constructive nature, the framework could provide a truly revolutionary approach to the foundations of mathematics.

Now, within the bigger picture of things, the consistency of PA is actually a tangential, secondary issue. Voevodsky’s seemingly polemic statement concerning the potential inconsistency of PA in fact seems to amount to the following: all the currently available proofs of the consistency of PA in fact rely on the very claim they prove, namely the consistency of PA, on the meta-level. (S. Awodey adds that it is a consequence of Gödel's results that all proofs of consistency of PA must use methods that are stronger than PA in the meta-language.) So if PA was inconsistent, these proofs would still go through; in other words, there is a sense in which such proofs are circular in that they presuppose the very fact that they seek to prove. I raised a similar point before in comments here: if PA was unsound (which it would be if it were inconsistent), it might be able prove its consistency even if it is actually inconsistent (which also means that Hilbert’s original goal may have had a suspicious circular component all along). Now, we know by Gödel that PA cannot prove its own consistency, but the proofs of the consistency of PA available all seem to presuppose the consistency of PA (on the meta-level), so it boils down to roughly the same situation of epistemic uncertainty. Bill Tait sums up this general point in his latest message to FOM:

I understand him [Voevodsky] to be saying the following: PA is just a formal system and if it is inconsistent, then none of its formal deductions are reliable: false things can be proved without an explicit inconsistency appearing. He wants to say that this will not happen in type theory: the 'proofs' of a sentence \phi in type theory are not just strings of symbols, but are objects of type \phi that we actually construct and we can check that we have made a proper construction of such an object (a pair, a function, etc.). So even if there is an inconsistency in the large, individual proofs in type theory can be checked for reliability. For example, to see that a particular term (proof) t of type \forall x \phi(x) really yields a function of that type, one need 'only' to show that tn computes to an object of type \phi(n) for each number n.

So it would seem that the main conclusion to be drawn from these debates, and as pointed out by Steve Awodey in one of his messages to FOM, is that the consistency of PA is really a minor, secondary issue within a much broader and much more ambitious new approach to the foundations of mathematics. Time will tell what will come out of it, but given the brilliancy of the people involved in the project and its innovative character, we can all look forward to the results to come. For those who would like to know more and keep track of the project, their website is:

www.homotopytypetheory.org

4 comments:

  1. Sorry to sound argumentative, but the problem is still that:

    "it is a consequence of Gödel's results that all proofs of consistency of PA must use methods that are stronger than PA in the meta-language."

    just isn't true. No system weaker than, or equivalent to, PA can prove the consistency of PA, but formal systems of arithmetic aren't linearly ordered. So the quoted claim above doesn't follow.

    At any rate, the repeated insistence that this was just a minor point, and the real issue is the homotopy theory, just seems fishy. If the inconsistency of PA weren't a serious issue, then why highlight it at the 80th anniversary of the IAS (which is obviously the sort of venue that would attract attention)? Why give the talk at all, and include all of the condescending comments about philosophical nonsense surrounding Goedel's theorem, if this weren't meant to be taken in exactly the tone it was presented in?

    It still just sounds like backpedalling and @$$covering after Voevodsky demonstrated a profound lack of understanding of traditional foundations of mathematics - a disturbing lack, given that he is now working on alternatives to this very tradition.

    ReplyDelete
  2. Hi Roy,

    Yes, I was also a bit puzzled by Awodey's comment concerning the need for methods stronger than PA on the meta-level; in my first post on the topic, I mentioned specifically that the system with which Gentzen formulated his proof of the consistency of PA is not stronger than PA itself. But who am I to contest somebody like Steve? :) I'm wondering how the meta-language thing would make the difference, I don't see how it would follow from Godel's results.

    For the rest, I don't really know whether it was bad rhetoric, whether it was a bad choice of topic for a talk for the general audience, plain ignorance, or what. I just thought it would be interesting to offer something like the bigger picture of the project, after talking to Steve Awodey about it; the bigger picture thing sounded very interesting, I must say. Of course, I'm also partial towards constructive type theory, having been a student of Goran Sundholm and all, and tend to like frameworks based on continuity rather than discreteness (so anything topology-related). But I agree with you that it is still utterly unclear what V. was up to during that lecture...

    ReplyDelete
  3. Let me add a clarification: the point of this post was precisely to draw attention to the larger project of Homotopy Type Theory. I feel we've been focusing too much on those lectures by Voevodsky, while there is already plenty of material available which might help us understand the larger context.

    Personally, I still think that the lectures were rather misleading, in particular in that they seemed to convey the idea that the consistency of PA was a central question (which, apparently, it isn't). But clearly the lectures alone are not sufficient for us to draw general conclusions. I haven't had the time to check the material in detail yet (and I doubt that I would understand much of it from just a quick look!), but I'm more than convinced that we are dealing with something of substantial interest much beyond the infamous lectures.

    ReplyDelete
  4. A couple things:

    First off, the tone of my post above might have been a bit inappropriate. For that I apologize.

    Also, some clarification is perhaps in order. I did not intend my comments to imply that there is anything 'fishy' about Voevodsky's (and others) work on homotopy theory, nor did I intend to suggest that the homotopy theory work isn't more important than the talk on inconsistency that Voevodsky gave (since it is clear both that the foundational work on homotopy theory is important and interesting, and in addition it is clear that this is where Voevodsky and others think the real substantial insights are to be found).

    All I meant to express by the claim that the comment in question was 'fishy' was this: Even if the stuff about inconsistency proofs isn't important to the larger project in foundations that Voevodsky and others are pursuing, this doesn't mean we need to give the talk a pass and ignore it. Some of the comments regarding the Voevodsky 'affair' seem to suggest that it is somehow innappropriate to focus attention on the less important material on inconsistency. On the contrary, I think we can (and should) multi-task, appreciating the excellent work on homotopy theory while simultaneously critiquing the (in my opinion not as excellent) talk on inconsistency.

    Nevertheless, I applaud Catarina's attempt to focus our attention on the homotopy itself, bringing some balance to the discussion. So now that my apology and clarifications are out of the way, back to our regularly scheduled programming.

    ReplyDelete