General recursive function

A partial recursive function that is defined for all values of its arguments. The concept of a general recursive function can also be defined independently of the concept of a partial recursive function as follows. The class of all general recursive functions is the smallest class of functions containing all primitive recursive functions and closed under composition of functions and the least-number operator $\mu$, under the condition that $\mu$ is only applied to a function $g(x_1,\ldots,x_n,y)$ when $$ \forall x_1,\ldots,x_n \exists y\,.\, g(x_1,\ldots,x_n,y) = 0 \ . $$

However, the study of general recursive functions is usually carried out within the class of all partial recursive functions. This is related, in particular, to the fact that there is no number $n>0$ for which there exists a general recursive function that is universal for the class of all $n$-place general recursive functions.

All general recursive functions are explicitly definable in formal arithmetic in the sense that for any such function $f(x_1,\ldots,x_n)$ an arithmetical formula $F(x_1,\ldots,x_n,y)$ can be constructed with the following property: For any natural numbers $k_1,\ldots,k_n,k$, if $f(k_1,\ldots,k_n) = k$, then $\vdash F(\bar k_1,\ldots,\bar k_n,\bar k)$ ; but if $f(k_1,\ldots,k_n) \ne k$, then $\vdash \neg F(\bar k_1,\ldots,\bar k_n,\bar k)$, where $\bar k_1,\ldots,\bar k_n,\bar k$ are the terms representing the numbers $k_1,\ldots,k_n,k$, and the symbol $\vdash$ denotes derivability in the arithmetic calculus.

References

[1]	P.S. Novikov, "Elements of mathematical logic" , Oliver & Boyd and Addison-Wesley (1964) (Translated from Russian)
[2]	E. Mendelson, "Introduction to mathematical logic" , v. Nostrand (1964)

References

[a1]	S.C. Kleene, "Introduction to metamathematics" , North-Holland (1951)
[a2]	H. Rogers jr., "Theory of recursive functions and effective computability" , McGraw-Hill (1967) pp. 164–165