FINITE NOTATIONS FOR INFINITE TERMS

Buchholz (1991) presented a method to build notation systems for infin ite sequent-style derivations, analogous to well-known systems of nota tion for ordinals. The essential feature is that from a notation one c an read off by a primitive (not epsilon(0)-) recursive function its nt h predecessor and, e.g. the last rule applied. Here we extend the meth od to the more general setting of infinite (typed) terms, in order to make it applicable in other proof-theoretic contexts as well as in rec ursion theory. As examples, we use the method to (1) give a new proof of a well-known trade-off theorem (Schwichtenberg, 1975), which says t hat detours through higher types can be eliminated by the use of trans finite recursion along higher ordinals, and (2) construct a continuous normalization operator with an explicit modulus of continuity. (C) 19 98 Elsevier Science B.V. All rights reserved.