Why isn't $0+a=a$ something we derive?

Question

In the usual natural number definition of addition $0+a=a$ is taken as true by definition. This feels like it should be something we derive from $0+0=0$, instead? As in, let's define addition this way:

$0+0=0$

$a+S(b)=S(a+b)$

Then prove the result:

Claim: $0+a=a$

Base case: $0+0=0$ by definition.

Inductive step: Suppose $0+a=a$. We must show that $0+S(a)=S(a)$. By definition of addition, $0+S(a)=S(0+a)$ then by inductive hypothesis equals $S(a)$ and we are done.

In other words we can derive the result rather than assume it true, so why do we skip this step usually?

Answer 1

Because defined that way you do not know how to compute $a+0$.

The axiom $0+0$ does not apply and neither the axiom $a+S(b)$ does, because $0$ is not a successor.

Example: how to compute $1+0$ with the purported definition of sum ? $1$ is $s(0)$: thus, the axiom $0+0=0$ will not work. But $0$ is not $s(n)$ for some $n$: thus, also the axiom $1+s(b)=s(1+b)$ will not work.

---

We must think at the axioms for sum (and the same for product) as rules to perform sum.

They allows us to complete the task working "backward" step by step.

If we have to compute e.g. $5+3$ we know that $3=s(2)$ and we apply the second axiom to get:

$5+3=5+s(2)=s(5+2)$.

And then we use the fact that $2=s(1)$ to get:

$5+3=5+s(2)=s(5+2)=s(5+s(1))=s(s(5+1))$.

Finally, with $1=s(0)$ we get to the end, using the first axiom:

$5+3=5+s(2)=s(5+2)=s(5+s(1))=s(s(5+1))=s(s(5+s(0)))=s(s(s(5+0)))=s(s(s(5)))=s(s(6))=s(7)=8.$.

Answer 2

As in, let's define addition this way: $$0+0=0$$ $$a+S(b)=S(a+b)$$

When you attempt to define a function like addition, a good start is to consider it as a general function. Even granting a domain of natural numbers and that the successor is +1, you have:

$$f(0, 0) = 0$$ $$f(a, b+1) = f(a, b) + 1$$

Try to think of another function with that property. One that comes to my mind is $f(x, y) = y$.