Addition is Primitive Recursive
Theorem
The function $\Add: \N^2 \to \N$, defined as:
- $\map \Add {n, m} = n + m$
Proof
We observe that:
- $\map \Add {n, 0} = n + 0 = n$
and that
- $\map \Add {n, m + 1} = n + \paren {m + 1} = \paren {n + m} + 1 = \map \Succ {\map \Add {n, m} }$
where $\Succ$ is the successor function, which is a basic primitive recursive function.
We are to show that $\Add$ is defined by primitive recursion.
So we need to find primitive recursive functions $f: \N \to \N$ and $g: \N^3 \to \N$ such that:
- $\map \Add {n, m} = \begin{cases}
\map f n & : m = 0 \\ \map g {n, m - 1, \map \Add {n, m - 1} } & : m > 0 \end{cases}$
Because $\map \Add {n, 0} = n$, we can see that:
- $\map f n = n$.
That is, $f$ is the basic primitive recursive function $\pr_1^1: \N \to \N$.
Because $\map \Add {n, m + 1} = \map \Succ {\map \Add {n, m} }$, we can see that $g$ needs to be a function which maps the ordered triple $\tuple {n, m, \map \Add {n, m} }$ to $\map \Succ {\map \Add {n, m} }$.
A suitable function is:
- $g: \N^3 \to \N$ where $\map g {n_1, n_2, n_3} = \map \Succ {n_3}$
because then:
- $\map g {n, m, \map \Add {n, m} } = \map \Succ {\map \Add {n, m} }$
It remains to be shown that $g$ is primitive recursive.
This is achieved by using the projection function:
- $\map g {n_1, n_2, n_3} = \map \Succ {\map {\pr_3^3} {n_1, n_2, n_3} }$
Thus $g$ is obtained by substitution from the basic primitive recursive functions $\Succ$ and $\pr_3^3$ and so is primitive recursive.
So $\Add$ is obtained by primitive recursion from the primitive recursive functions $\pr_1^1$ and $g$, and so is primitive recursive.
$\blacksquare$