Given a function (or, similarly, a set), one may be interested not only if it is computable, but also whether this can be
proven in a particular proof system (usually
first-order Peano arithmetic). A function that can be proven to be computable is called
provably total. The set of provably total functions is
recursively enumerable: one can enumerate all the provably total functions by enumerating all their corresponding proofs, that prove their computability. This can be done by enumerating all the proofs of the proof system and ignoring irrelevant ones.
Relation to recursively defined functions In a function defined by a
recursive definition, each value is defined by a fixed first-order formula of other, previously defined values of the same function or other functions, which might be simply constants. A subset of these is the
primitive recursive functions. Another example is the
Ackermann function, which is recursively defined but not primitive recursive. For definitions of this type to avoid circularity or infinite regress, it is necessary that recursive calls to the same function within a definition be to arguments that are smaller in some
well-partial-order on the function's domain. For instance, for the Ackermann function A, whenever the definition of A(x,y) refers to A(p,q), then (p,q) with respect to the
lexicographic order on pairs of
natural numbers. In this case, and in the case of the primitive recursive functions, well-ordering is obvious, but some "refers-to" relations are nontrivial to prove as being well-orderings. Any function defined recursively in a well-ordered way is computable: each value can be computed by expanding a tree of recursive calls to the function, and this expansion must terminate after a finite number of calls, because otherwise
Kőnig's lemma would lead to an infinite descending sequence of calls, violating the assumption of well-ordering.
Total functions that are not provably total In a
sound proof system, every provably total function is indeed total, but the converse is not true: in every first-order proof system that is strong enough and sound (including Peano arithmetic), one can prove (in another proof system) the existence of total functions that cannot be proven total in the proof system. If the total computable functions are enumerated via the Turing machines that produces them, then the above statement can be shown, if the proof system is sound, by a similar diagonalization argument to that used above, using the enumeration of provably total functions given earlier. One uses a Turing machine that enumerates the relevant proofs, and for every input
n outputs
fn(
n) + 1 (where
fn is
n-th function by
this enumeration) by invoking the Turing machine that computes it according to the
n-th proof. Such a Turing machine is guaranteed to halt if the proof system is sound, but the total function it computes cannot be any of the functions proven total by the proof system, otherwise there would be some
n for which
fn(
n) + 1 =
fn(
n). == Uncomputable functions and unsolvable problems ==