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,m+\sigma (n)=\sigma (m+n)\mathrm{.}$

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