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.