How to apply the recursion theorem in practice?
Solution 1:
The Recursion Theorem simply expresses the fact that definitions by recursion are mathematically valid, in other words, that we are indeed able correctly and successfully to define functions by recursion. Mathematicians implicitly use this fact whenever they define a function by recursion.
A more general version of the Recursion Theorem would allow the function $f$ to use the argument $n$ as well as $F(n)$. A still more general version of the Recursion Theorem, called course-of-values recursion, allows $f$ to use as an argument the entire restriction of the function $F\mid n$ to earlier values. (These more complex versions of the Recursion theorem can be derived solely from the single-value theorem you have stated, by using a function $f$ that takes a partial function $F\mid n$ (a finite object) and returns $F\mid (n+1)$ the partial function with one additional value in the domain.)
In the case of the factorial function, we define $0!=1$ and $(n+1)!=(n+1)\cdot n!$. This defines factorial recursively, once mulitplication has been defined. The fact that this does indeed define a function is because of the Recursion Theorem.
If one wants to start a bit earlier, then you may consider how the hierarchy of the primitive recursive functions are built up. Starting with the successor function $s(n)=n+1$, one may define addition by recursion: $a+0=a$, $a+(n+1)=s(a+n)$. Then one gets multiplication: $a\cdot 0=0$, $a\cdot(n+1)=(a\cdot n)+a$. Then exponentiation, factorial, etc. all in the usual way.
Set theorists tend to dwell on the recursion theorem in part because of the version of it that applies to transfinite recursion.
Solution 2:
In the form you have stated, you can't get the factorial function without a little bit of extra work. Nonetheless, it can be done.
Let $X = \mathbb{N} \times \mathbb{N}$ be the set of ordered pairs of natural numbers. Set $f(x, y) = (x + 1, (x + 1) y)$. Set $F(0) = (0, 1)$. Then, by the recursion theorem, there is a function $F : \mathbb{N} \to \mathbb{N} \times \mathbb{N}$ such that $F(n + 1) = f(F(n))$ for every $n$. A standard induction argument shows that $F(n) = (n, n!)$. Let $p_2 : \mathbb{N} \times \mathbb{N} \to \mathbb{N}$ be the projection map $p(x, y) = y$. Then $p_2 \circ F : \mathbb{N} \to \mathbb{N}$ is the factorial function you seek.
Solution 3:
Follow up: With the aid of my DC Proof program, I as able to formally prove that given a set X and element a in X and a function g: N x X --> X, there exists a function f: N --> X such that
f(1)=a
For all k in N, f(k+1) = g(k+1, f(k))
where N is set of natural numbers {1, 2, 3... }
Example: For the factorial function, we have X=N, a=1 and g(x,y) = x*y (multiplication on N).
Factorial(1)=1
For all k in N, Factorial(k+1) = (k+1) * Factorial(k)
I was able to construct f from the sets N and X using only Cartesian product, power set and subset rules.
See HTML version at http://www.dcproof.com/recursive.html (669 lines)