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