Primitive recursive function

More complex primitive recursive functions can be obtained by applying the operations given by these axioms:

The primitive recursive functions are the basic functions and those obtained from the basic functions by applying these operations a finite number of times.

The following examples and definitions are from Kleene (1952) pp. 223–231 — many appear with proofs. Most also appear with similar names, either as proofs or as examples, in Boolos-Burgess-Jeffrey 2002 pp. 63–70; they add the logarithm lo(x, y) or lg(x, y) depending on the exact derivation.

In the following we observe that primitive recursive functions can be of four types:

The generalization to any k-ary primitive recursion function is trivial.

However, the set of primitive recursive functions is not the largest recursively enumerable subset of the set of all total recursive functions. For example, the set of provably total functions (in Peano arithmetic) is also recursively enumerable, as one can enumerate all the proofs of the theory. While all primitive recursive functions are provably total, the converse is not true.

Primitive recursive functions tend to correspond very closely with our intuition of what a computable function must be. Certainly the initial functions are intuitively computable (in their very simplicity), and the two operations by which one can create new primitive recursive functions are also very straightforward. However, the set of primitive recursive functions does not include every possible total computable function—this can be seen with a variant of Cantor's diagonal argument. This argument provides a total computable function that is not primitive recursive. A sketch of the proof is as follows:

Other examples of total recursive but not primitive recursive functions are known:

They proved that the predecessor function still could be defined, and hence that "weak" primitive recursion also defines the primitive recursive functions.

Similarly, many of the syntactic results in proof theory can be proved in PRA, which implies that there are primitive recursive functions that carry out the corresponding syntactic transformations of proofs.