• A
  • A
  • A
  • ABC
  • ABC
  • ABC
  • А
  • А
  • А
  • А
  • А
Regular version of the site

Book chapter

Proof-theoretic analysis by iterated reflection

P. 225-270.

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ΣnIΣnIΣnIΠ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.