<p>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 <a href="https://en.wikipedia.org/wiki/Decidability_of_first-order_theories_of_the_real_numbers" rel="noreferrer">(see here)</a>. </p>

<p>If we consider the existential fragment of first-order theory with polynomials the complexity is PSACE instead of doubly exponential <a href="https://en.wikipedia.org/wiki/Existential_theory_of_the_reals" rel="noreferrer">(see here)</a>. </p>

<p>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.</p>

CC BY-SA 3.0
2016-03-23T19:49:45.903Z
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
CC BY-SA 3.0
2016-03-23T20:51:24.967Z
I can't quite see how, but the discussion in https://en.wikipedia.org/wiki/Tarski%27s_exponential_function_problem claims this is equivalent to decidability of the whole theory.
Emil Jeřábek
CC BY-SA 3.0
2016-03-24T09:00:15.237Z
@Steven Stadnicki: Thanks, I added more precise information.
Heinrich Ody
CC BY-SA 3.0
2016-03-24T15:42:50.313Z
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
CC BY-SA 3.0
2016-03-24T15:47:41.870Z
... 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
<decidability>
Decidability of existential first-order theory of reals with exponential
Heinrich Ody
# Decidability of existential first-order theory of reals with exponential

(Asked by: username_0 on 2016-03-23)

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)](https://en.wikipedia.org/wiki/Decidability_of_first-order_theories_of_the_real_numbers).

If we consider the existential fragment of first-order theory with polynomials the complexity is PSACE instead of doubly exponential [(see here)](https://en.wikipedia.org/wiki/Existential_theory_of_the_reals).

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.

**Tags:** decidability
> **Comments:**
> **username_1**: 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.  
> **username_2**: I can't quite see how, but the discussion in https://en.wikipedia.org/wiki/Tarski%27s_exponential_function_problem claims this is equivalent to decidability of the whole theory.  
> **username_0**: @Steven Stadnicki: Thanks, I added more precise information.  
> **username_2**: 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...  
> **username_2**: ... 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).  

---

## 0 answers

