Q11.8 of Boolos textbook - proving that $m \neq n$

Question

I'm working through Boolos' Computability and Logic textbook, and I am stuck on a question:

Add to the theory $\Gamma$ in the proof of Theorem 11.4 the sentence

$\forall x \mathbf{0} \neq x' \& \forall x \forall y (x'=y' \rightarrow x=y) $

Show that $\mathbf{m} \neq \mathbf{n} $ is then implied by $\Gamma$ for all natural numbers $m\neq n$ where $\mathbf{m}$ is the usual numeral for $m$.

I'm unsure how to start this.

I think I may also be confused by what the nature of "$\neq$" is. Is this just a new symbol that they are introducing, i.e. the new sentence could equivalently be written:

$\forall x NEQ(\mathbf{0}, x') \& \forall x \forall y (x'=y' \rightarrow x=y) $?

If so, I'm unclear how to deduce anything about $NEQ(\mathbf{m}, \mathbf{n})$. This could just be a relation which returns true whenever 0 is the first argument.

Answer 1

$\bf m \ne n$ is an abbreviation for $\lnot(\mathbf m=\mathbf n),$ not a new relation symbol.

You can prove $\lnot(\mathbf m=\mathbf n)$ by contradiction. Assume $\mathbf m = \mathbf n.$ Then you can use an instance of $\forall x,y (x'=y'\to x = y)$ to get $\mathbf{m-1}=\mathbf{n-1},$ and do that until you have $\mathbf{m-k}=\mathbf 0$ (assuming $m>n$), which contradicts $\forall x(\mathbf 0 \ne x').$

(Note here that $\mathbf m-\mathbf k$ is the numeral corresponding to the number $m-k$, not a subtraction of two numerals.)

Answer 2

Just to elaborate on the answer of @spaceisdarkgreen ...

In order to (mathematically) prove that the statement $\bf m \ne n$ is always (formal logically) provable for any numbers $m \neq n$, you want to use induction.

In particular, it's probably good to first prove that for any numbers $m$ and $n$ where $m < n$, you can prove $\bf m \ne n$, and from there it is easy to show that for any numbers $m$ and $n$ where $m > n$, you can prove $\bf m \ne n$: given $m >n$, then $n < m$, so you can prove $\bf n \ne m$, and so if you assume $\bf m = n$, you'd get $\bf n \ne n$ which is a contradiction, meaning that you have $\bf m \ne n$.

Now, like I said, to prove that for any numbers $m$ and $n$ where $m < n$, you can prove $\bf m \ne n$, use induction.

In particular, use induction on $m$: Prove that for any $m$, it is true that for any $n$: if $m < n$, then you can prove $\bf m \ne n$

Base: $m=0$. Well, for any $n$, if $m < n$, then that means that $\bf n$ is of the form $\bf p'$ for some number $p$, and by the given axiom, we can prove $\bf 0 \ne p'$

Step: move from $m$ to $m+1$. OK, so suppose we take any $n$ with $m +1 < n$. Then we can say that $n=p+1$ for some $p$, i.e. $m+1 < p+1$, and therefore also $m < p$ for which, by induction hypothesis, we can prove the corresponding $\bf m \ne p$ . So, in a formal proof, you could assume $\bf m+1 = p+1$, then use the axiom to show that $\bf m = p$, and that contradicts $\bf m \ne p$, meaning that we have a proof that $\bf m+1 \ne p+1$