Abstract:
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. In my talk I will explain how the notions of normal function and derivative 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.
