I Formal derivation of statement from Peano Arithmetic system

[cianfa72]

TL;DR Summary

About the formal derivation of a (meta)-statement from axioms of Peano Arithmetic formal system

I was reading a Bachelor thesis on Peano Arithmetic (PA). PA has the following axioms (not including the induction schema):
$$\begin{align}
& (A1) ~~~~ \forall x \neg (x + 1 = 0) \nonumber \\
& (A2) ~~~~ \forall xy (x + 1 =y + 1 \to x = y) \nonumber \\
& (A3) ~~~~ \forall x (x + 0 = x) \nonumber \\
& (A4) ~~~~ \forall xy (x + (y +1) = (x + y ) + 1) \nonumber \\
& (A5) ~~~~ \forall x (x \cdot 0 = 0) \nonumber \\
& (A6) ~~~~ \forall xy (x \cdot (y + 1) = (x \cdot y) + x) \nonumber
\end{align}
$$
The thesis claims the (meta)-statement $\text{PA} \vdash \varphi(0)$ where $\varphi(z)$ is the open well-formed formula (wff) $$\forall xy (x + (y + z) = (x + y) + z)$$ However I'm not sure how, from a formal viewpoint, it follows from axiom A3. Can you kindly help me ?

 

[mad mathematician]

You need to use induction on z and to invoke an instance of A4.

 

[cianfa72]

You need to use induction on z and to invoke an instance of A4.

Sorry, could you be more explicit about this ? Thanks.

 

[mad mathematician]

You want to use A4 to prove associativity of addition, so
we have for z=1: (x+y)+1=x+(y+1) this is an instantiation of axiom A4.
Now we use induction: suppose for z=n we have (x+y)+n=x+(y+n), now for z=n+1 we get: ((x+y)+(n+1))=((x+y)+n)+1=(x+(y+n))+1=x+((y+n)+1)=x+(y+(n+1)).
In the first equality (lhs) I used instantiation of A4, in the second equality it's the hypothesis of induction, the third equality is another instantiation of A4, and also the last equality is an instantiation of A4.

So we proved the associative of addition in PA, i.e $\varphi(z)$, $\varphi(0)$ is just the claim that x+y=x+y, which follows as always from reflexivity of '=', identity.

 

[cianfa72]

You want to use A4 to prove associativity of addition, so
we have for z=1: (x+y)+1=x+(y+1) this is an instantiation of axiom A4.
Now we use induction: suppose for z=n we have (x+y)+n=x+(y+n), now for z=n+1 we get: ((x+y)+(n+1))=((x+y)+n)+1=(x+(y+n))+1=x+((y+n)+1)=x+(y+(n+1)).
In the first equality (lhs) I used instantiation of A4, in the second equality it's the hypothesis of induction, the third equality is another instantiation of A4, and also the last equality is an instantiation of A4.

Sorry just to be sure: what you said in bold is an instance of axiom A4, you meant that formally (x+y)+1=x+(y+1) is the instance of A4 where the name of variables entering it are actually x and y. Furthermore the universal closure $\forall xy$ (or $\forall x \forall y$) is implicitly understood.

On the other hand, for the first equality (LHS) you used the instantiation of A4 where the variables' name are (x + y) and n respectively.

So we proved the associative of addition in PA, i.e $\varphi(z)$, $\varphi(0)$ is just the claim that x+y=x+y, which follows as always from reflexivity of '=', identity.

Ah ok, that's right. However that thesis claims that $PA \vdash \varphi(0)$ follows from axiom A3 (i.e. there is a formal proof from it), I don't see how though...