How do I know what I need to show when using induction? (Peano axioms)

Question

As an exercise I wanted to prove that addition was commutative using the Peano axioms.

To quickly restate the definition of addition (where $S(n)$ is the successor function of $n$, which we can show is the same as $S(n) = n+1$):

$$\begin{align} a + 0 &= a \tag{additive identity} \\ a + S(b) &= S(a + b) \tag{addition of naturals} \end{align}$$

The axiom of induction then is the statement that:

$$\forall P(P(0) \land (P(k) \implies P(k+1)) \implies \forall n(P(n)))$$

Which means for all predicates, some base case being true and the $k$th case implying the $k+1$th case means that the predicate is true for all $n$.

For the purposes of this question, assume we have just proven that $a + 0 = 0 + a$, that $a + 1 = 1 + a$, and that $(a+b)+c = a+(b+c)$.

Then my question is how we're actually using this induction for proving the general commutative case $a+b=b+a$. Here is what I originally did:

Base case: We have $a + 0 = 0 + a$ as true.

Inductive step: Suppose $a+b = b+a$. Then $a+S(b) = S(a + b) = S(b + a) = b + S(a) = b + (a + 1) = b + (1 + a) = (b + 1) + a = S(b) + a$. We also have $(b+1)+a = (1+b)+a = 1+(b+a) = 1+(a+b) = (1+a)+b = S(a) + b$.

I figure that $P(0)$ here is when $k=0$ and we say $a+k = k+a$ is our base case, same as how we say $a + 0 = 0 + a$ is our base case.

But then what exactly is the $k+1$th case here? I mean I tried to show that $a+b=b+a$ implied all sorts of identities (I basically tried to sledgehammer it with every permutation I could think of) but I don't know exactly what is minimal and sufficient to prove the inductive step.

If the inductive hypothesis is $a+b=b+a$ and this is our $k$th step, i.e. $P(k)$ is true, what is $k$ here? $k=a$? $k=b$? Is it enough to show that $S(a) + b = b + S(a)$? If not, how do I know what all I must prove here?

I'm trying to stay strict within the definitions here so that I don't run the risk of letting intuition and "common sense" cheat myself of the understanding here.

How do I correctly interpret the $P$ statements here? What is $P(0)$? What is $P(k)$? What is $P(k+1)$ and what must I do to show it? Or is my induction axiom not correct? What should I be doing here?

Answer 1

We want to prove commutativity of sum, i.e.: $m+n=n+m$.

The proof has a first step by induction on $n$, and thus the $P(n)$ to be used with induction axioms is:

$a+n=n+a$.

(i) Basis: $a+0=0+a$ ($P(0)$), and

(ii) Induction step: assuming that $a+n=n+a$ holds (induction hypotheses) we have to prove that $a+s(n) = s(n)+a$.

Having done the two steps of induction, the Induction axioms allows to conclude with:

$\forall n \ (a+n=n+a)$.

The above result has been derived for a "generic" $a$ (for $a$ whatever): thus, we may geenralize it using Universal generalization to conclude with:

$\forall m \ \forall n \ (m+n=n+m)$.

Answer 2

In the vein of my previous answer, here's some Agda:

data _≡_ {A : Set} (a : A) : A → Set where
    Refl : a ≡ a

data ℕ : Set where
    Z : ℕ
    S : ℕ → ℕ

_+_ : ℕ → ℕ → ℕ
m + Z = m
m + S n = S (m + n)

cong : {A B : Set} → (f : A → B) → {x y : A} → x ≡ y → f x ≡ f y
cong f Refl = Refl

_trans_ : {A : Set} → {x y z : A} → x ≡ y → y ≡ z → x ≡ z
Refl trans q = q

left-additive-identity : {n : ℕ} → (Z + n) ≡ n
left-additive-identity {Z} = Refl
left-additive-identity {S n} = cong S (left-additive-identity {n})

left-increment : {m n : ℕ} → (S m + n) ≡ S (m + n)
left-increment {m} {Z} = Refl
left-increment {m} {S n} = cong S (left-increment {m} {n})

commutative : {m n : ℕ} → (m + n) ≡ (n + m)
commutative {Z} {n} = left-additive-identity {n}
commutative {S m} {n} = left-increment {m} {n} trans cong S (commutative {m} {n})

This uses the equivalent of three uses of the induction axiom. One each for left-additive-identity which proves that $0+n=n$ ($n+0=n$ comes automatically from the definition of _+_); left-increment which proves $(m+1)+n=(m+n)+1$; and commutativity itself. Refl represents reflexivity of equality. cong represents the congruence property of equality, i.e. that functions take equal inputs to equal outputs. This is only used in the form: if $m=n$, then $m+1=n+1$. trans is the transitivity of equality.