The picture is from Enderton's "elements of set theory"(1977) page79.
My question is: How to construct the set "+" by using the axioms in ZF set theory? In the picture above, those one-place functions "Am" are constructed first, but I even have trouble constructing those one-place functions. I have no trouble constructing A1 or A2 or whatever because each of them can be obtained by the recursion theorem on ω(the set of natural numbers, which is defined to be the intersection of all inductive sets),but how can I define all of them? I have $\aleph_0$ such functions to define but it is impossible for me to apply the recursion theorem $\aleph_0$ times.
Or perhaps I can define "+" like this. I have seen this from other sources:
For any natural number m,n:
m+0=m
m+S(n)=S(m+n), S is the successor function on ω.
This definition seems to be able to skip those one-place functions and deal with the binary function directly, but meanwhile another problem arises. This definition would require another form of the recursion theorem as its justification. Such recursion theorem is nowhere to be found and I don't know how to state it and prove it.
You don't apply the recursion theorem infinitely many times. You apply it once.
First you prove that given an arbitrary $m$, the function $A_m$ is uniquely determined. Using generalization, we actually proved that for each $m$ there exists a unique function $A_m$ which has the properties that we want. Now, it is claimed that we can just define $m+n=A_m(n)$.
Of course for this we need to know that the map $m\mapsto A_m$ is also a set, but this holds because the formula used to define $A_m$ is the same formula used to define $A_{m'}$, namely $m$ is just a parameter. To see this, however, you have to delve into the proof of the recursion theorem.
It is, essentially, the same as defining it directly as $m+0=m; m+s(n)=s(m+n)$ and appealing to the recursion theorem. Since here it is clear why the function $m\mapsto A_m$ is a set as well.