# 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. – Steven Stadnicki Mar 23 '16 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. – Emil Jeřábek Mar 23 '16 at 20:51
• @Steven Stadnicki: Thanks, I added more precise information. – Heinrich Ody Mar 24 '16 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... – Emil Jeřábek Mar 24 '16 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). – Emil Jeřábek Mar 24 '16 at 15:47