Newbie to induction attempt to find natural deduction proof with given axioms

Question

I am trying to prove the conjecture:

$∀x.∀y.∀z.(x+y)+z=x+(y+z)$

I have access to the following axioms plus induction, and the others regular rules of natural deduction.

$A1: nat(0)$

$A2: nat(T) ⊢ nat(s(T))$

$A3: nat(T), nat(U) ⊢ nat(T+U)$

$A4: nat(T), nat(U) ⊢ nat(T · U)$

$A5: 1=s(0)$

$A6: ∀x. 0+x=x$

$A7: ∀x.∀y.s(x)+y=s(x+y)$

$A8: ∀x.0·x = 0$

$A9: ∀x.∀y.s(x)·y = y + x · y$

I am really close to completing this proof however I am not sure about how to complete it with the brackets issues...:

Answer 1

The trouble you are having is because you never use your inductive hypothesis (line 16). This is what you need to go through:

$(s(a2) + a3) + a4 = (\text{using} A7: s(a2) + a3 = s(a2 + a3))$

$s(a2 + a3) + a4 = (\text{using } A7 \text{ again})$

$s((a2 + a3) + a4) = (\text{use inductive hypothesis! }(a2 + a3) + a4 = a2 + (a3 + a4))$

$s(a2 + (a3 + a4)) =(\text{using } A7)$

$s(a2) + (a3 + a4)$

Below is a formal proof using the computer program called Fitch (which comes with the book Language Proof and Logic):

Please note how the formal proof closely mirrors the mathematical algebraic proof as shown at the beginning of this post: for every mathematical step, I do two steps in the formal proof, a $\forall \: Elim$ followed by a $= \: Elim$. I also start with a 'LHS=LHS' (LHS: left-hand side) statement at the start using a $= \: Intro$ to get the gradual transformation started. I know you do all these steps at some point as well in your proof, but the order in which you do them seem a bit less organized, so I encourage you to follow the systematic transformation as I do in my proof, because otherwise it is very easy to get lost in all the symbol strings, as I am sure you have noticed!

OK, I got the darn thing ... what a hellish interface!

Answer 2

It doesn't follow. [Or didn't before "and induction!"]

Take the model for Robinson Arithmetic and hence your arithmetic at p. 69 of my Gödel book -- and you will see that in that model, with $a$ and $b$ as defined, $(a + b) + a \neq a + (b + a)$.

The basic point is that, since you have no induction axiom inside your arithmetic, you can prove almost none of even the simplest general truths of arithmetic.

I'm being a bit terse, as I have already answered a similar question from the OP -- I'm not sure what book/set of lecture notes is being used here, but something is going awry.