8
$\begingroup$

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.

Improve this question
$\endgroup$
5
  • 3
    $\begingroup$ 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. $\endgroup$
    – Steven Stadnicki
    Mar 23, 2016 at 19:49
  • 1
    $\begingroup$ 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. $\endgroup$
    – Emil Jeřábek
    Mar 23, 2016 at 20:51
  • $\begingroup$ @Steven Stadnicki: Thanks, I added more precise information. $\endgroup$
    – Heinrich Ody
    Mar 24, 2016 at 9:00
  • 5
    $\begingroup$ 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... $\endgroup$
    – Emil Jeřábek
    Mar 24, 2016 at 15:42
  • 4
    $\begingroup$ ... 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). $\endgroup$
    – Emil Jeřábek
    Mar 24, 2016 at 15:47

0

Reset to default

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.