How strong are derivatives of normal functions?

Anton Freund, Technische Universität Darmstadt. Part of the Logic Seminar Series

A normal function is a strictly increasing function from ordinals to ordinals that is continuous at limit stages.  The fixed points of any normal function constitute the range of another normal function, called its derivative.  Building on work of Aczel and Girard, I will explain how normal functions and their derivatives can be formalized in second order arithmetic.  Under this formalization, the statement that every normal function has a derivative is shown to be equivalent to transfinite (bar) induction for Pi^1_1-formulas.  The talk is based on joint work with Michael Rathjen.  Full details can be found in arXiv:1904.04630.