A note on ordinal exponentiation and derivatives of normal functions
Anton Freund · Mathematical logic quarterly · 2020
Abstract Michael Rathjen and the present author have shown that ‐bar induction is equivalent to (a suitable formalization of) the statement that every normal function has a derivative, provably in . In this note we show that the base theory can be weakened to . Our argument makes crucial use of a normal function f with and . We shall also exhibit a normal function g with and .