Hacker Newsnew | past | comments | ask | show | jobs | submitlogin

So, Nelson had claimed to have proven Peano arithmetic inconsistent.

Peano arithmetic is a set of axioms that describe basic properties of the whole numbers (nonnegative integers). It's a pretty simple set of statements. The axioms are described in terms of 0, S (the successor function, S(n) = the next number after n), plus, and times.

The axioms are:

1. If Sn = Sm, then n=m

2. For all n, Sn is not 0

3. For all n, n+0=n

4. For all n and m, n+Sm = S(n+m)

5. For all n, n*0=0

6. For all n and m, n*Sm = n*m + n

7. [Induction] If P(n,m_1,...,m_k) is a predicate, and m_1,...m_k are whole numbers, such that:

A. P(0,m_1,...m_k) holds, and

B. For all n, P(n,m_1,...,m_k) implies P(Sn,m_1,...,m_k)

Then for all n, P(n,m_1,...,m_k) holds.

...OK, that last one is maybe a bit complicated. Technically, that one is actually what's called an axiom schema, that generates infinitely many axioms, one for each possible predicate of one or more variables (note you can have k=0). The theory is about whole numbers, not about predicates; the theory can't actually talk directly about predicates. Anyway, that's a bit of technical detail you don't really need to know for these purposes, so let's just move on. If you didn't understand that part, it's OK.

As you probably know, if we have a mathematical theory, and that theory is supposed to describe something that is supposed to actually exist (such as the whole numbers), that theory had better be consistent.

Firstly, because if it's not consistent, it can't possibly be true (the technical term is "sound"). Reality is consistent, so if something is inconsistent, it's incorrect.

Secondly, because of the principle of explosion. If you know P and not P for some statement P, you can conclude any statement Q. This principle of logic may be counterintuitive, but it's pretty essential. Some people have made a version of logic that don't include it ("minimal logic"), and it's basically unusable.

Suppose you know both P and not P, and you want to prove a statement Q. Well, you know P, so you certainly know P or Q. But you also know not P; that eliminates P as a possibility, leaving Q. So in order to get rid of the principle of explosion, you'd have to get rid of the principle that if you know A or B, and also know not A, then you can eliminate A as a possibility to conclude B. That's a pretty big tool to go without!

(Well, or you'd have to get rid of the possibility that if you know A, you can conclude A or B, but that's even worse.)

So, if a set of foundational mathematical axioms is found to be inconsistent, it could be something of a disaster for mathematics. People would need to come up with new, weaker axioms that somehow didn't lead to this contradiction. This would be a difficult thing to do -- which principles do you keep, and which do you jettison? (And which do you replace with weaker versions? And what new weaker ones do you invent to take the place of ones that had to be tossed?) That's not an easy question!

So let's say that the ZFC axioms were found to be inconsistent. The ZFC axioms are a set of axioms (and axiom schemas) that describe set theory, and basically all of "ordinary mathematics" can be founded on them. (I'm not going to list them all here; they're not that complicated, but they're rather more complicated than Peano arithmetic.)

If the ZFC axioms were found to be inconsistent, well, it could be a project of years or decades to come up with a new, hopefully consistent, foundation of mathematics. It would be quite the problem. But... it wouldn't destroy mathematics. After all, ZFC itself is what people came up with after the earlier attempts to axiomatize set theory were found to lead to contradictions, so this has in a sense happened once before.

So why would it be such a big deal if the Peano axioms in particular were found to be inconsistent? Why would do people say that would destroy mathematics?

There are a few reasons for this.

Firstly, the Peano axioms describe the whole numbers, rather than set theory. Set theory is kind of out there -- who can really say what should or should not be true of vastly infinite sets? Yeah, the ZFC axioms all seem like they should be true, but so did the axiom of unrestricted comprehension, and that turned out to be no good. The Peano axioms, by contrast, describe the whole numbers, and are pretty basic statements about them. They had better be true, or else we are very wrong about the whole numbers!

But, that's not the only reason. After all, if that were it, it would still likely be possible to recover from the problem by passing to a weaker system of axioms. And there are various ones that have been proposed! The Peano axioms are mostly pretty simple, but that last one, induction, has a lot of hidden complexity to it. People have suggested ways you could weaken the induction axiom by limiting what sorts of predicates it applies to. And that would certainly be contentious, but if Peano arithmetic were found to be inconsistent, we'd have to. Thing is, that wouldn't solve the real problem.

The problem is that weakening the induction axiom is only really a possibility if you want to describe the whole numbers in isolation. In reality, we don't consider the whole numbers in isolation, described by the Peano axioms; but rather as part of the broader picture of mathematics, described by ZFC. We don't study just whole numbers, but sets of whole numbers, whole numbers interacting with real numbers and complex numbers and p-adic numbers, whole numbers interacting with graphs and groups and partitions, whole numbers interacting with vector spaces and manifolds and all the rest of mathematics.

So, in reality, if Peano arithmetic were found to be inconsistent, the real task wouldn't be to weaken the Peano axioms so they'd be consistent; it would be to weaken the axioms of ZFC, in such a way that that would weaken the Peano axioms to remove the contradiction.

But that's just about an impossible task. It'd be nearly impossible to weaken the axiom schema of induction, while also leaving a theory that can interact with the rest of mathematics. Because you see, if we want the whole numbers to be able to interact with the rest of mathematics, then we have to be able to talk about sets of whole numbers.

And if we can talk about sets of whole numbers, then we can talk about the following variant of induction: Let S be a set of whole numbers, and suppose that 0 is in S, and, for each whole number n, n being in S implies n+1 is in S. Then all whole numbers are in S.

Now this may sound like the same thing I said above -- they're both just induction, right? But this one is about sets, not predicates, because now we're in a setting where we can talk about sets. And this one is more general -- because, if we have a predicate about whole numbers, we can form the set of whole numbers satisfying it. Whereas notionally one could have a set not described by any predicate.

So, if you have this statement (set induction), you get all of predicate induction. So you'd somehow have to weaken the axioms of mathematics such that:

1. You can still talk about sets of natural numbers, but

2. You don't get predicate induction.

And how on earth would one do that?? Stopping set induction sounds pretty much like a dead-end; like if you did that, how would you get any form of induction at all? (And if you don't have any form of induction, then you don't really have the whole numbers; it's kind of their defining feature.) I mean you could make special assumptions about whole numbers, but if we're trying to make more general set-theoretic axioms, where whole numbers aren't fundamental, those don't really belong.

So the remaining option then is to stop the link from set induction to predicate induction, by limiting what sorts of sets you can make, so not every predicate on whole numbers can be used to form a set of whole numbers.

But (while I think that's considered less impossible), that's not really a viable option either! Because that would mean that somehow you'd have to introduce, into your set theoretic axioms, restrictions on what predicates can be used to form sets; and while there are sensible ways one could formulate restrictions in the limited context of whole numbers, there's not really any good way to formulate such restrictions that would make sense in the broader context of mathematics as a whole.

So, basically, we'd be stuck. Coming up with new axioms if ZFC were proved inconsistent would be difficult but doable. Coming up with new axioms if Peano arithemtic were proved inconsistent seems basically impossible. So, finding a contradiction derivable from the Peano axioms could indeed destroy mathematics.

Of course, since people generally expect that the Peano axioms are true, nobody really expects that to happen. But Edward Nelson -- an adherent of the fringe mathematical school known as ultrafinitism -- disagreed, believing induction was probably not true and not consistent. And here he claimed to have found an actual inconsistency. But, as has been mentioned, Terry Tao found a hole in his argument. And so mathematics was not destroyed. At least not that day.



Oh, let me close up one little hole in my comment, before anyone points it out. :) This may require rather more mathematical knowledge I'm afraid.

Above I said the only reasonable way to weaken Peano arithmetic was to weaken induction. But that's not quite true. There's another way: Not changing any of the axioms, but weakening the underlying logic.

See, there's a school of mathematics known as "constructivism", and they object to the usual laws of logic, saying that they're too strong; they use a weaker logic. It ought to be called "constructive logic", but for historical reasons (that are really not worth getting into) it's called "intuitionistic logic" instead.

And this might seem to be a better approach, because weakening the laws of logic is something that can be done without regard for the setting; it doesn't matter here whether you're talking about just whole numbers, or mathematics as a whole. (Well, almost. Actually, from ZFC and intuitionistic logic, you can effectively get back classical logic. But there are pretty good ideas about how to modify ZFC to avoid that.)

The problem is, doing this doesn't help. Because it's known that if you can prove a contradiction from the Peano axioms using classical logic, you can also do so using intuitionistic logic. So even if you went constructive, you'd still be stuck with all the same problems.


In addition to weakening the logic (or avoiding the parts that introduce incompleteness, especially the existential quantifier) you also need to weaken your arithmetic. We know that Primitive Recursion (PR) is too weak to prove its own consistency, and Peano Arithmetic (PA) is too strong. So you may have to look at a strengthening of PR and/or weakening of PA in order to achieve a theory that proves its own consistency. Whether that theory exists is still an open question.


Getting a theory that proves its own consistency isn't what's being discussed here. What's being discussed here is just weakening a theory to remove a particular inconsistency after an inconsistency is found.

Trying to make a usable theory that also proves its own consistency is probably also a futile goal, per Gödel, but it's a separate one, and not one that people would likely go for if an inconsistency were found in Peano arithmetic.


> if you can prove a contradiction from the Peano axioms using classical logic, you can also do so using intuitionistic logic.

Are you sure it isn't the other way around? If you can prove a contradiction using intuitionistic logic, it's also a contradiction using classical.

If you proved the contradiction using the excluded middle then that proof wouldn't hold when you use intuitionistic logic. Maybe I'm missing or not understanding something here.


I mean, the other way around is also true, but the other way around is obvious. Obviously going from a weaker logic to a stronger logic can't eliminate contradictions.

What's surprising is that in this particular case (the Peano axioms), the reverse is also true; you won't be able to eliminate contradictions by passing to this weaker logic.

Note, all I said is, if you can prove a contradiction classically, then you can prove a contradiction constructively! I didn't say, if you have a classical proof of a contradiction then it's a valid constructive proof of a contradiction. Obviously not! But it will still be true that you'll be able to prove a contradiction constructively; it just won't necessarily be the same proof.

If you want to know more about the particular transformation, well, here's a relevant Wikipedia article: https://en.wikipedia.org/wiki/Double-negation_translation


Thank you for your explanation and pointing me to the double negation translation.

I know this is off-topic but if you have a book recommendation which teaches about intuitionistic logic/constructive math and also mentions the double negation translation, I'm interested. Most books I've read seem to either concentrate on only constructive or classical math.


I don't, sorry. I'm not really a logician, just a mathematician who thinks the foundations are worth understanding. :) I don't know what proper references on this material would be.


Classical logic can be embedded into intuitionistic logic. The double-negation translation N [0] turns any tautology of classical logic into a tautology of intuitionistic logic, so if θ ∧ ¬θ is provable with classical logic, N(θ) ∧ ¬N(θ) is provable with intuitionistic logic.

[0]: https://en.wikipedia.org/wiki/Double-negation_translation


What makes you say that reality is consistent? How would we know?


I think you may have a typo. Should 4 be Sn+Sm=S(n+m)?


No. Sn+Sm would be n+m+2, while S(n+m) is n+m+1.


When I read about Peano axioms I mentally think of Sn as the function S(n) = n+1 and that helps me understand them better.

As a non mathematician sometimes I wonder if this substitution is causing me to misunderstand something else about them.


S is not a multiplier; it's a call of the successor function. The distributive property doesn't apply.




Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact

Search: