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. In fact, by considering reflection principles of varying logical complexity one can assign a sequence of ordinals to T which we call its reflection spectrum, spec(T). Not much is known about the computation of reflection spectra beyond first-order arithmetic.

The main objective of the project is to develop tools to compute reflection spectra of theories including the Big Five theories of reverse mathematics, and possibly stronger theories. Along the way, we expect to isolate various arithmetical principles and modal logics of independent interest.