1. Nov 13, 2014

### HMPARTICLE

1. The problem statement, all variables and given/known data
For any natural numbers a,b,c, we have (a+b) + c = a + (b + c)

2. Relevant equations
Definition 2.2.1

Let m be a natural number. To add zero to m, we define 0 + m := m. Now suppose inductively that we have defined how to add n to m. Them we can add n++ to m by defining (n++) + m := (n + m)++.

Lemma 2.2.2
For any natural number n, n + 0 = n.

Lemma 2.2.3
For any natural numbers n and m , n + (m++) = (n+m)++

3. The attempt at a solution
We shall use induction on (a+b)
First we do the base case, c = 0.

By the definition of addition 0 + (a+b) = (a+b), while by lemma 2.2.2 (a+b) + 0 = (a+b). Thus the base case is done. Now suppose inductively that c + (a+b) = (a+b) + c, Now to we have to prove that c++ + (a+b) = (a+b) + c++ to close the induction.
By the definition of addition, c++ + (a+b) = (a+b+c)++ and while by lemma 2.2.3 (a+b) + c++ = (a+b+c)++. This is equal to (a+b+c)++ by the inductive hypothesis c + (a+b) = (a+b) + c. Thus c++ + (a+b) = (a+b) + c++ . Also suppose inductively that a + (b+c) = (b+c) + a.
Now to we have to prove that a++ + (b+c) = (b+c) + a++ to close the induction.
By the definition of addition, a++ + (b+c) = (a+b+c)++ and while by lemma 2.2.3 (b+c) + a++ = (a+b+c)++. This is equal to (a+b+c)++ by the inductive hypothesis a + (b+c) = (b+c) + a. Thus a++ + (b+c) = (b+c) + a++.

so (a+b) + c++ = (a+b+c)++ and (b+c) + a++ = (a+b+c)++
Hence
(a+b) + c = a + (b + c)

----------------------------------------------------------
Now is this a correct proof? if so, is it a decent one.

It seems to make sense to me.

2. Nov 13, 2014

### Joffan

I'd be a little anxious about your use of '(a+b+c)', which is not well-defined.

Personally I would probably start from (a+b)+0 = a + (b+0) and run induction on that.

3. Nov 13, 2014

### HMPARTICLE

Now suppose inductively that c + (a+b) = (a+b) + c, Now to we have to prove that c++ + (a+b) = (a+b) + c++ to close the induction....

I would write;
Now suppose inductively that (a+b)+0 = a + (b+0), Now to we have to prove that (a+b) + 0++ = a + (b+0)++ to close the induction.
By the definition of addition, 0++ + (a+b) = 1 + (a+b) and while by lemma 2.2.3 (a+b) + 0++ = (a+b) + 1. This is equal to 1 + (a+b) . Also
suppose inductively that (b+0) + a = a + (b+0), Now to we have to prove that (b+0)++ + a = a++ + (b+0)++ to close the induction.
By the definition of addition, (b+0)++ + a = b + a + 1 and while by lemma 2.2.3 (b+0) + a++ = b + a + 1.
so (a+b) + 0++ = a + (b+0)++.
Therefore (a+b)+0 = a + (b+0) by mathematical induction.

How would i introduce c?

4. Nov 13, 2014

### Joffan

You can show that (a+b)+0 = a+(b+0) just by using Lemma 2.2.2 (twice)

What I'm suggesting is that you then show that [ (a+b)+c = a+(b+c) ] ⇒ [ (a+b)+(c++) = a+(b+(c++)) ] , which should just be a couple of uses of Lemma 2.2.3.

5. Nov 13, 2014

### HMPARTICLE

i see; from what you have said, this is what i have come up with

First we show that (a+b) + 0 = a + (b+0)
By definition 2.2.1;
(a+b) +0 = a+b,
and by lemma 2.2.2
a + (b+0) = a+b.

Now we show that (a+b) + c = a + (b+c)
by lemma 2.2.3;
(a+b) + c++ = (a+b+c)++
also
a + (b+c)++ = (a+b+c)++

so (a+b) + c+ = a + (b+c)++ and by axiom 2.4 we deduce that (a+b) + c = a + (b+c).

Also thanks for being patient with me.

6. Nov 13, 2014

### Joffan

(a+b+c) still doesn't mean anything, you have to avoid using this formulation. It means that there is an extra step where you use the given statement of the inductive step.

Also you have to justify that a+(b+(c++)) = a+(b+c)++

Last edited: Nov 13, 2014
7. Nov 13, 2014

### HMPARTICLE

thank you!

Last edited: Nov 13, 2014