Transfinite Induction Principles and Iterated Reflection Principles
Summary
Two of the methods used to assign proof-theoretic ordinals to theories are using transfinite induction principles, inspired by Gentzen's consistency proof for $\mathsf{PA}$ via $\varepsilon_0$-induction, and approximating them by transfinite iterations of reflection principles, an approach first proposed by Turing and developed further by Feferman, Schmerl and Beklemishev. A number of well-known results by Feferman, Kreisel and Lévy, Schmerl, Sommer and Beklemishev relate transfinite induction to reflection. In this paper we study the relationships between partial transfinite induction principles obtained by restricting it to a class $\Sigma_n$ or $\Pi_n$ in the arithmetical hierarchy and iterated reflection principles. Our goal is to obtain a complete characterisation of transfinite induction principles in terms of reflection principles, closing the last remaining gap in the overall picture.
We first introduce our base theory of choice, the arithmetic $\mathsf{EA}$ of Kalmár elementary functions, and outline various details about its arithmetisation and conducting ordinal arithmetic (up to $\varepsilon_0$) within it. We then introduce partial transfinite induction and reflection principles and present some key facts established by Sommer, Schmerl and Beklemishev. Finally we state and prove our main result: the transfinite induction schema for $\Pi_n$ formulae up to the ordinal $\omega^{\omega^\alpha}$ is equivalent to $\alpha+1$ times iterated uniform reflection principle for $\Pi_{n+2}$ formulae over $\mathsf{EA}$.