# A note on ordinal exponentiation and derivatives of normal functions

## TL;DR

This paper explores the relationship between ordinal exponentiation, derivatives of normal functions, and logical induction principles, showing that certain equivalences hold in weaker base theories like RCA_0.

## Contribution

It demonstrates that the equivalence between normal function derivatives and bar induction can be established in RCA_0, using specific normal functions with particular properties.

## Key findings

- Normal functions with bounds f(α) ≤ 1 + α^2 and g(α) ≤ 1 + α·2 are constructed.
- Derivatives of these functions correspond to specific ordinal exponentiation functions.
- The base theory can be weakened from ACA_0 to RCA_0 for these equivalences.

## Abstract

Michael Rathjen and the present author have shown that $\Pi^1_1$-bar induction is equivalent to (a suitable formalization of) the statement that every normal function has a derivative, provably in $\mathbf{ACA_0}$. In this note we show that the base theory can be weakened to $\mathbf{RCA_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)\leq 1+\alpha\cdot 2$ and $g'(\alpha)=\omega^{1+\alpha}$.