?
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 Π0nΠn0. 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 Π01Π10. 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ΣnIΣn, IΣ−nIΣn−, IΠ−nIΠ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 Σ1Σ1-reflection principle for T is Σ2Σ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.