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

  • $\begingroup$ 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? $\endgroup$ Dec 17, 2012 at 11:58
  • $\begingroup$ Yes, that is right. $\endgroup$
    – M Carl
    Dec 17, 2012 at 13:52
  • $\begingroup$ 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. $\endgroup$
    – user44143
    Mar 6, 2019 at 17:27


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Browse other questions tagged or ask your own question.