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.


  • 1
    $\begingroup$ 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. $\endgroup$ – Dan Christensen Mar 31 at 3:21

You are using the same plan I would use. The two key lemmas are:

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

  • $\begingroup$ Thanks, Carl! It looks like it's Lemma 2 that I'm missing. I don't think we've been provided it, so I'll have to prove it first. I can see how this will get me to where I need to go, but am nonetheless unsure that this is the intended route (though I don't see any other way at the moment!). $\endgroup$ – ata Mar 31 at 0:58
  • $\begingroup$ Update: I think I've now figured out proofs for both the second lemma and the commutativity of addition (writing them out natural-deduction style isn't so fun). Thanks again for your guidance :) $\endgroup$ – ata Mar 31 at 2:41
  • 1
    $\begingroup$ Great - I'm glad you got the proofs. I can sympathize with writing out all the details. $\endgroup$ – Carl Mummert Mar 31 at 12:27

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.