peano arithmetic - addition associativity In studying Peano Arithmetic, there was an example that I'm having trouble seeing how the induction axiom works.
The example I was looking at was to show that PA proves the associative law for addition, that is $\forall x \forall y \forall z((x+y)+z = x+(y+z))$. Here's the solution given by my textbook
Most of the solution made sense, but I have a few questions regarding it's overall structure:


*

*The solution refers to $Ind(A(z))$ twice. Is it implied that its known what the induction axiom does to $A(z)$? To improve on this solution, is there a way to expand on the $Ind(A(z))$ to make it clear on what the axiom is doing to $A(z)$ in the solution?

*Comparing to this method for proving the associative law for +, what are the main differences between the PA proof and this one? The main difference I see is that the induction axiom plays a role in proving using PA but is there something else I'm missing?

*I was told that the solution does not need to be fully in PA, but it can be shown that the solution can be given in PA. Does the solution fufill this requirement?
Thanks for reading and helping!
 A: Ind(A(z)) is literally just the statement of mathematical induction, in the special case of the predicate A.
The two proofs you listed are the same proof, except that the chains of equalities are depicted in the reverse order.
A: I'll address your last two questions first:


  
*Comparing to this method for proving the associative law for +, what are the main differences between the PA proof and this one? The main difference I see is that the induction axiom plays a role in proving using PA but is there something else I'm missing?
  

The two proofs are really the same. The first one is just more formal by providing quantified formal logic statements and a formal logic expression of the induction scheme.


  
*I was told that the solution does not need to be fully in PA, but it can be shown that the solution can be given in PA. Does the solution fufill this requirement?
  

Actually the proof given is fully in PA: every step is justified by P3, P4, or pure logic. Though see at the end of this Answer for a full formal proof, if that is what is sought after.
OK, now the first question:

  
*
  
*The solution refers to $Ind(A(z))$ twice. Is it implied that its known what the induction axiom does to $A(z)$? To improve on this solution, is there a way to expand on the $Ind(A(z))$ to make it clear on what the axiom is doing to $A(z)$ in the solution?
  

Once $A(z)$ has been specified, then we indeed know exactly what $Ind(A(z))$ looks like. In the proof, they set $A(z): (x + y) + z = x + (y + z)$, so with that, $Ind(A(z))$ becomes:
$\forall x \forall y \big( \big[ (x + y) + 0 = x + (y + 0) \land \forall z \: ((x + y) + z = x + (y + z) \rightarrow (x + y) + sz = x + (y + sz))\big] \rightarrow \forall z \: (x + y) + z = x + (y + z) \big)$
To use this induction scheme to prove $\forall x \forall y \forall z \: (x + y) + z = x + (y + z)$, you would do the inductive proof within a universal proof. That is, you would set up the universal proof by saying that $x$ and $y$ are arbitrary objects, and so by the induction scheme above, we have:
$\big( \big[ (x + y) + 0 = x + (y + 0) \land \forall z \: ((x + y) + z = x + (y + z) \rightarrow (x + y) + sz = x + (y + sz))\big] \rightarrow \forall z \: (x + y) + z = x + (y + z) \big)$
Then, as the book does, prove the base case:
$(x + y) + 0 = x + (y + 0)$
and the inductive step:
$\forall z \: ((x + y) + z = x + (y + z) \rightarrow (x + y) + sz = x + (y + sz))$
Conjunct these two, and perform Modus Ponens to get 
$\forall z \: (x + y) + z = x + (y + z)$
And finally, complete the universal proof. That is, since $x$ and $y$ were arbitrary:
$\forall x \forall y \forall z \: (x + y) + z = x + (y + z)$
Below is a 'Fitch-style' formal proof for this whole process:

