0
$\begingroup$

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.

$\endgroup$
  • 2
    $\begingroup$ 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. $\endgroup$ – Mauro ALLEGRANZA May 15 at 7:04
  • 1
    $\begingroup$ 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. $\endgroup$ – Mauro ALLEGRANZA May 15 at 7:13
  • $\begingroup$ 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. $\endgroup$ – Steven Thomas Hatton May 15 at 7:31
1
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ I don't fully understand what that means. If I were to assume contraposition as a rule of inference, I would do so as an abbreviation of the proofs of the rules of contraposition which appeal to the basic rules of classical logic. So having contrposition as a rule of inference wouldn't really change the structure of a proof, it would just move some of the steps elsewhere. $\endgroup$ – Steven Thomas Hatton May 21 at 2:54
  • $\begingroup$ @StevenThomasHatton True ... Contraposition can be seen as embodying an implicit proof by contradiction. But, some formal systems have a precise rule for Proof by Contradiction, and regard Contraposition as a different rule. $\endgroup$ – Bram28 May 21 at 15:18

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.