How to define addition on the naturals as a function rather than with the successor "function". It is my understanding that when an algebraic structure (in this case a commutative monoid) is equipped with an operation (in this case $+$) that binary operation is a function of two variables.
I usually define a function $f$ as a set of $n$-tuples. For example:
$$\div\equiv\{(x,y,z)\in\mathbb{\mathbb{R}}^3\mid x=y\times z \land y\not=0\}$$
Now we can call $\div(x,y)=z$. So, for example, $\div(15,3)=5$ or if we use more conventional notation: $15\div 3=5$.
My problem is that whenever I have seen references to the addition of natural numbers, it is in the context of the successor function $S(n)$. Thus addition is defined indirectly via two rules:
$$x+0=x$$
$$x+S(y)=S(x+y)$$
Where $x$ and $y$ are natural numbers and $S(n)=n\cup\{n\}$.
I don't have any problem with how these two rules uniquely define addition of the naturals. Rather, my problem is with how I can take this definition and put it in the form above, the one in which the $+$ operator is defined as a set of $3$-tuples rather than a shorthand for some logical formula.
 A: The definition of addition you cite is an inductive definition: given a relation $R\subseteq\mathbb{N}^3$, it returns a larger relation $R^+$ consisting of:


*

*all triples in $R$,

*all triples of the form $(x, 0, x)$, and

*all triples $(a,  b, c)$ such that for some $u, v$ we have $b=S(u)$, $S(v)=c$, and  $(a, u, v)\in R$.
For any relation $R$, let $LFP(R)$ be the least fixed point of $R$: namely, the intersection of all relations containing $R$ and left unchanged by $^+$. (Exercise: show that this exists.)
The ternary relation corresponding to addition is $LFP(\emptyset)$. Alternately, we can define it as $$\{(x, y, z): (x, y, z)\in LFP(\emptyset)\},$$ or $$\{(x, y, z): \forall R\subseteq\mathbb{N}^3(R^+=R\implies (x, y, z)\in R)\}.$$
Meanwhile, the fact that inductive definitions are not first-order provides an obstacle to any simpler definition; in particular, addition is not first-order definable in the structure $(\mathbb{N}, S)$ (and similarly multiplication isn't definable in the structure $(\mathbb{N}, +)$).
