Provably Recursive Functions of NT

Kreisel once asked the question if it is possible to obtain upper bounds for the proof-theoretic ordinal of a theory whose language does not include free predicate variables without using Gödel's second incompleteness theorem. In Sect. 9.3 we proved in Theorem 9.3.2 that cut elimination is close to trivial for semi-formal systems which derive only sentences. Subsequently we discussed that no ordinal information can be expected from cut-elimination in such semi-formal systems. The proof of Theorem 9.3.2 fails, however, in the presence of set variables. For the standard procedure in getting an ordinal analysis of NT it is therefore crucial to include free set variables in its language. This is probably the background of Kreisel's question. On the other side, we have seen in Chap. 9 that controlling operators may allow us to obtain information also from semi-formal systems without free set variables in their languages. Weiermann observed that this is also true for “predicative” semi-formal systems. He could prove that the methods of impredicative proof theory are also applicable in predicative proof theory and lead there to better results. In particular he succeeded in (re)characterizing the provably recursive functions of NT (cf. [106] and [10]). In the following sections we present a variant of one of Weiermann's approaches.