BIBLIOPOLIS, EDIZIONI DI FILOSOFIA E SCIENZE
Via Arangio Ruiz 83-80122 Napoli-Italy
Telephone +39-081-664606
Fax +39-081-7616273

STUDIES IN PROOF THEORY 2

INTRODUCTION

The definition of a set of natural numbers is called impredicative if it refers to the completed totality of all sets of natural numbers. The least upper bound principle of classical analysis provides an important example of the necessary use of such an impredicative definition. So the full theory of real members (analysis) cannot be obtained by strict predicativeness. But for subsystems of analysis a predicative interpretation can be given. This was first done by S. FEFERMAN after he and  K SCHÜTTE independently from each other had determined the limiting ordinal Γ0 of predicativity.
The first constructive consistency proof for an essentially impredicative  subsystem of analysis  was given by G. TAKEUTI. In proof-theoretical investigations of such impredicative systems are carried out following the work of Takeuti. After the publication of essential progress in the proof-theoretical investigations of relatively strong subsystems of analysis was achieved mainly by W. BUCHHOLZ, S.FEFERMAN, H. FRIEDMAN , J.Y. GIRARD, G. JÄGER, W. POHLERS, W. SIEG  and W.W. TAIT. There the methods of Takeuti were successful1y replaced by more perspicuous techniques which also made it possible to determine the precise proof-theoretical ordinals of the systems considered.
The present book provides a uniform proof-theoretical treatment of several essentially impredicative subsystems of analysis, beginning with simple analysis and ending with the system (Δ12CA) + (BR) of Δ12comprehension and bar-rule. For the proof-theoretical analysis of these systems a certain constructive system of ordinal notations suffices which we call T (Ω).
But for the proof-theoretical treatment of stronger subsystems of analysis or set theory, as carried out by G. JÄGER and W. POHLERS, a much stronger subsystem of ordinal notations is needed. In this book we do not present these stronger proof-theoretical studies but only give a reference to them.
In chapter I the ordinal notation system T (Ω) is developed.
In chapters II and III upper bounds for the provable ordinals of the various impredicative subsystems of anaIysis are estabIished. Chapter IV contains formalized well ordering proofs for certain segments of T (Ω) which are used to show that the upper bounds of chapters II and III are best possibie and thus are in fact the proot-theoreticai ordinals of the respective formaI systems.