# Does $n^\prime\ne n^{\prime\prime}$ require proof by contradiction? $n^\prime$ is the successor of $n$.

This is the statement of Peano's axioms I will assume for this discussion:

1. $$1$$ is a number.
2. To every number $$n$$ there corresponds exactly one number $$n^\prime.$$
3. $$n^\prime=m^\prime\implies n=m.$$
4. $$n^\prime\ne 1$$
5. Let $$P\left[x\right]$$ be a proposition (propositional form) containing the number variable $$x$$. If $$P\left[1\right]$$ holds and if $$P\left[n^\prime\right]$$ follows from $$P\left[n\right]$$ for every number n, then $$P\left[x\right]$$ holds for every number $$x$$.

My question is: does the proposition $$n^\prime\ne n^{\prime\prime}$$ require proof by contradiction? In particular does it require the kind of argument that appears in the induction step of the following proof:

If for some $$m\in\mathbb{N}$$ we had $$m^\prime=m^{\prime\prime},$$ then we would have $$n\in\mathbb{N}$$ such that $$m^\prime=n=n^\prime$$.

We now propose $$\forall_{x\in\mathbb{N}}\left[P\left[x\right]:=x\ne x^\prime\right]$$. To prove this we first observe that $$P\left[1\right]$$ is axiom 4. If we had $$P\left[n\right]\iff n\ne n^\prime$$ and $$\lnot P\left[n^\prime\right]\iff n^\prime= n^{\prime\prime},$$ then by axiom 3 we would have $$n= n^\prime\iff \lnot P\left[n\right].$$ So we have $$P\left[1\right]\land \left(P\left[n\right]\implies P\left[n^\prime\right]\right)\iff \left\{n\backepsilon P\left[n\right]\right\}=\mathbb{N}.$$

Since $$n\ne n^\prime$$ for all $$n\in\mathbb{N},$$ and $$n\in\mathbb{N} \implies n^\prime\in\mathbb{N}$$ we have $$n^\prime\ne n^{\prime\prime}.$$ QED

The reason I ask is that the proof I came up with is more complicated than I expected it to be. I'm sure it could be abbreviated by omitting some of the obvious steps, leaving them to the reader to infer. But can the structure of the argument be simplified? I'm also speculating that the fact that the hypothesis $$n^\prime\ne n^{\prime\prime}$$ contains what amounts to a logical negation it it, the proof also requires a logical negation.

• Related to your previous post... I think that the best strategy is to prove by induction : $\forall n (n \ne n')$, starting from Ax.4 as the base case. – Mauro ALLEGRANZA May 15 at 7:04
• IMO, the proof is not "complicated". The base case nedds only the use of Universal Instantiation rule : $\forall n (n' \ne 1) \to (1' \ne 1)$. And the induction step have to assume $n \ne n'$ (induction hypo) and assume (for contra) : $n' = n''$. By Ax.3 $n=n'$ and the contradiction is there. – Mauro ALLEGRANZA May 15 at 7:13
• I started out as you suggest, with axiom 4. My first attempt was to assume $n=n^\prime$ which immediately fails for $n=1$. But then I realized that I had only shown that $n=n^\prime$ fails for some number. – Steven Thomas Hatton May 15 at 7:31

If you had Contraposition, you could take $$n' = n'' \to n = n'$$ and transform that into $$n \not = n' \to n' \not = n''$$, and then it's a simple Modus Ponens to go from $$n \not = n'$$ to $$n' \not = n''$$.
However, few systems have Contraposition as an inference rule; most have $$\neg Intro$$ (i.e. the formalization of proof by contradiction) as the only way to introduce a negation.