## Tuesday, 27 September 2011

### 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.

1. The use of an automatic theorem-prover is really interesting. It saves time and produces an output that can be integrated directly in a book or a paper. The use of this type of tools is really the future and will certainly change the practice of the logician and of the mathematician. We can compare it to the apparation of the calculator. Today, almost nobody will check by hand that [(145 + 256) * 7] + 942 = 3812 and use instead a software to compute it. Why bother to produce and check simple proofs if a tool can do it? Anyway, without clear specification about its software, we can ask ourself what kind of logic is implemented. It seems that only classical logical steps are used in this case.

Concerning his claim about the inconsistency of PA, it's really too high level for me.

Mathieu

2. As I understood him, Nelson is not using an automated theorem-prover, but rather a theorem-*checker*.
He does say that all proofs are indirect proofs, so presumably there is something very classical in the background.

3. Perhaps I misunderstood the difference between a theorem prover and a theorem checker.

But by skimming through the book is working on, I found page 40 more explanations on qea:
"The simple proof was automatically generated from the text proof by a program called
qea. Proofs generated by qea are simple proofs consisting of five parts...."

When I read this passage, I understand that the tool does not only check but gives proofs, at least for the simple ones. Perhaps a lot of them were trivial but anyway, the tool gives the proof and checks it at the same time. Then from page 41 to the end, a long list of definitions and theorems are given (the last is numbered 733). Surely, most of these theorems are automatically generated by qea.

I find this way of working really interesting.

Mathieu

4. Ok, so inside the book he does refer to automated theorem-proving, not only theorem-checking. I am also fascinated by this idea, that's why I singled it out as something particularly thought-provoking in the claims being made by Nelson.

5. Commenting on John Baez share of this at g+, Terence Tao wrote:

"I think I can reconstruct enough of the argument to figure out where the error in reasoning is going to be. Basically, in order for Chaitin's theorem (10) to hold, the Kolmogorov complexity of the consistent theory T has to be less than l. But when one arithmetises (10) at a given rank and level on page 5, the complexity of the associated theory will depend on the complexity of that rank and level; because there are going to be more than 2^l ranks and levels involved in the iterative argument, at some point the complexity must exceed l, at which point Chaitin's theorem cannot be arithmetised for this value of l."

6. The logical system employed is not intuitionistic. This becomes apparent at least from Theorem 7 onward.

7. @jrshipley, thanks for the pointer! I've added an update linking both to the n-Category Cafe' post and to the G+ thread (gotta love G+!)

8. I checked the first paragraphs of the book quickly and as a result I wanted to ask you about a very interesting point I noticed in Nelson's attempt to proof that PA is inconsistent.

(In page 11 and above) It seems like he is trying to push the argument against finitsm. In order to do that, he argues against mathematical induction. The argument (more or less) depends on the fact that natural numbers' properties are due to the very concept of standard model which, in turn needs ZF theory to prove some results about numbers and numerals. Therefore, finitsm has an infinitist foundation, which means the entire idea of finitism crashed.

Did I get it (a little bit) right? What did you understand?

And more important: Could anyone see this as a negative result about standard models?

Of course ruling out standard models is a big issue and could have colossal results for example in work with paradoxes involving infinite constructions.

9. Theorem: Nelson's proof can't be right.

Proof: The formal system within which Nelson carries out his proofs requires a theory of syntax. This theory is surely at least as strong as PRA. So:

(1) If Nelson's proof is right, then it follows that Nelson's proof is wrong.

Since, if the proof that PRA is inconsistent were correct, then it would presuppose, in the account of syntax for the language in which it is carried out, an inconsistent theory.

Even an intuitionist will admit that the above is equivalent to:

(2) Nelson's proof is wrong.

QED.

[There is a serious point being made here about the role of arithmetic in formulating syntax - one which Jeff has made elsewhere. In essence, you can't prove ANYTHING in a formal system without assuming some basic arithmetic. So if you show that the basic arithmetic in question is faulty, then you can't prove ANYTHING. So even if Nelson is in some sense 'right', there is some reason for thinking that, even by his own lights, he hasn't actually proven anything.]

10. I do not think that RoyTCook's point is correct. If, while working within a formal language system, one can prove its inconsistency by obtaining a statement within the system that is both true and false, then one has indeed invalidated the proof, but the proof is needed no longer. That is, the only way in which the proof is invalidated is if the theory of syntax in which it is carried out is inconsistent in the first place.

11. D Tausk has clarified the sense in which Tao takes the Kolmogorov complexity of a number to depend on a theory.
It appears that at a minimum Professor Nelson will need to modify his proof.

12. It's instructive to contrast this episode with the "proof" of P=NP earlier this year, when the math blogs were filled with daily chatter on the subject for months. In that case, the "proof" was amorphous and most effort went in to determining if anything substantial and new had been proven.

In this case, a coherent system was presented in a verifiable form, and a serious flaw was detected within hours. The reserved silence of the community has been almost eerie as an acknowledgement of the error is awaited, possibly with a modification or indication of the next step.

Even if the error is not repairable, this episode marks a victory for mathematical discourse.

13. Even if the error is not repairable, this is no importent, because ZFC is inconsistent.