Summary. lnspired by Buchholz’ technique of operator controlled derivations (which were introduced for simplifying Pohlers’ method of local predicativity) a straightforward, perspicuous and conceptually simple method for characterizing the provably recursive functions of Peano arithmetic in terms of Kreisel's ordinal recursive functions is given. Since only amazingly little proof and hierarchy theory is used, the paper is intended to make the field of ordinally informative proof theory accessible even to non-prooftheorists whose knowledge in mathematical logic does not exceed a first graduate level course.

Introduction and Motivation

A fascinating result of ordinally informative proof theory due to Kreisel (1952) is as follows:

Theorem: (*)

The provably recursive functions of Peano arithmetic are exactly the ordinal recursive functions.

Folklore (proof-theoretic) proofs for (*) [cf., for example, Schwichtenberg (1977), Takeuti (1987), Buchholz (1991) or Friedman and Sheard (1995) for such proofs] rely on non trivial metamathematical evaluations of the Gentzenor Schütte-style proof-theoretic analyses of Peano arithmetic. Alternatively a proof- and recursion-theoretic analysis of Gödel's 1958 functional interpretation of Heyting arithmetic can be employed for proving (*), cf. for example [Tait (1965), Buchholz (1980), Weiermann (1995)]. A proof of (*) which does not rely on metamathematical considerations - like primitive recursive stipulations of codes of infinite proof-trees - has been given in [Buchholz (1987), Buchholz and Wainer (1987)]. A proof of (*) using the slow growing hierarchy is given in [Arai (1991)]. A local predicativity style proof - which generalizes uniformly to theories of proof-theoretic strength less than or equal to K PM, cf. [Rathjen (1991)] - of (*) has been given in [Weiermann (1993), Blankertz and Weiermann (1995)]. Other proofs for (*) which are based on model theory can be found, for example, in [Hajek and Pudlak (1993)]. Buchholz (1992) introduced the technique of operator controlled derivations which allows a simplified and conceptually improved exposition of Pohlers’ local predicativity. One aim of the present paper is to give a contribution to the following question (Buchholz, private communication, 1993): Is it possible to use operator controlled derivations to give a proof for (*) - and generalizations of (*) - which is technically smooth?

Erecursion theory extends the notion of computation from hereditarily finite sets to sets of arbitrary rank. Selection theorems, forcing arguments and priority constructions are developed in the setting of E-recursive enumerability.

The notion of a recursive function resulted from an attempt in the 1930's to provide a precise mathematical characterization of the concept of a mechanically or algorithmically calculable function from into. One way to understand this concept is to imagine an idealized digital computer not subject to error or limitations of memory or storage space. Then a partial function F is mechanically calculable just in case there is a finite program (or algorithm) for this computer which directs it to accept inputs of the form m and carry out a computation with two possible results: if m E Dm F, the computation terminates after finitely many steps with the correct value F(m) as output; if m £ Dm F, the computation does not terminate.

As this is an intuitive concept, however, it cannot be described completely except by convention. Not only is any attempt subject to legitimate disagreement on the basis of current knowledge, but also the possibility remains open that in the future a new means of calculation will be discovered which will be agreed by mathematicians to be mechanical but will not fall under the proposed description. Still, from a practical point of view, the notion seems to be a viable one: most people with a thorough understanding of the concepts involved will agree on the question of whether or not a given method of calculation is mechanical.

In particular, although we cannot give a rigorous proof that every recursive function is mechanically calculable, our justification of this assertion in § 2 below should be convincing to almost everyone. The converse proposition, known as Church's Thesis, that all mechanically calculable functions are recursive, is somewhat more problematic. Without a precise ∧delineation of the class of mechanically calculable functions, we are in no position to prove that all of its members are recursive. We are forced, therefore, to rely on what might be called circumstantial evidence. Most importantly, no one has exhibited a function which is agreed to be mechanically calculable but is not recursive. In a similar vein, every known procedure which produces from calculable functions another calculable function also produces a recursive function from recursive functions.