# Peano axioms and commutativity of addition

I'm trying to prove the commutativity of addition in Peano arithmetic in something like a natural deduction system, but am stuck halfway (I say "something like a natural deduction system" because I don't really know how to format one here; I'll do my best to represent it, however). I must have gone wrong somewhere, but I cannot see how.

I am using axioms written as follows (leaving out those for multiplication):

A1. $$(\forall x) S(x) ≠ 0$$

A2. $$(\forall x)(\forall y) (S(x) = S(y) \rightarrow x = y)$$

A3. $$(\forall x) +(x, 0) = x$$

A4. $$(\forall x)(\forall y) +(x, S(y)) = S(+(x, y))$$

A5. Axiom schema of induction: For any formula $$\phi$$ built from =, $$S$$, +, with one free variable: $$[\phi (0) \space\And\space (\forall x)(\phi(x) \rightarrow \phi(S(x)))] \rightarrow (\forall x)\phi(x)$$

It's been recommended that I use the induction schema twice, first to prove $$(\forall x) +(0, x) = x$$, and then to get $$(\forall x)(\forall y)+(x, y) = +(y, x)$$. This is what I've done so far:

1. $$+(0, 0) = 0$$ $$\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space$$(A3 instantiation)
2. $$+(0, a) = a$$ $$\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space$$(assumption)
3. $$+(0, S(a)) = S(+(0, a))$$ $$\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space$$ (A4 instantiation)
4. $$+(0, S(a)) = S(a)$$ $$\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space$$(Leibniz's law, 2, 3)
5. $$+(0, a) = a \rightarrow +(0, S(a)) = S(a)$$ $$\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space$$ (conditional proof, 2-4)
6. $$(\forall x) (+(0, a) = a \rightarrow +(0, S(a)) = S(a))$$ $$\space\space\space\space\space\space\space\space\space\space\space\space$$ (universal generalization, 5)
7. $$[ +(0, 0) = 0 \space\And\space (\forall x) (+(0, a) = a \rightarrow +(0, S(a)) = S(a))] \rightarrow (\forall x) +(0, x) = x$$ $$\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space$$(A5 instantiation)
8. $$+(0, 0) = 0 \space\And\space (\forall x) (+(0, a) = a \rightarrow +(0, S(a)) = S(a))$$ (conjuction, 1, 6)
9. $$(\forall x) +(0, x) = x$$ $$\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space$$(modus ponens, 7, 8)

So this brings me to the end of the first induction, the result of which I seemingly am supposed to use to get to commutativity of addition. So I continued as follows:

1. $$+(0, b) = b$$ $$\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space$$(universal instantiation, 9)
2. $$+(b, 0) = b$$ $$\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space$$(A3 instantiation)
3. $$+(0, b) = +(b, 0)$$ $$\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space$$(Leibniz's law, 10, 11)
4. $$(\forall x) +(0, x) = +(x, 0)$$ $$\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space\space$$ (universal generalization, 12)

13 is the base case for the second induction. I've then tried to get the induction step by assuming $$(\forall x) +(a, x) = +(x, a)$$, and using this to find $$(\forall x) +(S(a), x) = +(x, S(a))$$ by conditional proof, with the plan to universally generalize over the dummy name 'a'.

However, I cannot seem to get it right – I keep ending up with, e.g., the wrong equivalences, and so cannot generate the correct generalization. But I don't know where I'm going wrong. Am I making the wrong assumption for the second conditional proof? Do I need something other than the information I've provided? Any help would be greatly appreciated.

Thanks!

• I did an exercise like this some years ago. It might be easier to first prove right-cancelability $(x+y = z+y \to x=z)$and associativity. – Dan Christensen Mar 31 at 3:21

• Lemma 1: $$\forall q, +(q,0) = +(0,q)$$. Proved by induction on $$q$$.
• Lemma 2: $$\forall p, \forall q, S(+(p, q))) = +(S(p), q)$$. Proved by induction on $$q$$.
Given the lemmas, to prove the overall result, we prove $$\forall x, \forall y, +(x,y) = +(y,x)$$ by induction on $$y$$. The base case is Lemma 1. For the inductive case, we have this outline of the calculation: $$\begin{split} +(x, S(y)) & =S (+(x,y))\\ &= S(+(y,x)) \\ &= +(S(y),x)). \end{split}$$ where the first line is from the definition of $$+$$, the second is the inductive hypothesis, and the third is lemma 2.