# 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
{"found_math": true, "script_math_tex": 0, "script_math_asciimath": 0, "math_annotations": 0, "math_alttext": 0, "mathml": 0, "mathjax_tag": 0, "mathjax_inline_tex": 1, "mathjax_display_tex": 0, "mathjax_asciimath": 0, "img_math": 0, "codecogs_latex": 0, "wp_latex": 0, "mimetex.cgi": 0, "/images/math/codecogs": 0, "mathtex.cgi": 0, "katex": 0, "math-container": 0, "wp-katex-eq": 0, "align": 0, "equation": 0, "x-ck12": 0, "texerror": 0, "url": "https://mathoverflow.net/questions/116544/what-is-the-simplest-known-arithmetic-definition-of-exponentiation", "fetch_time": 1701849392000000000, "content_mime_type": "text/html", "warc_filename": "crawl-data/CC-MAIN-2023-50/segments/1700679100583.31/warc/CC-MAIN-20231206063543-20231206093543-00868.warc.gz", "warc_record_offset": 428686347, "warc_record_length": 25663, "token_count": 466, "char_count": 1536, "score": 3.6875, "int_score": 4, "crawl": "CC-MAIN-2023-50", "snapshot_type": "latest", "language": "en", "language_score": 0.8460251092910767, "file_path": "/sailhome/yjruan/project/latent-lm/data/processed/finemath-4plus/finemath-4plus/train-00026-of-00064.parquet"}