A note on ordinal exponentiation and derivatives of normal functions

Michael Rathjen and the present author have shown that Π11‐bar induction is equivalent to (a suitable formalization of) the statement that every normal function has a derivative, provably in ACA0. In this note we show that the base theory can be weakened to RCA0. Our argument makes crucial use of a normal function f with f(α)≤1+α² and f′(α)=ωωα. We shall also exhibit a normal function g with g(α)≤1+α·2 and g′(α)=ω1+α.