Derivatives of normal functions in reverse mathematics (Q2216034)

It is well known that continuous, strictly increasing -- or ``normal'' -- class functions on ordinals are in direct correspondence with closed and unbounded (club) classes of ordinals. The fixed point set of such a function is a club, and thus it is described by another such function, called the \textit{derivative} of the original one. In this paper, this normal function property of having a derivative is studied reverse-mathematically. To do that, normal functions are restricted first to (ordinary set-theoretic) functions defined on \(\aleph_1\) (making use of its regularity) and then to those which are describable by dilators (for which the derivative may be described in a more elegant way). Thus, in this restricted sense, the property is shown to be equivalent over \(\textbf{ACA}_0\) (this was later weakened to \(\textbf{RCA}_0\) in a separate paper of Anton Freund, the first author of this paper) to the principle of \(\Pi^1_1\)-bar induction (also called transfinite induction).