How can I prove this proposition from Peano Axioms: (Cancellation law). Let a, b, c be natural numbers such that a + b = a + c. Then we have b = c.

Question

Peano Axioms.

Axiom 2.1

$0$ is a natural number.

Axiom 2.2

If $n$ is a natural number then $n++$ is also a natural number. (Here $n++$ denotes the successor of $n$ and previously in the book the notational implication has been bijected to the familiar $1,2…$).

Axiom 2.3

$0$ is not the successor of natural number; i.e. we have $n++≠0$ for every natural number $n$.

Axiom 2.4

Different natural numbers must have different successors; i.e., if $n,m$ are natural numbers and $n≠m$, then $n++≠m++$.

Axiom 2.5

Let $P(n)$ be any property pertaining to a natural number $n$. Suppose that $P(0)$ is true, and suppose that whenever $P(n)$ is true, $P(n++)$ is also true. Then $P(n)$ is true for every natural number $n$.

Definition of Addition: Let m be a natural number. We define, $0+m=m$ and suppose we have inductively defined the addtion $n+m$ then we define, $(n++)+m=(n+m)++$. Where $n++$ is the successor of $n$.

Terence Tao has a proof in his Analysis I book, but I couldn't understand . I want a proof line by line like this:

Thm: 3 is a natural number \begin{align*} & 0 \text{ is natural } && \text{Axiom 2.1 }\\ & 0++ = 1 \text{ is natural } && \text{Axiom 2.2}\\ & 1++ = 2 \text{ is natural } && \text{Axiom 2.2}\\ & 2++ = 3 \text{ is natural } && \text{Axiom 2.2} \end{align*}

Answer 1

The proof is by induction on $a$.

Basis [case with $a=0$]. We want to prove that :

if $0+b=0+c$, then $b=c$.

But we have that : $0+b=b$, by definition of addition.

And also : $0+c=c$.

Thus, by transitivity of equality : $b=c$.

---

Induction step. Assume that the property holds for $a$ and prove it for $a'$ [I prefer to use $a'$ instead of $a++$ for the successor of $a$].

This means :

assume that "if $a+b=a+c$, then $b=c$" holds, and prove that "if $a'+b=a'+c$, then $b=c$" holds.

We have $a'+b=(a+b)'$ by definition of addition.

And $a'+c=(a+c)’$, by definition of addition.

We assume that : $a'+b=a'+c$, and thus, again by transitivity of equality, we have that : $(a+b)'=(a+c)'$.

By axiom 2.4 (different numbers have different successors), by contraposition, we conclude that $(a+b)=(a+c)$.

Thus, applying induction hypothesis, we have that :

$b=c$.

---

---

The general strategy used above in order to prove "if $P$, then $Q$", is to assume $P$ and derive $Q$.

This type of proof is called Conditional Proof; we can see it above :

1) if $a+b=a+c$, then $b=c$ --- induction hypothesis

2) $a'+b=a'+c$ --- assumption for CP

3) $(a+b)'=(a+c)'$ --- from 2) and definition of addition and tarnsitivity of equality

4) $a+b=a+c$ --- from 3) and axiom 2.4 by Contraposition [the axiom says : "if $(a+b \ne a+c)$, then $(a+b)' \ne (a+c)'$"; thus, contraposing it we get : "if $(a+b)' = (a+c)'$, then $(a+b) = (a+c)$"] and Modus ponens

5) $b=c$ --- from 4) and 1) by Modus ponens (also called : detachment)

6) if $a'+b=a'+c$, then $b=c$ --- from 2) and 5) by Conditional Proof.

Answer 2

Here is a formal proof done in Fitch:

(Note: I use $s(x)$ instead of $x$++)