Transfinite induction principles and iterated reflection principles
Joonas Jürgen Kisel
Tallinn University of Technology
Abstract:
Two of the methods used to assign proof-theoretic ordinals to theories are approximating theories by transfinite induction principles, inspired by Gentzen's consistency proof for PA via \varepsilon_0-induction, and approximating them by transfinite iterations of reflection principles, an approach first proposed by Turing and Feferman and developed further by Schmerl and Beklemishev. We first introduce our base theory of choice, EA, and discuss some details about conducting ordinal arithmetic (up to \varepsilon_0) within it. We then introduce partial transfinite induction and reflection principles and highlight some key facts established by Sommer, Schmerl and Beklemishev. Finally we state, and outline the proof of, a result first conjectured in the correspondence between Beklemishev and Freund, expressing partial transfinite induction principles in terms of iterations of partial uniform reflection principles.