Defining the sum on the set $\mathbb N$ Suppose we have a set $\mathbb N$, $0\in \mathbb N$ and $\sigma\colon \mathbb N \to \mathbb N$ satisfying Peano axioms of natural numbers. 
Inside ZF (or ZFC if needed) how do we define the "addition" function i.e. a function $+ \colon \mathbb N \times \mathbb N \to \mathbb N$ satisfying for all $n,m \in \mathbb N$
$$
  n + 0 = n\\
  n + \sigma(m) = \sigma(n+m).
$$
I have tried to consider all relations satisfying these properties and taking their intersection $R$. I would like to prove that what I get is a function. I have proved that its domain is $\mathbb N \times \mathbb N$ but I am not able to prove that such relation is univoque. To get the result I would need to prove that $\le$ is a well ordering. But to define $\le$ I would like to have already defined $+$... so I'm not sure which one should be defined first and how to proceed.
A reference to a book would be also appreciated.
 A: What you are trying to prove is a particular case of this:
Theorem: Let $A$ be a set, let $a$ be an element of $A$, and let $\alpha\colon A\longrightarrow A$ be a function. Then there is on and only one function $f\colon\mathbb{N}\longrightarrow A$ such that $f(0)=a$ and that $(\forall n\in\mathbb N):f\bigl(\sigma(n)\bigr)=\alpha\bigl(f(n)\bigr)$.
Your approach to the proof is correct. You define$$\mathcal{A}=\left\{S\subset\mathbb{N}\times A\,\middle|\,\right(0,a)\in S\wedge(\forall n\in\mathbb{N}):(n,b)\in S\implies\bigl(\sigma(n),\alpha(b)\bigr)\in S\}$$and then you define $f$ as the intersection of all elements of $\mathcal A$. Then you prove that $f$ is a function (that is, for each $n\in\mathbb N$, there is one and only one $b\in A$ such that $(n,b)\in f$). It is trivial that $f$ is the only function under the conditions of the theorem.
This theorem is Theorem I in Leon Henkin's On Mathematical Induction (The American Mathematical Monthly
67, No. 4 (Apr., 1960), pp. 323–338).
Proof: The set $\mathcal A$ is not empty, since $\mathbb{N}\times A\in\mathcal A$. Let $f$ be the intersection of all elements of $\mathcal A$. Since $(0,a)$ belongs to each element of $\mathcal A$, then it belongs to $f$ too. On the other hand, whenever $(n,b)\in f$, then $\bigl(\sigma(n),\alpha(b)\bigr)\in f$, because each element of $\mathcal A$ has this property.
Now, I shall prove that, for each $n\in\mathbb N$, there is some $b\in A$ such that $(n,b)\in f$. That's easy to do by induction. If $n=0$, we've already seen that we can take $b=a$. Now, let $n\in\mathbb N$ and suppose that there is a $b\in A$ such that $(n,b)\in f$. Then $(n,b)$ belongs to each element of $\mathcal A$, and therefore so does $\bigl(\sigma(n),\alpha(b)\bigr)$. So $\bigl(\sigma(n),\alpha(b)\bigr)\in f$. This proves what I wanted to prove.
Now, I shall prove that, for each $n\in\mathbb N$ there is only one $b\in A$ such that $(n,b)\in f$. Again, I shall use induction. Suppose that $(0,b)\in f$ for some $b\neq a$. Consider the set $f\setminus\{(0,b)\}$. Then $f\setminus\{(0,b)\}\in\mathcal A$ and therefore, by the definition of $f$, $f\subset\setminus\{(0,b)\}$, which is absurd. So, the only element $b\in A$ such that $(0,b)\in f$ is $b=a$. Now, let $n\in\mathbb N$ and suppose that there is only one $b\in A$ such that $(n,b)\in f$. We already know that $\bigl(\sigma(n),\alpha(b)\bigr)\in f$. Suppose that $\bigl(\sigma(n),b'\bigr)\in f$ for some $b'\neq\alpha(b)$. Then $f\setminus\bigl\{\bigl(\sigma(n),b'\bigr)\bigr\}\in\mathcal A$ and therefore, by the definition of $f$, $f\subset f\setminus\bigl\{\bigl(\sigma(n),b'\bigr)\bigr\}$, which, again, is absurd.
So, I proved that $f$ is a function. This function is also such that


*

*$f(0)=a$;

*$(\forall n\in\mathbb{N}):f\bigl(\sigma(a)\bigr)=\alpha\bigl(f(n)\bigr)$.


Finally, $f$ is the only such function. Indeed, if $g$ is another function with the same properties, then $g\in\mathcal A$ and therefore $f\subset g$. Since both $f$ and $g$ are functions, $g=f$.
A: In this answer $V$ denotes the universe of regular sets.
In general the following statement is true for a class $R$ of ordered pairs.

Let $R$ be well-founded and local and let $t:V\times V\times V\rightarrow V$
  be an operation. 
Exactly one operation $s:V\times V\rightarrow V$
  exists such that $s\left(a,b\right)=t\left(a,b,\left\{ \left(x,s\left(a,x\right)\mid xRb\right)\right\} \right)$
  for all sets $a,b$.

A corollary of this is:
For any two operations $G:\omega\rightarrow V$ and $H:\omega\times\omega\times V\rightarrow V$
there is exactly one function $F:\omega\times\omega\rightarrow V$
satisfying:


*

*$F\left(n,0\right)=G\left(n\right)$

*$F\left(n,\sigma\left(m\right)\right)=H\left(n,m,F\left(n,m\right)\right)$


If $G$ is prescribed by $n\mapsto n$ and $H$ is by $\langle n,m,k\rangle\mapsto\sigma(k)$ then $F$ is the function that you are after.
A: I struggled with the same problem some years ago. Just construct $A$ as a subset of $N^3$ such that:
$\forall a,b,c:[(a,b,c)\in A \iff (a,b,c)\in N^3 $
$\land [\forall d\subset N^3: [\forall e\in N: (e,0,e) \in d $
$\land \forall e,f,g: [(e,f,g)\in d \implies (e,\sigma(f), \sigma(g))\in d]$
$ \implies (a,b,c)\in d]]]$
You should then be able to prove that $A$ is the required function. Not a trivial exercise. 
A similar construction can be used for multiplication and exponentiation on $N$. The strange thing about exponentiation, though, is that any value will work for $0^0$ without affecting the other values. It turns out there are infinitely many binary functions on $N$ that satisfy 
$x^2=x\times x$
$x^3 = x\times x \times x$ 
$x^4 = x\times x \times x\times x$
and so on.
But they differ only in the value of $0^0$.
