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.