For $n$ a natural number, let $E_n$ denote the set of bounded arithmetic formulas consisting of n alternating blocks of bounded quantifiers starting with an existential quantifier, followed by a quantifier-free formula. Let $IE_n$ denote the axiom system of arithmetic with induction restricted to $E_n$-formulas. What is the smallest known $n$ such that there is an $E_n$-formula $\phi(x,y)$ such that:
(1) For $x,y\in\mathbb{N}$, $\phi(x,y)$ iff $2^{x}=y$ (i.e. $\phi$ defines exponentiation on the standard naturals)
(2) $E_n$ proves that for each $x$, there is at most one $y$ such that $\phi(x,y)$
(3) $E_n$ proves that if $x_1\leq x_2$, $\phi(x_1,y_1)$ and $\phi(x_2,y_2)$, then $y_1 \leq y_2$ (i.e. the function given by $\phi$, where defined, is monotonic)
(If we replace $IE_n$ by $I\Delta_0$, then such a formula is known to exist, i.e. exponentiation can be defined by a bounded formula. I'm interested in how simple such a definition can be.)
