Derivatives of normal functions in reverse mathematics

Consider a normal function $f$ on the ordinals (i. e. a function $f$ that is strictly increasing and continuous at limit stages). By enumerating the fixed points of $f$ we obtain a faster normal function $f^{\mathrm{\prime }}$, called the derivative of $f$. The present paper investigates this important construction from the viewpoint of reverse mathematics. Within this framework we must restrict our attention to normal functions $f:{\mathrm{\aleph }}_1\to {\mathrm{\aleph }}_1$ that are represented by dilators (i. e. particularly uniform endofunctors on the category of well-orders, as introduced by J.-Y. Girard). Due to a categorical construction of P. Aczel, each normal dilator $T$ has a derivative $\partial T$. We will give a new construction of the derivative, which shows that the existence and fundamental properties of $\mathrm{\partial }T$ can already be established in the theory ${\mathbf{R}\mathbf{C}\mathbf{A}}_0$. The latter does not prove, however, that $\mathrm{\partial }T$ preserves well-foundedness. Our main result shows that the statement ``for every normal dilator $T$, its derivative $\mathrm{\partial }T$ preserves well-foundedness’’ is ${\mathbf{A}\mathbf{C}\mathbf{A}}_0$-provably equivalent to ${\mathrm{\Pi }}_1^1$-bar induction (and hence to ${\mathrm{\Sigma }}_1^1$-dependent choice and to ${\mathrm{\Pi }}_2^1$-reflection for $\omega$-models).