A note on ordinal exponentiation and derivatives of normal functions

Michael Rathjen and the present author have shown that ${\mathrm{\Pi }}_1^1$-bar induction is equivalent to (a suitable formalization of) the statement that every normal function has a derivative, provably in $\mathbf{A}\mathbf{C}{\mathbf{A}}_{\mathbf{0}}$. In this note we show that the base theory can be weakened to $\mathbf{R}\mathbf{C}{\mathbf{A}}_{\mathbf{0}}$. Our argument makes crucial use of a normal function $f$ with $f(\alpha)\leq 1+\alpha^2$and$f’(\alpha)=\omega^{\omega^\alpha}$. We will also exhibit a normal function $g$ with $g(\alpha )\le 1+\alpha \cdot 2$ and $g^{\mathrm{\prime }}(\alpha )={\omega }^{1+\alpha }$.