Peano arithmetic is probably inconsistent | Hacker News Reader

Peano arithmetic is probably inconsistent

cs.nyu.edu

73 pointsmike_esspe33 comments

See http://golem.ph.utexas.edu/category/2011/09/the_inconsistenc... for interesting discussion of this result.

However http://xkcd.com/955/ applies in spades here. While it would be really interesting if Peano arithmetic is inconsistent, it is also really unlikely. For those who don't know the Peano axioms, see http://en.wikipedia.org/wiki/Peano_axioms.

Of those axioms, nobody has any trouble with any axiom other than the last one. Which is induction. His claim boils down to stating that allowing proof by induction leads to contradictions. But there is a pretty big tower of theorems needed to get there. Most people's guess is that he has made a mistake. If he hasn't, then it is still far more likely that some theorem in that tower is wrong than that induction leads to contradictions.

However if he proves to be right, in that tiny sliver, this will be really cool.

Now for the people who think I'm wrong, anyone want to wager $200 on the outcome? :-)

I'll wager $200, but first I need to know the odds offered. Also, I will want my payment even if you can prove that $5 == $200 (1 to 1 odds assumed) if Peano arithmetic is inconsistent.

basically you want consistent system embedding formal proof of Peano arithmetic inconsistency.

Overturning induction is a pretty tall order.

The longest road begins with a single step . . .

... and has the property that if every step is followed by another step, then the entire road will be walked.

I haven't even been able to overturn seduction.

I will join you, if there is more than $200 to be covered. What are the expected odds?

edit: seriously, this would surprise me significantly more than the neutrino thing, and I'm happy to take 100-1 odds on that.

What's interesting is that proof is computer assisted:

The proofs are automatically checked by a program I devised called qea (forquod 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.

I suspect that the theorem itself would prove the unreliability of the program. I suppose that puts you in a "bit of a pickle".

It doesn't matter if the program is unreliable, since it generates proofs that are easy (but tedious) for a human to check.

I don't think so; from a quick glance, I believe the theorem deals with inconsistencies when dealing with infinities, and the program and its output are all finite. If the program hangs or runs out of disk space, then that might be confirming evidence for the theorem ;-).

No,

An consistent theorem system can know no bounds. There's halfway. If Peano arithmetic is inconsistent every statement in it is provably true and false. QED.

Here's an example of such a mini-proof:

http://www.math.princeton.edu/~nelson/proof/BSI10.pdf

For those who are wondering if this is a crank. He is a notable mathematician. He is most notable for his work on http://en.wikipedia.org/wiki/Internal_set_theory which is a way to simplify the handling of non-standard analysis (calculus with infinitesimals - hyperreals on a rigorous footing).

He also wrote this book http://www.math.princeton.edu/~nelson/books/rept.pdf that studies probability theory without measure theory - I've only been through a couple chapters but I recommend it as interesting. Different perspectives help to allow one to understand things more fully.

Radically Elementary Probability Theory (REPT above) is an excellent book. A very thin volume that anyone who labored through measure-theoretic probability would enjoy at least scanning.

It is fascinating and original, like the proof mechanism mentioned upthread.

He is a noted mathematician- but also has driven the computer science community through this sort of thing before: http://rjlipton.wordpress.com/2011/10/01/what-if-peano-is-in... http://rjlipton.wordpress.com/2009/08/20/what-will-happen-wh...

Sensationalist title. A better one would be "Unreviewed proof claims that Peano arithmetic is inconsistent". This is self-published, hasn't been looked at by anybody else, and contradicts a very well-accepted and thoroughly examined argument for consistency from way back in 1936.

1: http://en.wikipedia.org/wiki/Gentzen%27s_consistency_proof

[edit: as the commenters point out, I'm no mathematician, and I'm working off Wikipedia. Go with what they say.]

For this kind of stuff there should be a way to flag a submission as 'sensationalist title' or 'likely false'. I just don't have the time to read all the comments for all submission just to find out if the submission is true or not.

Then don't read them; the community will figure out over the next few months whether Nelson's proved what he's claimed. The Peano axioms have stood for 120 years, it's probably not imperative that you find out whether they've been shown to be inconsistent right this minute.

> Then don't read them

I think that's his point: it's difficult to differentiate things that are likely wrong/false and things that have been verified by the community. Flags could help that.

I prefer simply relying on the comments, personally. In the comments you can see who's knowledgeable about the topic and often they'll explain what's wrong with the article. Votes and flagging can't do that.

Flags are a binary mechanism just like voting, and as such are vulnerable to precisely the same epistemic problems. As you say, comments offer a way of demonstrating expertise, not merely asserting it.

For this reason someone interested in a disputed topic such as this will either have to read the comments, in the hope of discovering the main lines of argument and improving the likelihood that the picture they form is correct, or suspend their judgement until such a time as better evidence (in this case, peer review of the claimed proof) is available.

Even so, I don't think most people would mind a disincentive for posts with titles that drastically overstate their content

What a stinking horrible idea.

How do you think scientific authority works, by the way? Why would you trust any given person with powers of "flagging" to flag something correctly? How would such people even be evaluated? Don't you think think the process of peer review is complicated for a reason?

If you want knowledge served up on a silver platter, you are going to starve to death.

No, it does not contradict Gentzen's proof.

Gentzen's proof proves that one set of axioms we think is consistent proves that another set of axioms we think is consistent is indeed consistent. However both sets of axioms could be inconsistent. We don't think that is so, but it could be.

Gentzen's proof relies on transfinite induction up to epsilon_0, which is not a principle liable to be accepted by someone with Nelson's foundational views. A good primer on these can be found in his book Predicative Arithmetic.

http://www.math.princeton.edu/~nelson/books/pa.pdf

Nelson is a full professor of mathematics at Princeton.

Some more discussion here: http://golem.ph.utexas.edu/category/2011/09/the_inconsistenc...

Notably, Terry Tao doesn't buy it.

Nelson's short reply to one of Tao's comments:

http://www.cs.nyu.edu/pipermail/fom/2011-September/015826.ht...

Ed Nelson has now withdrawn his claim.

http://www.cs.nyu.edu/pipermail/fom/2011-October/015832.html

    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.
    In the Kritchman-Raz proof, there is a low complexity
    proof of K(\bar\xi)>\ell if we assume \mu=1, but the
    Chaitin machine may find a shorter proof of high
    complexity, with no control over how high.
    
    My thanks to Tao and Tausk for spotting this.
    I withdraw my claim.
    
    The consistency of P remains an open problem.

If this is true, it would be a bigger deal to logicians than a solution to P vs NP.

My guess is that there will end up being a mistake somewhere (based purely on statistics of huge claims without full posted proofs), but it seems too early to say anything definitive. Terence Tao has guessed it is wrong, which is evidence against it, but then Nelson acknowledged Tao's remarks and said it isn't a problem, which is interesting. This is making me wish I was more of an expert so I could decide for myself.

I think the write-up has some bad signs (no central point, lots of side discussion, no new method ... see: http://www.scottaaronson.com/blog/?p=304 ).

IANAMathematician, but isn't this implied by the incompleteness theorem? Is this result significant because the seams in the consistency of Peano arithmetic haven't been formalized yet?

edit: After a quick visit to Wikipedia, it appears that completeness and consistency are actually separate things. I'll go back to coding now.

One consequence of the second incompleteness theorem is that no consistent arithmetic theory of sufficient strength can express its own consistency. One way of proving such a theory inconsistent is therefore to find a proof within that theory of its own consistency.

A complete theory is one in which, for any statement φ in the language of that theory, either φ is provable or ¬φ is provable within that theory. Note that this is a different sense of completeness than that proven in Gödel's Completeness Theorem, which states that any sentence satisfied by all models of a theory is provable.

A consistent theory is one which contains no contradictions. Because mathematics generally employs classical logic it is explosive [1] and any contradiction allows one to derive any sentence whatsoever in the language of the theory as a theorem. Because of this an alternative way to say that a theory is inconsistent is to say that all the sentences in the language of the theory are theorems.

[1] http://en.wikipedia.org/wiki/Principle_of_explosion

Reply on news.ycombinator.com