Does this in complete detail prove $\forall x, y \in N, x + (y + 0) = (x + y) + 0$?

Question

My goal is to prove math theorems without skipping any steps. Is this proof correct?

I googled Peano exercises

I found: http://www.public.coe.edu/~jwhite/s11/fndho5.s11.pdf

Question 1 says to prove the following from Peano Axioms: $\forall x, y \in N, x + (y + 0) = (x + y) + 0$.

1. Axiom: $\forall x (x + 0 = x)$, therefore $\forall y (y + 0 = y)$ (substituting $x$ for $y$).

2. Axiom: $\forall x (x=x)$ therefore $\forall x, y \in N, x + (y + 0) = x + (y + 0)$. Can you do this in a single step? Or would you need to build up the expression on either side?

3. 2: $\forall x, y \in N, x + (y + 0) = x + (y + 0)$ and 1: $\forall y (y + 0 = y)$ therefore $\forall x, y \in N, x + (y + 0) = x + y$ (substituted the second instance of $(y + 0)$ for $y$).

4. Axiom: $\forall x (x + 0 = x)$, therefore $\forall x,y ((x + y) + 0 = (x + y))$ (substituting $x$ for $(x + y)$). Is this valid?

5. Axiom: $\forall a,b ((a = b) \implies (b = a))$ and 4: $\forall x,y (((x + y) + 0) = (x + y)))$ therefore $\forall x,y ((x + y) = ((x + y) + 0))$ (substituting $((x + y) + 0)$ for $a$ and $(x + y)$ for $b$).

6. 3: $\forall x, y \in N, x + (y + 0) = x + y$ and $\forall x,y ((x + y) = ((x + y) + 0))$ therefore $\forall x, y \in N, x + (y + 0) = (x + y) + 0$ (substituting $((x + y) + 0)$ for $(x + y)$). Question 1 has been proved.

Something that puzzles me - does this mean $\forall x (x=x)$ that $x$ doesn't have to be used by substituting a constant like $1$, $2$, etc. but can be an expression like $a+b$?

Answer 1

To answer you last question, yes - $\forall x P(x)$ lets you substitute any expression for $x$, as long as you do it carefully. For example, when you have an expression like $xy$ then substituting $a+b$ for $y$ needs to be protected with parentheses, i.e. you get $x(a+b)$ rather than $xa+b$ since those are two very different things.

As for your proof, it looks pretty good. At this level of rigor, all of the steps are required, but once you get past the foundational proofs it's standard to leave some of the details as given (e.g. basic algebraic manipulation like swapping $a=b$ and $b=a$ doesn't require stating an axiom).

Answer 2

You use a bit of an unusual proof technique where you move from one universal statement to another.

It's not wrong, but typically, a proof like this would start with something like:

"Let $a$ and $b$ be any numbers. Given the axiom that says that $\forall x \ x + 0 = 0$, we can say that $(a + b) + 0 = a + b$. ...[bla bla] ... and therefore $a + (b + 0) = (a + b) + 0$. Since $a$ and $b$ were arbitrary, this means $\forall x \forall y \ x + (y + 0) = (x + y) + 0$."

So note that by picking arbitrary objects, you can ignore all universals until the very end. I think it's a bit easier to follow ... and it's compatible with most treatments of formal logic involving quantifiers.