Hierarchies of Provably Computable Functions

Abstract

A computable number theoretic function is (total) recursive if some algorithm for it terminates on all inputs. From the algorithm we can unravel a tree of subcomputations such that termination is equivalent to well-foundedness with respect to the ‘computation-branches’. If the tree is well-founded we can prove termination by induction over it. Linearisation of the tree’s ordering then leads to a countable well-ordering whose size and structure reflects the complexity of the function, in terms of the inductive proof needed to verify its termination. We then say that the function is provably recursive -by induction over the given well-ordering. For example, the Ackermann Function is provably recursive, by induction over the lexicographical well-ordering of pairs of numbers; so the order-type of this well-ordering viz. the ordinal ω ², in some sense measures its complexity. We further say that a function is provably recursive in a given formal theory (containing basic arithmetic) if the ∀∃-sentence asserting its totality is a theorem of that theory, or alternatively if it is provably recursive by induction over a provable well-ordering of the theory.