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 0 , 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 : ℵ1 → ℵ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 ∂T. We will give a new construction of the derivative, which shows that the existence and fundamental properties of ∂T can already be established in the theory RCA0. The latter does not prove, however, that ∂T preserves well-foundedness. Our main result shows that the statement “for every normal dilator T, its derivative ∂T preserves wellfoundedness” is ACA0-provably equivalent to Π1 1 -bar induction (and hence to Σ1 1 -dependent choice and to Π1 2 -reflection for ω-models)