Editing Computable function (section)

== Provability ==

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 logic|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 function]]s. Another example is the [[Ackermann function]], which is recursively defined but not primitive recursive.<ref>{{cite journal 
 |last= Péter 
 |first= Rózsa
 |author-link= Rózsa Péter
 |journal= [[Mathematische Annalen]] 
 |title= Konstruktion nichtrekursiver Funktionen 
 |year= 1935 
 |volume= 111
 |pages= 42–60 
 |doi= 10.1007/BF01472200
 |s2cid= 121107217 
}}</ref>

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 <math>A</math>, whenever the definition of <math>A(x,y)</math> refers to <math>A(p,q)</math>, then <math>(p,q) < (x,y)</math> w.r.t. the [[lexicographic order]] on pairs of [[natural number]]s. 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 [[soundness|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'' calls ''f''<sub>''n''</sub>(''n'') (where ''f''<sub>''n''</sub> 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.