# Derivatives of normal functions in reverse mathematics

## TL;DR

This paper explores the derivative of normal functions on ordinals within reverse mathematics, establishing the logical strength needed for their well-foundedness preservation, linking it to significant subsystems like ACA₀.

## Contribution

It provides a new construction of derivatives of normal dilators and characterizes the logical strength of their well-foundedness preservation in reverse mathematics.

## Key findings

- Existence and properties of derivatives are provable in RCA₀.
- Preservation of well-foundedness by derivatives is equivalent to ACA₀.
- Main result links well-foundedness preservation to Pi¹₁-bar induction.

## 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).