General recursive functions
Julia Robinson · Proceedings of the American Mathematical Society · 1950
robinson 1. Introduction.A primitive recursive function is one which can be obtained from the initial functions /"* (1 ^k^n), 0n («^0), and S, by repeated substitution and recursion.HereS denotes the successor function, and the recursion scheme has the form F(t, 0) = Ah F(i, Sy) = B(h y, F(i, y)),where we have put | = • • • , xn), m = 0.' The class of general recursive functions is obtained if we allow one additional scheme for defining functions, namely Ft = ßy{A(x, y) = 0}, where the symbol on the right denotes the smallest y such that •4(f, y) =0, under the assumption that there is such a y for each r.Kleene showed that this definition of general recursive function is equivalent to Herbrand-Gödel metamathematical definition.2In this paper we shall be concerned with the mathematical (as opposed to metamathematical) aspects of the theory of general recursive functions.Starting from the definition stated, we shall investigate the possible restrictions on the defining schemes.Part of the results obtained are already known from the work of Kleene, but we go further in this direction than Kleene did.No previous knowledge of general recursive functions is assumed in this paper.It will be convenient to have a logical symbolism to express the conditions that appear in applications of the u-rule.We shall use: A (for every), V (there exists), A (and), V (or), ~ (not), -► (ifthen), (if and only if).The following equivalences will be useful: