# What is the simplest known arithmetic definition of exponentiation?

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.)

• Juat to clarify, the quantifiers are on variables over natural numbers, and the quantifier-free formula can contain equality, addition and multiplication of natural numbers, right? Dec 17, 2012 at 11:58
• Yes, that is right. Dec 17, 2012 at 13:52
• It would be reasonable to replace (3) with: $E_n$ proves that if $\phi(x_1,y_1)$ and $\phi(x_2,y_2)$, then $\phi(x_1+x_2,y_1y_2)$. This the key property of exponentation, and monotonicity follows from this as a corollary.
– user44143
Mar 6, 2019 at 17:27