We define a coding of natural numbers — which we will call the exponential notations — and interpretations of the less-than-relation, the successor function, addition and exponentiation on the exponential notations. We prove that all these interpretations are polynomial time computable. As an application we show that we can interpret terms over a certain restricted language — including exponentiation — in polynomial time on exponential notations.

We show that there is a primitive recursive tree which is not well-founded, but which is well-founded for co-r.e. sets, provable in Σ_1-Ind. It follows that the supremum of order-types of primitive recursive well-orderings, whose well-foundedness on co-r.e. sets is provable in Σ_1-Ind, equals the limit of all recursive ordinals.

We determine the exact bounds for the length of an arbitrary reduction sequence of a term in the typed λ – calculus with β -, ξ – and η – conversion. There will be two essentially different classifications, one depending on the height and the degree of the term and the other depending on the length and the degree of the term.

We use a modified Howard-Schütte-function [ ]_0 which assigns finite ordinals to each term from Tpred and which witnesses the strong normalization for T^pred . Furthermore the derivation lengths function for T^pred is elementary recursive, hence representable functions in T^pred are computable in elementary time, hence are elementary recursive. On the other hand it is shown that random-access machine transitions can be simulated in simple typed combinatorial calculus with combinators for the case distinction function and for the predecessor function, hence T^pred represents any elementary recursive function.

Inspired from Buchholz’ ordinal analysis of ID_1 and Beckmann’s analysis of the simple typed λ – calculus we classify the derivation lengths for Gödel’s system T in the λ – formulation (where the η – rule is included).

In this paper we introduce an infinitary proof system for a language of second order arithmetic which is complete for Pi^1_1 – sentences. The main observation there is the Boundedness Theorem telling that the order-type of a Sigma^1_1 – definable well-ordering < is less than or equal to the truth complexity of TI(<) . The commonly known Boundedness Principle of Generalized Recursion Theory will be obtained as a consequence of our proof theoretical Boundedness Theorem which in turn is a consequence of cut-freeness. This yields a proof of the Boundedness Principle which does not use the Analytical Hierarchy Theorem.

A natural term rewriting framework for the Bellantoni Cook schemata of predicative recursion, which yields a canonical definition of the polynomial time computable functions, is introduced. In terms of an exponential function both, an upper bound and a lower bound are proved for the resulting derivation lengths of the functions in question. It is proved that any natural reduction strategy yields an algorithm which runs in exponential time. We give an example in which this estimate is tight. It is proved that the resulting derivation lengths become polynomially bounded in the lengths of the inputs if the rewrite rules are only applied to terms in which the safe arguments – no restrictions are assumed for the normal arguments – consist of values, i.e. numerals, and not of names, i.e. non numeral terms. It is proved that in the latter situation any inside first reduction strategy and any head reduction strategy yield algorithms, for the function under consideration, for which the running time is bounded by an appropriate polynomial in the lengths of the input. A feasible rewrite system for predicative recursion with predicative parameter substitution is defined. It is proved that the derivation lengths of this rewrite system are polynomially bounded in the lengths of the inputs. As a corollary we reobtain Bellantoni´s result stating that predicative recursion is closed under predicative parameter recursion.