Addition of natural numbers

Addition $+ : \mathbb{N} \times \mathbb{N} \to \mathbb{N}$ is defined by recursion on the second argument: for each fixed $m \in \mathbb{N}$,

$m + 0 = m, \qquad m + \sigma(n) = \sigma(m + n).$

This is a definition by recursion, and it requires justification: it does not directly say what $m + n$ is, but pins down $m + 0$ and reduces $m + \sigma(n)$ to $m + n$. The recursion theorem (The recursion theorem) guarantees that for each $m$ there is exactly one function $n \mapsto m + n$ obeying these two equations, so $+$ is a well-defined total binary operation (Addition is a well-defined total operation).

Taking $m = n = 0$ gives $0 + 0 = 0$. The equation $m + \sigma(n) = \sigma(m+n)$ with $n = 0$ gives $m + 1 = m + \sigma(0) = \sigma(m + 0) = \sigma(m)$, so $\sigma(m) = m + 1$: the successor is "add one", recovering the familiar reading of the Peano successor. The basic laws (commutativity, associativity, cancellation, and the left identity $0 + n = n$) are not built in and must be proved by induction (Left identity for addition, Addition is commutative, Addition is associative, Addition is cancellative).