The termination of rewrite systems for parameter recursion, simple nested recursion and unnested multiple recursion is shown by using monotone interpretations both on the ordinals below the first primitive recursively closed ordinal and on the natural numbers. We show that the resulting derivation lengths are primitive recursive. As a corollary we obtain transparent and illuminating proofs of the facts that the schemata of parameter recursion, simple nested recursion and unnested multiple recursion lead from primitive recursive functions to primitive recursive functions.

I survey the syntactic technique of tiering which can be used to restrict the power of a recursion scheme. I show how various results can be obtained entirely proof theoretically without the use of a model of computation.

It is shown how to restrict recursion on notation in all finite types so as to characterize the polynomial-time computable functions. The restrictions are obtained by using a ramified type structure, and by adding linear concepts to the lambda calculus.

A classical quantified modal logic is used to define a "feasible" arithmetic A 1 2 whose provably total functions are exactly the polynomial-time computable functions. Informally, one understands $\Box\alpha$ as "α is feasibly demonstrable". A 1 2 differs from a system A 2 that is as powerful as Peano Arithmetic only by the restriction of induction to ontic (i.e., $\Box$ -free) formulas. Thus, A 1 2 is defined without any reference to bounding terms, and admitting induction over formulas having arbitrarily (...) many alternations of unbounded quantifiers. The system also uses only a very small set of initial functions. To obtain the characterization, one extends the Curry-Howard isomorphism to include modal operations. This leads to a realizability translation based on recent results in higher-type ramified recursion. The fact that induction formulas are not restricted in their logical complexity, allows one to use the Friedman A translation directly. The development also leads us to propose a new Frege rule, the "Modal Extension" rule: if $\vdash \alpha$ then $\vdash A \leftrightarrow \alpha$ a for new symbol A. (shrink)

Let T be Gödel's system of primitive recursive functionals of finite type in a combinatory logic formulation. Let $T^{\star}$ be the subsystem of T in which the iterator and recursor constants are permitted only when immediately applied to type 0 arguments. By a Howard-Schütte-style argument the $T^{\star}$ -derivation lengths are classified in terms of an iterated exponential function. As a consequence a constructive strong normalization proof for $T^{\star}$ is obtained. Another consequence is that every $T^{\star}$ -representable number-theoretic function is elementary (...) recursive. Furthermore, it is shown that, conversely, every elementary recursive function is representable in $T^{\star}$ .The expressive weakness of $T^{\star}$ compared to the full system T can be explained as follows: In contrast to $T$ , computation steps in $T^{\star}$ never increase the nesting-depth of ${\mathcal I}_\rho$ and ${\mathcal R}_\rho$ at recursion positions. (shrink)