# Metamath Proof Explorer

According to Wikipedia ("Primitive recursive function", 19-May-2024, https://en.wikipedia.org/wiki/Primitive_recursive_function): "In computability theory, a primitive recursive function is, roughly speaking, a function that can be computed by a computer program whose loops are all "for" loops (that is, an upper bound of the number of iterations of every loop is fixed before entering the loop). Primitive recursive functions form a strict subset of those general recursive functions that are also total functions."

Furthermore: "A primitive recursive function takes a fixed number of arguments, each a natural number (nonnegative integer: {0, 1, 2, ...}), and returns a natural number. If it takes n arguments it is called n-ary.

The basic primitive recursive functions are given by ... axioms:

1. Constant functions

2. Successor function

3. Projection functions

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

4. Composition operator

5. Primitive recursion operator

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