Predicativity Revisited

The ordinal analyses of ID₁ and (Π₂–REF) show that their crucial “impredicative” axioms are ID ¹ ₁ and the reflection scheme. Their presence forced us to develop the collapsing machinery in the ordinal analysis. This, however, is not the complete truth. The impredicative character of these axioms comes only in connection with foundation. This observation is due to Jäger (cf. [48] and [52]). He has shown that theories which are considerably stronger than KPω) become reducible to predicative theories as soon as the foundation scheme is removed or restricted. The methods of predicative proof theory are not in the center of this book. However, we have introduced most of the main notions and techniques needed in Jäger's work. Therefore, we sketch Jäger's approach leaving most of the proofs as exercises. One aim of this chapter is to compute Г₀ as an upper bound for proof-theoretic ordinal of the theories KPi₀ and KPl₀ introduced in Sect. 11.6. Together with Exercise 11.6.5 this also yields Г₀ as upper bound for the proof-theoretic ordinal of the theory (ATR)₀ which in turn with Exercise 8.5.31 implies that Г₀ is the exact proof-theoretic ordinal for all these theories.