set-theoretic function definition; recursion theorem I am an undergraduate student, currently studying axiomatic set theory (I am reading Halmos' Naive Set Theory as an overview, and consulting other sources recommended to me to supplement the sparser parts of the exposition; I am familiar with all of the material in his book up to this point, but not much more). 
After proving the Peano "axioms" in ZF, Halmos states the Recursion Theorem (given $f: X \rightarrow X$, $a \in X$, \begin{equation} \exists u: \omega \rightarrow X (u(0) = a \land u(n^+) = f(u(n))) 
\end{equation}
and this $u$ is unique).
Halmos' proof sketch raised some questions for me (I am aware that some ground has been broken with these here $\rightarrow$ Need help with Recursion Theorem (Set Theory) , Explaining why a function is well-defined ): 


*

*It was mentioned in the above articles that recursively defining a factorial function, or the Fibonacci numbers, or other truly recursive functions, requires a more general theorem; could someone sketch a proof of that?

*Halmos' argument about discarded elements does not convince me (I object to the induction step, which is vague); can this argument be improved?

*Since I have only seen the existence of numbers and the empty set postulated so far: will ZFC at some point gain the ability to discuss collections of objects which are not numbers? 

 A: This is an attempt to answer your first question.
First of all, I strongly recommend the book Introduction to Set Theory by Karel Hrbacek and Thomas Jech. It contains a lucid exposition of elementary axiomatic set theory. In particular, in the section 3 of the chapter 3 various versions of the recursion theorem and some applications of them are presented. One of these versions is the following

Theorem (3.5 in the 2nd edition): For any set $S$ and any function $g:\operatorname{Seq}(S)\to S$ there exists a unique sequence $f:\omega\to S$ such that
  $$
f_n=g(f\restriction n)\quad\text{for all $n\in\omega$}.
$$
  ($\operatorname{Seq}(S)$ is the set of all finite sequences of the elements of $S$).

Now if we let
$$
g:\operatorname{Seq}(\omega)\to\omega,\ g(t)=
\begin{cases}
1 & \text{if the length of $t$ if $0$ or $1$;} \\
t_{n-1}+t_{n-2} & \text{if the length of $t$ (denote by $n$) is greater than $1$,}
\end{cases}
$$
then the aforementioned theorem gives a sequence $f:\omega\to\omega$ such that $f_n=g(f\restriction n)$. This is exactly the Fibonacci sequence:
$$
\begin{align*}
&f_0=g(f\restriction 0)=g(\emptyset)=1 \\
&f_1=g(f\restriction 1)=g(\langle f_0\rangle)=1 \\
&f_2=g(f\restriction 2)=g(\langle f_0,f_1\rangle)=f_1+f_0=1+1=2 \\
&f_3=g(f\restriction 3)=g(\langle f_0,f_1,f_2\rangle)=f_2+f_1=2+1=3\quad\text{and so on.}
\end{align*}
$$
Regarding the factorial function, note that once you have defined multiplication (which is done also by recursion) the factorial function can be defined using the Recursion Theorem of Halmos by letting $a=1$ and $f:\omega\to\omega,f(n)=n\cdot n^+$.
A: I'm not sure exactly what Halmos' presentation is since I don't have the book handy, but regarding the third point, ZFC does have the ability to discuss collections of objects which are not numbers. For instance, take the collection E of even numbers. ZFC can prove the set {E, 24} is a set, while only its second element is a number. And this is far more general. In fact, ZFC has the ability to discuss and even prove that there exist sets which are (functionally equivalent) to any mathematical object you can readily think of, be it structures like the natural, reals, complex numbers, or group, topological spaces, even whole models of set theory! 
