Edward Nelson claims proof of inconsistency in Peano Arithmetic

We've discussed Edward Nelson's beliefs and work before. Now, he claims to have a proof of a contradiction in Peano Arithmetic; which if correct is not that specific to PA but imports itself into much weaker systems. I'm skeptical of the proof but haven't had the time to look at it in detail. There seem to be two possible weakpoints in his approach. His approach is to construct a system Q_0^* which looks almost but not quite a fragment of PA and then show that PA both proves this system's consistency and proves its inconsistency. 

First, he may be mis-applying the Hilbert-Ackermann theorem-when it applies is highly technical and can be subtle. I don't know enough to comment on that in detail. The second issue is that in trying to show that he can use finitary methods to show there's a contradiction in Q_0^* he may have proven something closer to Q_0^* being omega-inconsistent. Right now, I'm extremely skeptical of this result.  

If anyone is going to find an actual contradiction in PA or ZFC it would probably be Nelson. There some clearly interesting material here such as using a formalization of the  surprise examiation/unexpected hanging to get a new proof of of Godel's Second Incompleteness Theorem. The exact conditions which this version of Godel's theorem applies  may be different from the conditions under which the standard theorem can be proven. 

Comments

sorted by
magical algorithm
Highlighting new comments since Today at 1:00 AM
Select new highlight date
All comments loaded

Is that a withdrawal of the entire approach or just one part of it?

On the FOM list, he writes:

Terrence Tao, at http://golem.ph.utexas.edu/category/2011/09/ and independently Daniel Tausk (private communication) have found an irreparable error in my outline. (...)

(...) I withdraw my claim.

The consistency of P remains an open problem.

I am interested in how this event has influenced peoples view of the consistency of arithmetic. For those who had a viewpoint on it prior to this, what would you have estimated before and after and with what confidence? I will not state my own view for fear of damaging the results.

Specifically, Tao's comment:

I have read through the outline. Even though it is too sketchy to count as a full proof, 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.

(One can try to outrun this issue by arithmetising using the full strength of Q_0^*, rather than a restricted version of this language in which the rank and level are bounded; but then one would need the consistency of Q_0^* to be provable inside Q_0^*, which is not possible by the second incompleteness theorem.)

I suppose it is possible that this obstruction could be evaded by a suitably clever trick, but personally I think that the FTL neutrino confirmation will arrive first.

He's such a glorious mathematician. <3

FTL neutrinos and now a proof of inconsistency in Peano Arithmetic? What next?

I have devised a little proof of inconsistency of the Newtonian mechanics, years ago.

http://critticall.com/alog/Antinomy_inside_mechanics.pdf

Can you spot the error?

Vg vf pbeerpg gung ng g=0, rnpu cnegvpyr unf n yrsgjneqf irybpvgl. Ohg vg vf abg pbeerpg gung gur prager bs tenivgl ng g=0 unf n yrsgjneqf irybpvgl. Guvf vf orpnhfr gur flfgrz orunirf qvfpbagvahbhfyl ng g=0, naq fb gur irybpvgl bs gur prager bs tenivgl pnaabg or qrgrezvarq ol gnxvat n jrvtugrq nirentr bs gur vavgvny irybpvgvrf bs gur pbzcbaragf.

Va zber qrgnvy:

Yrg P(g) or gur cbfvgvba bs gur prager bs tenivgl ng gvzr g.

Gur irybpvgl bs gur prager bs tenivgl ng g=0 vf gur yvzvg nf g -> 0 bs (P(g)-P(0))/g.

Ng nal gvzr g, P(g) vf gur fhz bire a bs Z(a)C(a,g), jurer Z(a) vf gur znff bs gur agu cbvag naq C(a,g) vgf cbfvgvba.

Gur nethzrag eryvrf ba pbzchgvat qP/qg nf gur fhz bire a bs Z(a)qC(a,g)/qg. Guvf fjncf gur beqre bs gjb yvzvgvat cebprffrf, fhzzngvba naq qvssreragvngvba, juvpu vf inyvq sbe jryy-orunirq fhzf, ohg abg sbe guvf bar.

For intuition, imagine that there were just the first three particles in the sequence, and that the number 10 is replaced by something much larger. The two leftmost particles will rapidly oscillate about one another, while drifting slowly towards the rightmost. Now imagine the first four particles are present. The two leftmost will oscillate madly about each other, while that system as a whole oscillates rapidly about the third from the left (I'm conveniently ignoring what happens at the instants when particles meet and pass through each other), and the ensemble of the three leftmost drifts towards the rightmost. Repeat.

Similar, for those who enjoyed discussing this problem: Did you know that Newtonian mechanics is indeterministic?

These equations don't make sense dimensionally. Are there supposed to be constants of proportionality that aren't being mentioned? Are they using the convention c=1? Well, I doubt it's relevant (scaling things shouldn't change the result), but...

Edit: Also, perhaps I just don't know enough differential equations, but it's not obvious to me that a curve such as he describes exists. I expect it does; it's easy enough to write down a differential equation for the height, which will give you a curve that makes sense when r>0, but it's not obvious to me that everything still works when we allow x=0.

And here I thought there wasn't anything besides c I'd bet on at 99-to-1 odds.

Two! Two things in the universe I'd bet on at 99-to-1 odds. Though I'm not actually going to do it for more than say $2k if anyone wants it, since I don't bet more than I have, period.

Would you bet at 99-to-1 odds that I will not win the lottery tomorrow?

So by now Nelson's outline has been challenged by the formidable Terry Tao, and Nelson (himself formidable!) has responded to this challenge and isn't budging. Link.

The FTL thread has attracted many confident predictions about the ultimate outcome. But this one hasn't. Is this because people find the subject less interesting? Or because they are less confident?

For what it's worth, here's the timeline of my thoughts/beliefs, in silly internal-monologue form. Maybe the numbers shouldn't be taken too seriously, and I'm not trying to bait anyone into betting 200 grand against my 10 dollars, but I'd be interested to hear what people have been thinking as (or if) they've been following this.

A few days ago: "Contrary to almost everybody, I don't think there is any reason to believe PA is consistent. Someone, e.g. Nelson or the much younger Voevodsky, might show it is inconsistent in my lifetime." P approx 5%.

Nelson's announcement: "Holy shit he's done it." P approx 40%

Tao's challenge: "Oh, I guess not, poor guy how embarrassing." P back down to 5%

Nelson neither ignores nor caves to Tao: "Beats me, maybe he's done it after all." P now maybe at 10%.

I've put up on Prediction Book a relevant prediction. The main reason I've given only a 75% percent chance that it may take a lot of time to study the matter in detail.

If you are putting 10% on the chance that Nelson's proof will turn out to be correct, then 10% seems way too high for essentially reasons that benelliot touched on below. My own estimate for this is being correct is around 0.5%. (That's sort of a meta estimate which tries to take into account my own patterns of over and underconfidence for different types of claims.) I'd be willing to bet 100$ to 1$ which would be well within both of our stated estimates.

The issue is mainly that I don't think I'm qualified to determine the outcome of the debate, Nelson and Tao are both vastly better at maths than me, so I don't have much to go on. I suspect others are in a similar predicament.

I've been trying to understand their conversation and if I understand correctly Tao is right and Nelson has made a subtle and quite understandable error, but I also estimate P(my understanding is correct) < 0.5 is not very large, so this doesn't help much, and even if I am right there could easily be something I'm missing.

I would also assign this theorem quite a low prior. Compare it to P =! NP, when a claimed proof of that comes out, mathematicians are usually highly sceptical (and usually right), even if the author is a serious mathematician like Deolalikar rather than a crank. Another example that springs to mind is Cauchy's failed proof of Fermat's last theorem (even though that was eventually proven, I still think a low prior was justified in both cases).

This, if correct, would be a vastly bigger result than either of those. I don't think it would be an exaggeration to call this the single most important theorem in the history of mathematics if correct, so I think it deserves a much lower prior than them. Even more so, since in the case of P =! NP most mathematicians at least think it's true, even if they are sceptical of most proofs, in this case most mathematicians would probably be happy to bet against it (that counts for something, even if you disagree with them).

I don't have much money to lose at this point in my life, but I'd be happy to bet $50 and $1 that this is wrong.

I think there's a salient difference between this and P = NP or other famous open problems. P = NP is something that thousands of people are working on and have worked on over decades, while "PA is inconsistent" is a much lonelier affair. A standard reply is that every time a mathematician proves an interesting theorem without encountering a contradiction in PA, he has given evidence for the consistency of PA. For various reasons I don't see it that way.

Same question as for JoshuaZ: has your prior for "a contradiction in PA will be found within a hundred years" moved since Nelson's announcement?

has your prior for "a contradiction in PA will be found within a hundred years" moved since Nelson's announcement?

Yes, obviously P(respectable mathematician claims a contradiction | a contradiction exists) > P(respectable mathematician claims a contradiction | no contradiction exists), so it has definitely moved my estimate.

Like yours, it also moved back down when Tao responded, back up a bit when Nelson responded to him, and back down a bit more when Tao responded to him and I finally managed a coherent guess at what they were talking about.

I think there's a salient difference between this and P = NP or other famous open problems. P = NP is something that thousands of people are working on and have worked on over decades, while "PA is inconsistent" is a much lonelier affair.

I'm not sure this is an important difference. I think scepticism about P =! NP proofs might well be just a valid even if far fewer people were working on it. If anything it would be more valid, lots of failed proofs gives you lots of chances to learn from the mistakes of others, as well as building avoiding routes which are proven not to work by others in the field. Furthermore, the fact that huge numbers of mathematicians work on P vs NP but have never claimed a proof suggests a selection effect in favour of those who do claim proofs, which is absent in the case of inconsistency.

Furthermore, not wanting to be unfair to Nelson, but the fact he's working alone on a task most mathematicians consider a waste of time may suggest a substantial ideological axe to grind (what I have heard of him supports this thoery) and sadly it is easier to come up with a fallacious proof for something when you want it to be true.

I'm not sure if this line of debate is a productive one, the issue will be resolved one way or the other by actual mathematicians doing actual maths, not by you and me debating about priors (to put it another way, whatever the answer ends up being, this conversation will have been wasted time in retrospect).

Yes, obviously P(respectable mathematician claims a contradiction | a contradiction exists) > P(respectable mathematician claims a contradiction | no contradiction exists), so it has definitely moved my estimate.

Can you roughly quantify it? Are we talking from million-to-one to million-to-one-point-five, or from million-to-one to hundred-to-one?

I'm not sure if this line of debate is a productive one, the issue will be resolved one way or the other by actual mathematicians doing actual maths, not by you and me debating about priors (to put it another way, whatever the answer ends up being, this conversation will have been wasted time in retrospect).

Sorry if I gave you a bad impression: I am not trying to start a debate in any adversarial sense. I am just curious.

Furthermore, not wanting to be unfair to Nelson, but the fact he's working alone on a task most mathematicians consider a waste of time may suggest a substantial ideological axe to grind (what I have heard of him supports this thoery) and sadly it is easier to come up with a fallacious proof for something when you want it to be true.

Of that there's no doubt, but it speaks well of Nelson that he's apparently resisted the temptation toward self-deceipt for decades, openly working on this problem the whole time.

Can you roughly quantify it? Are we talking from million-to-one to million-to-one-point-five, or from million-to-one to hundred-to-one?

The announcement came as a surprise, so the update wasn't negligible. I probably wouldn't have gone as low as million-to-one before, but I might have been prepared to estimate a 99.9% chance that arithmetic is consistent. However, I'm not quite sure how much of this change is a Bayesian update and how much is the fact that I got a shock and thought about the issue a lot more carefully.

Cauchy? Don't you mean Lamé?

Anyway if you lose the bet 1 = 0 therefore you don't need to transfer any money.

Cauchy? Don't you mean Lamé?

From what gathered both went down a similar route at the same time, although it is possible that I am mistaken in this. I named Cauchy as he seems to be the best-known of the two, and therefore the one with the highest absolutely-positively-not-just-some-crank factor.

Anyway if you lose the bet 1 = 0 therefore you don't need to transfer any money.

If I lose the bet (not that anyone has yet agreed to accept the bet), then payment will be based on restricted number theory without the axiom of induction.

Assume for a second that FTL communication is possible and that PA is inconsistent. How could this possibly influence a proof of AI friendliness that has been invented before those discoveries were made and how can one make an AI provably friendly given other possible fundamental errors in our understanding of physics and mathematics?

So this is an interesting set of questions. I don't think FTL issues should matter in this context. Inconsistency in PA is more of an issue. I'm not terribly worried about an actual inconsistency in PA. So much goes wrong if that's the case that AI issues might actually be small (no really. It could be that bad.). That said, however, this sort of worry makes a lot more sense for proofs in ZF or ZFC. I'd be a lot more worried about a contradiction showing up in ZF than in PA. So one might want to make sure that any such proofs use as small a segment of ZF as possible.

I'm not terribly worried about an actual inconsistency in PA. So much goes wrong if that's the case that AI issues might actually be small (no really. It could be that bad.)

That is an understandable reaction. But since encountering Nelson's ideas a while ago, I've found myself thinking less and less that it would be that bad at all. There is no very strong evidence that completed infinities need to be grappled with at a physical or real-world level. The main "finitary" thing you lose without PA is superexponentiation. But that shows up surprisingly rarely, in the universe and in math. (Or maybe not so surprisingly!)

Interestingly, superexponentiation shows up very often on less wrong. Maybe that's a good answer to XiXiDu's question. If Nelson is right, then people should stop using 3^^^3 in their thought experiments.

My understanding is that Nelson doesn't necessarily believe in exponentiation either although his work here doesn't have the direct potential to wreck that.

The real issue isn't PA as much as the fact that there are a very large number of theorems that we use regularly that live in axiomatic systems that model PA in a nearly trivial fashion. For example, ZFC minus replacement, choice and foundation. Even much weaker systems where one replaces the power set axiom with some weaker axiom allows you to construct PA. For example if you replace the power set axiom with the claim that for any two sets A and B their cartesian product always exists. Even this is much stronger than you need. Similarly, you can massively reduce the allowed types of input sets and predicates in the axiom schema of specification and still have a lot more than you need. You can for example restrict the allowed predicate sets to at most three quantifiers and still be ok (this may be restrictable to even just two quantifiers but I haven't worked out the details).

And what Nelson's proof (if valid) breaks is weaker than PA which means that if anything the situation is worse.

It may be for example that any axiomatic system which lets us talk about both the real numbers and the integers allows Nelson's problem. Say one for example one has an axiomatic system which includes Nelson's extreme finitary version of the natural numbers, include the very minimal amount of set theory necessary to talk about sets, include second order reals, and an axiom embedding your "natural numbers" into the reals. Can you do this without getting all sorts of extra stuff thrown in? I don't know and this looks like an interesting question from a foundational perspective. It may depend a lot on which little bits of set theory you allow. But, I'm going to guess that the answer is no. I'll need to think about this a bit more to make the claim more precise.

My understanding is that Nelson doesn't necessarily believe in exponentiation either although his work here doesn't have the direct potential to wreck that.

I know this isn't the main point of your comment but I got carried away looking this stuff up.

In his 1986 book, he defines a predicate exp(x,k,f) which basically means "f is a function defined for i < k and f(i) = x^i". And he defines another predicate epsilon(k) which is "for all x there exists f such that exp(x,k,f)". I think you can give a proof of epsilon(k) in his regime in O(log log k) steps. In standard arithmetic that takes O(1) steps using induction, but O(log log k) is pretty cheap too if you're not going to iterate exponentiation. So that's a sense in which Nelson does believe in exponentiation.

On the other hand I think it's accurate to say that Nelson doesn't believe that exponentiation is total, i.e. that for all n, epsilon(n). Here's an extract from Nelson's "Predicative Arithmetic" (Princeton U Press 1986). Chapter heading: "Is exponentiation total?"

Why are mathematicians so convinced that exponentiation is total (everywhere defined)? Because they believe in the existence of abstract objects called numbers. What is a number? Originally, sequences of tally marks were used to count things. Then positional notation -- the most powerful achievement of mathematics -- was invented. Decimals (i.e. numbers written in positional notation) are simply canonical forms for variable-free terms of arithmetic. It has universally assumed, on the basis of scant evidence, that decimals are the same kind of thing as sequences of tally marks, only expressed in a more practical and efficient notation. This assumption is based on the semantic view of mathematics, in which mathematical expressions, such as decimals and sequences of tally marks, are regarded as denoting abstract objects. But to one who takes a formalist view of mathematics, the subject matter of mathematics is the expressions themselves together with the rules for manipulating them -- nothing more. From this point of view, the invention of positional notation was the creation of a new kind of number.

How is it then that we can continue to think of the numbers as being 0, S0, SS0, SSS0, ...? The relativization scheme of Chapter 5 [heading: "Induction by relativization"] explains this to some extent. But now let us adjoin exponentiation to the symbols of arithmetic. Have we again created a new kind of number? Yes. Let b be a variable-free term of arithmetic. To say that the expression 2^b is just another way of expressing the variable-free term of arithmetic, SS0 SS0 ... SS0 with b occurrences of SS0, is to assume that b denotes something that is also denoted by a sequence of tally marks. (The notorious three dots are a direct carry-over from tally marks.) The situation is worse for expressions of the form 2^2^b -- then we need to assume that 2^b itself denotes something that is also denoted by a sequence of tally marks.

Mathematicians have always operated on the unchallenged assumption that it is possible in principle to express 2^b as a numeral by performing the recursively indicated computations. To say that it is possible in principle is to say that the recursion will terminate in a certain number of steps -- and this use of the word "numbers" can only refer to the primitive notion; the steps are things that are counted by a sequence of tally marks. In what number of steps will the recursion terminate? Why, in somewhat more that 2^b steps. The circularity in the argument is glaringly obvious.

We'd have to know what a proof of friendliness looks like to answer this.

This aspect is very interesting:

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 difficult 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, definitions, and theorems, and qea checked the work in 93 seconds of user time, writing to files 23 megabytes of full proofs that are available from hyperlinks in the book.

It seems easier to me to simply trust Coq than to read through 23 megabytes of proofs by eye. But I'm not entirely certain what the purpose of qea is.

Actually, I would be more interested in the size of checking core of Qea. Quickly inspecting 23 megabytes of proofs sounds like a bad idea. A converter to TSTP first-order proof format (for example) would allow me to use a few different bug-for-bug-independent well-tested checkers for this format that are already out there; that I would trust more than both human inspection and any single-implementation prover.

To date there are 733 axioms

How do you get to 733 axioms? Maybe I'm being stupid, but doesn't PA run on just 5?

Strictly speaking, PA uses infinitely many axioms -- the induction axiom is actually an axiom schema, one axiom for each predicate you can plug into it. If you actually had it as one axiom quantifying over predicates, that would be second-order.

I think 733 is counting axioms, definitions, and theorems all.

It said "733 axioms, definitions, and theorems"

I'm guessing 733 is the sum of the axioms, definitions and theorems, not just the axioms alone.

Here's a summary and discussion of the affair, with historical comparison to the Gödel results and their reception (as well as comments from several luminaries, and David Chalmers) on a philosophy of mathematics blog whose authors seem to take the position that the reasons for consensus in the mathematical community are mysterious. (It is admitted that "arguably, it cannot be fully explained as a merely socially imposed kind of consensus, due to homogeneous ‘indoctrination’ by means of mathematical education.") This is a subject that needs to be discussed more on LW, in my opinion.