Proof Theoretic Analysis by Iterated Reflection

Progressions of iterated reflection principles can be used as a tool for the ordinal analysis of formal systems. Moreover, they provide a uniform definition of a proof-theoretic ordinal for any arithmetical complexity $$\Pi _{n}^{0}$$ . We discuss various notions of proof-theoretic ordinals and compare the information obtained by means of the reflection principles with the results obtained by the more usual proof-theoretic techniques. In some cases we obtain sharper results, e.g., we define proof-theoretic ordinals relevant to logical complexity $$\Pi _{1}^{0}$$ . We provide a more general version of the fine structure relationships for iterated reflection principles (due to Ulf Schmerl). This allows us, in a uniform manner, to analyze main fragments of arithmetic axiomatized by restricted forms of induction, including $$I\Sigma _{n}$$ , $$I\Sigma _{n}^{-}$$ , $$I\Pi _{n}^{-}$$ and their combinations. We also obtain new conservation results relating the hierarchies of uniform and local reflection principles. In particular, we show that (for a sufficiently broad class of theories T) the uniform $$\Sigma _{1}$$ -reflection principle for T is $$\Sigma _{2}$$ -conservative over the corresponding local reflection principle. This bears some corollaries on the hierarchies of restricted induction schemata in arithmetic and provides a key tool for our generalization of Schmerl’s theorem.