Peano axioms: $∀y∀x(x×y = y×x)$, using induction in $y$

Question

Considering a first order logic language for arithmetic and the Peano's axioms (PA) for the number theory get natural deduction (with Fitch notation) for the following $\psi$ formulas (i.e. PA $⊢ \psi$).

Peano's axioms:

1. $∀x(x+1 \neq 0)$
2. $∀x∀y(x+1 = y+1 → x = y)$
3. $0+1 = 1$
4. $∀x(x+0 = x)$
5. $∀x∀y(x+(y+1) = (x+y)+1)$
6. $∀x(x×0 = 0)$
7. $∀x∀y(x×(y+1) = (x×y)+x)$
8. (principle of induction) $(\varphi[0/x] ∧ ∀x(\varphi → \varphi[x+1/x])) → ∀x$ $\varphi$

How to use Axiom 8: being $∀x$ $\varphi$ what you want to deduct, you should deduct $\varphi([0/x])$ first and then $∀x(\varphi → \varphi[x+1/x])$ (and using axiom 8 and modus ponens you get what you want).

Answer 1

Hint

You have to follow the "instructions" on how to use Ax.8 [the Induction axiom].

The first step is to find the correct formula $\varphi(x)$ to which apply the axiom; the natural choice is to consider :

$\varphi(x) := \forall y \ (x \times y = y \times x)$.

If so, $\varphi(0)$ will be : $\forall y \ (0 \times y = y \times 0)$ and thus the induction proof will be organized with :

(i) basis - prove that :

$\mathsf {PA} \vdash \forall y \ (0 \times y = y \times 0)$

i.e. $\mathsf {PA} \vdash \varphi(0)$;

(ii) induction step - prove that :

$ \forall y \ (x \times y = y \times x) \to \forall y \ ((x+1) \times y = y \times (x+1))$

i.e. $\mathsf {PA} \vdash \forall x \ [\varphi(x) \to \varphi(x+1)]$.

Finally, with (i) and (ii) use Ax.8 and $\to$-elim [i.e. modus ponens] twice to conclude with :

$\mathsf {PA} \vdash \forall x \ \varphi$.