Here we go again: "PA is inconsistent" (Edward Nelson)

UPDATE October 1st: Nelson withdraws his claim.

Readers probably recall the 'Voevodsky affair' of a few months ago (as reported here and in subsequent posts), prompted by Voevodsky's claim (or suggestion?) that the consistency of PA is an open problem. This week, an even more daring claim has circulated at the FOM list: PA is downright inconsistent. Its author is Edward Nelson, professor of mathematics at Princeton, known for his work on Internal Set Theory and Robinson arithmetic. In his words:

I am writing up a proof that Peano arithmetic (P), and even a small fragment of primitive-recursive arithmetic (PRA), are inconsistent.

He refers to a draft of the book he is working on, available here, and to a short outline of the book, available here. I've skimmed through the outline, which focuses mostly on a critique of finitism for making tacit infinitary assumptions, and towards the end there are some interesting considerations on the methodology he has been working with. In particular, he has devised a automated theorem-checker, qea:

Qea. If this were normal science, the proof that P is inconsistent could be written up rather quickly. But since this work calls for a paradigm shift in mathematics, it is essential that all details be developed fully. At present, I have written just over 100 pages beginning this. The current version is posted as a work in progress at http://www.math.princeton.edu/~nelson/books.html, and the book will be updated from time to time. The proofs are automatically checked by a program I devised called qea (for quod est absurdum, since all the proofs are indirect). Most proof checkers require one to trust that the program is correct, something that is notoriously diffi cult to verify. But qea, from a very concise input, prints out full proofs that a mathematician can quickly check simply by inspection. To date there are 733 axioms, de nitions, and theorems, and qea checked the work in 93 seconds of user time, writing to les 23 megabytes of full proofs that are available from hyperlinks in the book.

At this point, I really do not know what to think of Nelson's claims, and I doubt that I would be able to make much sense of his proofs anyway. So for now I'm just acting as a 'reporter', but I'd be curious to hear what others think!

UPDATE: Over at The n-Category Cafe', John Baez has a much more detailed post on Nelson's claims, including a suggestion by Terry Tao on a G+ thread as to what seems to be wrong with the proof. (Yay for G+!) Check also Tao's comment at 5:29.

ANOTHER UPDATE: Edward Nelson has replied at FOM to some of the queries that had been put forward. You can read his message here. He replies in particular to Tao's observations:

So far as I know, the concept of the "Kolmogorov complexity of a theory", as opposed to the Kolmogorov complexity of a number, is undefined. Certainly it does not occur in Chaitin's theorem or the Kritchman-Raz proof.  I work in a fixed theory Q_0^*. As Tao remarks, this theory cannot prove its own consistency, by the second incompleteness theorem. But this is not necessary. The virtue of the Kritchman-Raz proof of that theorem is that one needs only consider proofs of fixed rank and level, and finitary reasoning leads to a contradiction.

UPDATE AGAIN: I really encourage everybody to go check the comments at the The n-Category Cafe' post; the explanations of what is wrong with Nelson's purported proof are really very clear and accessible. I'm wondering if it would be worth writing a separate post on this? (Anyone?) At any rate, as an anonymous commentator says below, there's much to be commended in a purported proof whose loop-hole(s) can be identified fairly quickly; at least it was well formulated to start with.