Arnold Beckmann and Wolfram Pohlers
Annals of Pure and Applied Logic, Volume 94, Pages 7-19
Publication year: 1998

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.