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 (note that n should be actually a standard numeral term of the underlying formal language).

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...

 

[mad mathematician]

Sorry just to be sure: when 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.


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 do not see why though...

In my derivation I forgot to mention that I use y+0=y; acknowledged we proved already x+(y+z)=(x+y)+z plug z=0, and get: x+(y+0)=(x+y)+0; now from the axiom A3 we have: y+0=y and (x+y)+0=(x+y), and you proved that also $\varphi(0)$ follows from A3.

 

[cianfa72]

x+(y+0)=(x+y)+0; now from the axiom A3 we have: y+0=y and (x+y)+0=(x+y), and you proved that also $\varphi(0)$ follows from A3.

Ok, so basically (x+y)+0=(x+y) is the axiom A3 with x+y in place of the first variable. So both y+0=y and (x+y)+0=(x+y) are instantiations of axiom A3.

From the latter by substitution y=y+0 only in the second occurrence of y we get $\varphi(0)$.