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