Derivatives of normal functions in reverse mathematics

Abstract

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'$, 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:\aleph_1\rightarrow\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 $\partial T$ can already be established in the theory $\mathbf{RCA}_0$. The latter does not prove, however, that $\partial T$ preserves well-foundedness. Our main result shows that the statement ``for every normal dilator $T$, its derivative $\partial T$ preserves well-foundedness'' is $\mathbf{ACA}_0$-provably equivalent to $\Pi^1_1$-bar induction (and hence to $\Sigma^1_1$-dependent choice and to $\Pi^1_2$-reflection for $\omega$-models).