Why isn't the additive identity also an axiom?

Question

In the Peano axioms, the concept of addition is described:

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

where $S(n)$ is the successor function. As far as I can tell $a+0=a$ is (even in books such as Tao's Analysis vol 1) not an axiom but rather an identity or a definition.

Why is this so? To my mind an axiom is something we accept as true without further proof, which seems to be exactly what $a+0=a$ is doing. I accept that it's an identity, but if we are to call it a definition as well, to me a definition is a sort of "relabeling" or "rewording" of something.

For example we might "define" $1 := S(0)$ or $2 := S(S(0))$ or even $2 := S(1)$ because all those nested functions become unwieldy. But my point here is that the "definition" is simply placing some new notation or syntax or label on something that we can already describe in other terms.

So if $a+0=a$ isn't an axiom we simply accept as true, and it is a definition instead, how do we describe the underlying operations in terms of the stuff we already have? What is $a+0=a$ formally "shorthand for"? Is it a matter of first-order logic? Functions?

For example I might think that $a+0=a$ is a way to say $a$ is shorthand for some arbitrarily-deep nested successor function stack and then $+0$ is equivalent to "not recursing any further" but I don't know if this is right or if this is even how it's formally described.

How do we break down $a+0=a$ even further? What is it a definition of? Why do we not call this an axiom as well?

Edit: To be clear, I completely understand that $a+0=a$ is the "base case" of an inductive concept $a+S(b)=S(a+b)$ -- but this is not what my question is about.

Answer 1

Recall the principle of recursive definition:

Let $z$ be any element of a set $X$ and let $r : X \to X$ be any function. There is a unique function $f : \mathbb{N} \to X$ such that:

• $f(0) = z$
• $f(S(n)) = r(f(n))$ for every $n \in \mathbb{N}$

In this case, we choose:

• $z = a$
• $r = S$

then the principle of recursive defintion gives a function — one we will call "$a + $" such that

• $``a+"0 = a$
• $``a+" S(x) = S(``a+"x)$

The equation $a+0=a$ is 'shorthand' for "If you take the function given by the principle of recursive definition to the choices of $z=a$ and $r=S$ and apply it to zero, you get $a$.

(of course, $a$ is a variable, and this defines for every natural number $n$ the corresponding function $n+$; by uncurrying we collect these into a single bivariate function we call $+$)

---

For practical usage, this isn't really any different than adding a new unary operation symbols "a+" to the language and take the formulas above as axioms. (or adding a binary operation symbol "+").

Generally, you won't see people bother to distinguish between the two unless they're doing technical work in formal logic.

Answer 2

The axioms just describe the natural numbers, not addition of the natural numbers. The axioms don't say anything about addition. The definition of the addition function includes the fact that $a+0=a.$

Answer 3

It's an axiom. $0$ is defined (or declared to exist, if you like that phrase better) in a previous axiom as the only element which isn't the successor of any other element. Once we want to define / declare the operation of addition, we need to establish how it works. One of the axioms of addition is that $a+0=a$ for all $a\in \Bbb N$.

Answer 4

The peano axioms do not deal with addition, they axiomatize the natural number as such, by introducing a $0$ and for each number a successor. Addition is then defined from that starting point. Both $a+0 :\!= a$ and $a+S(b) :\!=S(a+b)$ are definitions and this is also how Tao states it in Definition 2.2.1.