Definition of the sum of natural numbers

Question

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)?

Answer 1

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