Definition of the sum of natural numbers

After define the natural numbers using the Peano axioms, I'm trying to understand the definition of sum between natural numbers, let $s$ be the successor function used in the Peano axioms. The most natural definition of sum of natural numbers is $m+n=s^n(m)$, i.e., the sum $m+n$ is the function $s$ iterated $n$ times at the element $m$. But what does it mean the phrase "$n$ times", if we don't have this concept yet (for while $n$ is only an element of the natural numbers)?

Thanks

You may think that is the "most natural" definition, but that's not how it is ever defined, for the reason that you gave. Instead, it can be recursively defined by the equations

\begin{align} m + 0 & = m\\ m + s(n) & = s(m + n) \end{align}

which don't depend on any notion of "$n$ times". Note that for any sum of the form $m+n'$, either $n'$ is equal to $0$, in which case the first clause applies, and the sum can be evaluated immediately, or $n'$ is the successor $s(n)$ of some natural number $n$, in which case the second clause applies, and we can compute the sum in terms of a strictly simpler sum.

For example, to determine the value of $X = s(0)+s(0)$ we turn to the second clause, which asserts that this sum is equal to $s(s(0)+0)$. Since the first clause tells us that the inner sum $s(0)+0$ is equal to $s(0)$, the sum $X$ is equal to $s(s(0))$, which is the correct answer.

This technique is how one would generally formalize "$f$ iterated $n$ times" in Peano arithmetic (and related settings): If \begin{align} g(m,0) &= m \\ g(m,s(n)) &= f(g(m,n)) \end{align} then $g(m,n)=f^n(m)$ for all $m$ and $n$.

• yes, I agree with you, but how can you define $m+n$ using your definition? – user42912 Jan 28 '15 at 19:44
• @user42912: The first set of displayed equations is the usual definition of $m+n$. – hmakholm left over Monica Jan 28 '15 at 19:44
• Not that it matters, but I am accustomed to $m+s(n)=s(m+n)$. – André Nicolas Jan 28 '15 at 19:49
• @Trevor Feel free to edit. – MJD Jan 28 '15 at 20:09
• @user42912: The "Peano axioms" come in two different flavors. In Peano's original formulation (which doesn't mention addition) it is tacitly assumed that enough set theory or higher-order reasoning is available as a background theory to know that recursive definitions are possible. On the other hand, in the modern first-order formulation, usually known as "Peano Arithmetic", addition is a primitive concept and its two defining equations are axioms. In that case you don't need a recursion theorem because the axioms explicitly assert that the function exists. – hmakholm left over Monica Jan 30 '15 at 13:10