< Back to previous page

Project

Reflection Spectra: Predicative Mathematics and Beyond

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.

Date:1 Apr 2020 →  31 Dec 2023
Keywords:Reflection principles, Provability logic, Ordinal analysis
Disciplines:Mathematical logic and foundations