# $0 \neq 1$ not provable in axiomatic arithmetic?

I am reading my logic professor's notes, and he writes

What then is the evidence that there are no undiscovered contradictions from axioms of arithmetic? Exactly why is $0 \neq 1$ not provable in an axiomatic arithemic based on a specific list of properties expressed in a language?

This is shortly after he listed the Peano axioms. $1$ is just shorthand for $s(0)$, and we have as an axiom that $(\forall x)\neg(s(x)=0)$. So in particular, $\neg (s(0)=0)$, i.e., $1 \neq 0$. So what could my professor mean when he says $0 \neq 1$ is not provable in an axiomatic arithmetic? It is possible he has misspoken.

• Perhaps you can ask your professor. – Michael Apr 7 '17 at 19:10
• While I do not know what axioms you have, you might try $x \in \{0,1\}$ and use mod-2 arithmetic to see if your axioms are consistent in that case. So in that case $s(0)=1$ and $s(1)=0$, which seems fine as long as you remove that assumption that $s(x) \neq 0$. – Michael Apr 7 '17 at 19:14
• The point is that there might be a long and sophisticated proof of $0 = 1$, which would be a contradiction. The question is how do we know that our axioms are consistent? That is not as obvious as it may seem. – Mark Bennet Apr 7 '17 at 19:15
• @MarkBennet Thank you, that does seem to be the point he was trying to make. – kccu Apr 7 '17 at 19:16

Your professor misspoke. The doubt is whether "$0=1$" could somehow be proved from the axioms of arithmetic - note that this is equivalent to those axioms being inconsistent. Of course, the statement "$0\not=1$" is very easily provable from those axioms.

• This looks good (I give plus 1, don't know why others downvote). My interpretation is a bit different though, one could ask "why do we need to include the axiom $s(x) \neq 0$, can't we just prove $s(x) \neq 0$ from the other axioms"? And I think a simple proof that "it is not provable from the other axioms" is if you define your set of numbers to be something trivial, like the set 0 alone, or the mod-2 binary field, which likely satisfies all other axioms. Overall, the professor is there and likely holds office hours, it makes sense to ask him/her directly! – Michael Apr 7 '17 at 19:24
• @Michael That would be a very reasonable question, but I don't think it's the one the professor was mentioning: "What then is the evidence that there are no undiscovered contradictions from axioms of arithmetic?" is asking about the issue of being able to prove too many things from already given axioms, not about needing more axioms to prove new things (although of course the issue of sufficiency is a fundamental point in mathematical logic!). – Noah Schweber Apr 7 '17 at 19:27
• I was focusing on the second sentence of the professor "Exactly why is $0\neq 1$ not provable in an axiomatic arithmetic," which suggested to me the idea of removing this as an axiom and trying to prove it as a lemma. You are convincing that, in view of the first sentence, the "$0\neq 1$" was likely a typo that should have been "$0=1$." This is kind of an interesting "max-likelihood error correction" problem on language. – Michael Apr 7 '17 at 20:09
• @Michael Yeah, another possibility that leapt to mind was that maybe the professor meant to say "Exactly why is $0\not=1$ not disprovable in ...", which is the sort of thing I used to say before I figured out why three negatives in a row are a bad idea. – Noah Schweber Apr 7 '17 at 20:16

$1 \not = 0$ is not the same statement as $0 \not = 1$, but that is easily fixed, assuming some standard rules of logic:

1. $\forall x \neg s(x) = 0$ Peano Axiom 1

2. $\quad 0 = s(0)$ (Assumption)

3. $\quad 0 = 0$ ($=$ Intro)

4. $\quad s(0) = 0$ ($=$ Elim 2,3)

5. $\quad s(0) \not = 0$ ($\forall$ Elim 1) (i.e. '$1 \not = 0$')

6. $\quad \bot$ ($\bot$ Intro 4,5)

7. $0 \not = s(0)$ ($\neg$ Intro 2-6) (i.e. '$0 \not = 1$')

OK, so it is definitely false that '$0 \not = 1$' is not provable from the Peano Axioms.

But probably your professor meant the following: how do we know our axioms are consistent? How do we know we are not able to infer a contradiction from them (which would be the case if, e.g. '$1=0$' would be provable)?

That's a good question, and the standard answer is that we can come up with a model for the Peano axioms ... which is of course just the domain of natural numbers, together with the successor, addition , and multiplication functions as we know them. And since there is a model, that means it is impossible to derive a contradiction assuming your logical inference rules are sound (as they are for any standard proof system). So, it would be impossible to prove 1=0 or anything else like that that would lead to a contradiction.

• Symmetry of $\neq$ was not part of my confusion. – kccu Apr 7 '17 at 19:19
• @kccu Understood. I updated my answer to address what I think your professor really meant – Bram28 Apr 7 '17 at 19:24
• Why the downvote? – Bram28 Apr 7 '17 at 19:24
• I did not downvote, but I suspect it is because your original answer did not address my question. However, is it really true that because there is a model it is impossible to derive a contradiction? I thought it was not possible to prove the consistency of arithmetic. – kccu Apr 7 '17 at 19:26
• @kccu But we can prove the consistency of proof systems, i.e. of logic itself. So, if there is a model for a set of statements, you really cannot derive a contradiction from it (using a sound proof system). – Bram28 Apr 7 '17 at 19:27