In untyped lambda calculus, the fix-point operator $\mathcal{Y}$ can be used "to create" recursion. This is ok to me. But when we think about fix-points in the context of recursive functions, although we have a similar theorem that presents fix-points, this fix-points operates only on indices of recursion functions. The theorem says that, given a total function $f$, there is a fix point $n$ such that $\phi_n = \phi_{f(n)}$. In Odifreedi book, Classical Recursion Theory, page 157, it says we can take only this components to define all the partial recursive functions:
I didn't get what are this fixed-point definitions. How we can understand this? It seems to me if we take only the fix-point theorem as a way to define other functions, we would get stuck in the indices. For example, if $f$ is the function $f(x) = xf(x-1)$, if $x \not = 0$, and $f(x) = 1$, if $x= 0$, we would get:
$$\phi_n \simeq \phi_{f(n)} \simeq \phi_{f\circ f(n)} \simeq ... \simeq \phi_{n!}$$
But it seems to me we would have to use the S-m-n theorem to get the $n!$ out of the indices. In wikipedia (link here) it says we have to use the second recursion theorem to get this (and the second recursion theorem needs the S-m-n plus fix-point theorems). The second theorem says that, for every partial recursive functions $\psi$, there is a index $e$ such that:
$$\phi_e(x) \simeq \psi(e,x).$$ This theorem uses the S-m-n theorem in the proof. And it seems it can be used to get a function $\psi$ out of the index. But I didn't understand the proof used in wikipedia to show that we can eliminate primitive recursion in this context.
So my questions are:
- How this proof works?
- What are "fixed-point definitions"? Can we assume it is only the fix-point theorem? Or we need something like the S-m-n theorem also (or the second recursion theorem)?