# Decidability of existential first-order theory of reals with exponential

The first-order theory over the reals as an ordered field with polynomials is decidable with doubly exponential complexity. However, if we additionally allow the exponential function, that is $e^x$ decidability is unknown (see here).

If we consider the existential fragment of first-order theory with polynomials the complexity is PSACE instead of doubly exponential (see here).

I am interested in results concerning decidability of existential first-order theory with polynomials extended with the function $a^x$, where $a$ is a rational number. I consider this not standard exponential function because of the application I have for this logic.

• For clarification purposes: when you say 'the exponential function', do you mean the univariate $f(x)\equiv e^x$, or the bivariate $f(x,y)\equiv x^y$? I'm presuming the former from context (and also presuming that this is all over the reals as an ordered field, likewise from context) but it would be good to be clearer. Mar 23, 2016 at 19:49
• I can't quite see how, but the discussion in en.wikipedia.org/wiki/Tarski%27s_exponential_function_problem claims this is equivalent to decidability of the whole theory. Mar 23, 2016 at 20:51
• @Steven Stadnicki: Thanks, I added more precise information. Mar 24, 2016 at 9:00
• Thanks for the clarification. Wikipedia is correct: I finally got hold of Macintyre & Wilkie, On the decidability of the real exponential field; they prove (unconditionally) that the real field with “restricted exponentiation” $(\mathbb R,\exp((1+x^2)^{-1}))$ is effectively model complete, and while they cannot quite prove that for $(\mathbb R,\exp)$, they still obtain the result that the theory of $(\mathbb R,\exp)$ is axiomatized over its existential theory by an explicit recursive set of axioms. Thus, If the existential theory is decidable, then the full first-order theory is decidable... Mar 24, 2016 at 15:42
• ... This is all for natural exponentiation $\exp(x)=e^x$. I don’t know whether it also applies to exponentiation with rational basis. It is easy to see that binary exponentiation $x^y$ is existentially definable from $a^x$ for any constant $a>0$, hence the existential theories of $(\mathbb R,a^x)$ for rational $a$ are all reducible to each other, and also reducible to $(\mathbb R,\exp)$. Conversely, $e$, hence $\exp(x)$, is also definable from any $a^x$, but I don’t see how to make the definition existential (it can be made universal). Mar 24, 2016 at 15:47