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

Question

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.

Answer 1

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

Answer 2

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.