By work of Austrian logician Kurt Gödel in the 1930s, no sound and sufficiently strong computably enumerable arithmetic theory can prove its own consistency. Soon after Gödel's work, G. Gentzen provided an almost finitary proof of the consistency of Peano Arithmetic, with only one extraneous component: a use of transfinite induction up to a suitable ordinal number. Ordinal analysis is the branch of proof theory that studies generalizations of Gentzen's theorem whereby one identifies larger ordinal numbers and extracts from them crucial information about a mathematical theory T. Depending on the precise methodology employed, the resulting number associated to a theory T is given a different name; among these are the Pi^1_1-ordinal of T, the Pi^0_2- ordinal of T, or---the focus of this project---the Pi^0_1-ordinal of T. This latter number usually gives somewhat more information about T than its coarser counterparts and generalizes to define the reflection spectrum of a theory, spec(T). Not much is known about the
computation of Pi^0_1 ordinals or reflection spectra beyond firstorder arithmetic. The main objective of the project is to develop tools to compute reflection spectra of predicative theories including ATR_0, and impredicative theories such as ID_1 or Pi^1_1-CA_0; perhaps more, if time permits. Along the way, we expect to isolate various arithmetical principles and modal logics of independent interest.