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.

  • $\begingroup$ I'm confused - in all presentations I've seen it is listed as an axiom (e.g. on Wikipedia). $\endgroup$ – Noah Schweber Mar 12 '18 at 19:01
  • $\begingroup$ In Tao's Analysis it is referred to as a definition (page 27) and kept separate from the other axioms he mentionos, and then over here mathworld.wolfram.com/PeanosAxioms.html addition is not lumped in with the typical axioms $\endgroup$ – user539262 Mar 12 '18 at 19:02
  • $\begingroup$ It is both. See my answer. $\endgroup$ – vrugtehagel Mar 12 '18 at 19:02
  • $\begingroup$ Also according to this answer math.stackexchange.com/a/1963970/539262 the Wiki page is not the usual representation of the axioms. $\endgroup$ – user539262 Mar 12 '18 at 19:04
  • $\begingroup$ The point is that (in many frameworks) + is not an innate part of the structure; it's an additional piece of structure layered over the top. Viewed from this perspective, $a+0=a$ is part of the definition of addition; it gives us a 'base case' from which we can use inductive principles (and specifically, the second part of the definition $a+Sb=S(a+b)$ to define addition for all pairs of numbers. $\endgroup$ – Steven Stadnicki Mar 12 '18 at 19:07

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.

  • $\begingroup$ I thought in the Peano axioms, you have to assume there exist addition and multiplication operations satisfying the recursive definitions, in order to then bootstrap into defining arbitrary recursively defined functions. i.e. without assuming these operations exist, the other axioms alone don't intrinsically allow you to define an addition operation recursively, at least not axiomatically in the restricted first-order Peano arithmetic theory. $\endgroup$ – Daniel Schepler Mar 12 '18 at 19:11
  • $\begingroup$ @DanielSchepler: Since this is from the introductory chapters of a text on analysis, I don't think the author intends to restrict himself to the first-order theory given by peano's axioms (or first-order theory of peano arithmetic). $\endgroup$ – Hurkyl Mar 12 '18 at 19:18
  • $\begingroup$ Is "principle of recursive definition" a first-order-logic concept? Something deeper? $\endgroup$ – user539262 Mar 12 '18 at 19:21
  • $\begingroup$ @user539262: It's a feature of any (reasonable) setting where one can quantify over functions from the natural numbers to itself. We could be working in first-order ZFC, some suitable type theory, ETCS, or some other thing; it doesn't really matter. IIRC, Tao deliberately tries to be agnostic about this choice; that everything he says about foundations is in a way that can be suitably interpreted in your favorite choice. $\endgroup$ – Hurkyl Mar 12 '18 at 19:27

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.$


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.

  • $\begingroup$ My question though is why are these merely definitions and not also axioms? If they are not axioms then it means we should be able to describe this definition formally in terms of the underlying principles no? $\endgroup$ – user539262 Mar 12 '18 at 19:13
  • $\begingroup$ The definition uses $0$ and the successor map, which are the underlying principles, no? $\endgroup$ – Christoph Mar 12 '18 at 19:14
  • $\begingroup$ Intuitively yes but I'd argue formally, something more is needed since we have to describe what the definition is shorthand for. Instead of numbers we could use any other labels instead. Say "elephant" is the element that is not a successor. Why is a+elephant=a? $\endgroup$ – user539262 Mar 12 '18 at 19:17
  • $\begingroup$ See Hurkyls answer for a formal treatment using the principle of recursive definition (which is a consequence of the peano axioms and the principle of induction). $\endgroup$ – Christoph Mar 12 '18 at 19:21

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$.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.