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

Question

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.

Answer 1

It depends on the rules of the proof system that you are working with ...

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.