# 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:

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

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

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

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.

• So does the first solution given by the textbook not demonstrate that the proof can be constructed in PA as it's still the same as the 2nd proof? – Jack Williams Mar 23 '17 at 5:50
• @Jack: I honestly don't see where you get that idea. For each A, Ind(A(z)) is one of the axioms of PA, in case that wasn't clear. – user14972 Mar 23 '17 at 6:03

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

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

1. 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: • Just to help answer (3), the "not fully in PA" might mean "meta-proof that a proof in PA exists". This is very frequently done, because it's just too tedious to construct the proof itself. For example if you use the deduction theorem in a Hilbert-style calculus, you need to work in the meta-system and would essentially prove existence of a proof in the target system, without actually showing it. – user21820 Mar 23 '17 at 13:58
• @user21820 Ah! Yes, that makes sense, thanks! – Bram28 Mar 23 '17 at 14:02