F. Provably Computable Functions

One aim of proof theory is to find uniform scales against which one can measure the computational complexity of functions verifiably computable in “known” theories. Given a theory T, one is often interested in its provably computable functions, also know as its provably recursive functions.

One of the oldest results of this sort is due to many people (at least Mints, Parsons, Takeuti).

A not too difficult proof is obtained via partial cut elimination followed by “reading-off” primitive recursive bounds for existential quantifiers in such proofs.^[59]

For full PA there is Kreisel’s classification of the provably computable functions as the $<{\epsilon }_0$ recursive functions in Kreisel 1952. Here an ordinal representation system provides the uniform scale. Such a characterization can actually be extracted from the ordinal analysis of any theory. Indeed, it is a general fact that an ordinal analysis of a theory T yields, as a by-product, a characterization of the provably computable functions of T. An ordinal analysis of T via an ordinal representation system $⟨A,⊲,\dots ⟩$ provides a reduction (also ensuring at least ${\mathrm{\Pi }}_2^0$-conservativity) of T to

where $\bigcup _{\alpha \in A}\text{TI}({⊲}_{\overline{\alpha }})$ denotes the schema of transfinite induction for all initial segments ${⊲}_{\overline{\alpha }}$ of the well-ordering $⊲$ (indexed externally). On the strength of the latter, it suffices to characterize the provably computable functions of theories of type $(\text{f1})$.

The proof of Theorem F.4 poses, however, fascinating technical problems since the cut elimination usually takes place in infinitary calculi. A cut-free proof of a ${\mathrm{\Sigma }}_1^0$ statement can still be infinite and one needs a further “collapse” into the finite to be able to impose a numerical bound on the existential quantifier. One technical tool for achieving this characterization is to embed $\mathbf{\text{PA}}+\bigcup _{\alpha \in A}\text{TI}({⊲}_{\overline{\alpha }})$ into a system of Peano arithmetic with the $\omega$-rule and a repetition rule, Rep, which simply repeats the premise as the conclusion. The addition of the Rep rule enables one to carry out a continuous cut elimination, due to Mints (1978), which is a continuous operation in the usual tree topology on proof trees. A further pivotal step consists in making the $\omega$-rule more constructive by assigning codes to proofs, where codes for applications of finitary rules contain codes for the proofs of the premises, and codes for applications of the $\omega$-rule contain Gödel numbers for partial functions enumerating codes of the premises. The aforementioned enumerating functions can be required to be partial recursive, making the proof trees recursive, or even primitive recursive in the presence of the rule Rep which enables one to stretch recursive trees into primitive recursive ones. A variant of the characterization of Theorem F.4^[60] is given in Friedman & Sheard 1995, where the provably computable functions of $\mathbf{\text{PA}}+\bigcup _{\alpha \in A}\text{TI}({⊲}_{\overline{\alpha }})$ are classified as the descent recursive functions over A. However, there is a more recent approach which has the great advantage over the previous one that one need not bother with codes for infinite derivations. In this approach one adds an extra feature to infinite derivations by which one can exert a greater control on derivations so as to be able to directly read off numerical bounds from cut free proofs of ${\mathrm{\Sigma }}_1^0$ statements. This has been carried out in Buchholz & Wainer 1987 for the special case of PA. In much greater generality and flexibility this approach has been developed by Weiermann (1996).

Ordinal analysis can also be used to extract information about other types of provable functions and higher type functionals, for example, hyperarithmetic functions, set recursive functions and ordinal recursive functions; cf. Rathjen 2006.