Tarski's exponential function problem
In model theory, Tarski's exponential function problem asks whether the theory of the real numbers together with the exponential function is decidable. Tarski had previously shown that the theory of the real numbers (without the exponential function) is decidable.
Contents
1 The problem
2 Conditional and equivalent results
3 Workaround
4 See also
5 References
The problem
The ordered real field R is a structure over the language of ordered rings Lor = (+,·,−,<,0,1), with the usual interpretation given to each symbol. It was proved by Tarski that the theory of the real field, Th(R), is decidable. That is, given any Lor-sentence φ there is an effective procedure for determining whether
- Th(R)⊨φ.{displaystyle operatorname {Th} (mathbb {R} )models varphi .}
He then asked whether this was still the case if one added a unary function exp to the language that was interpreted as the exponential function on R, to get the structure Rexp.
Conditional and equivalent results
The problem can be reduced to finding an effective procedure for determining whether any given exponential polynomial in n variables and with coefficients in Z has a solution in Rn. Macintyre & Wilkie (1995) showed that Schanuel's conjecture implies such a procedure exists, and hence gave a conditional solution to Tarski's problem. Schanuel's conjecture deals with all complex numbers so would be expected to be a stronger result than the decidability of Rexp, and indeed, Macintyre and Wilkie proved that only a real version of Schanuel's conjecture is required to imply the decidability of this theory.
Even the real version of Schanuel's conjecture is not a necessary condition for the decidability of the theory. In their paper, Macintyre and Wilkie showed that an equivalent result to the decidability of Th(Rexp) is what they dubbed the Weak Schanuel's Conjecture. This conjecture states that there is an effective procedure that, given n ≥ 1 and exponential polynomials in n variables with integer coefficients f1,..., fn, g, produces an integer η ≥ 1 that depends on n, f1,..., fn, g, and such that if α ∈ Rn is a non-singular solution of the system
- f1(x1,…,xn,ex1,…,exn)=…=fn(x1,…,xn,ex1,…,exn)=0{displaystyle f_{1}(x_{1},ldots ,x_{n},e^{x_{1}},ldots ,e^{x_{n}})=ldots =f_{n}(x_{1},ldots ,x_{n},e^{x_{1}},ldots ,e^{x_{n}})=0}
then either g(α) = 0 or |g(α)| > η−1.
Workaround
Recently there are attempts at handling the theory of the real numbers with functions such as exp, sin by relaxing decidability to the weaker notion of quasi-decidability. A theory is quasi-decidable if there is a procedure that decides satisfiability but that may run forever for inputs that are not robust in a certain, well-defined sense. Such a procedure exists for systems of n equations in n variables (Franek, Ratschan & Zgliczynski (2011)).
See also
- Decidability of first-order theories of the real numbers
References
Kuhlmann, S. (2001) [1994], "Model theory of the real exponential function", in Hazewinkel, Michiel, Encyclopedia of Mathematics, Springer Science+Business Media B.V. / Kluwer Academic Publishers, ISBN 978-1-55608-010-4.mw-parser-output cite.citation{font-style:inherit}.mw-parser-output q{quotes:"""""""'""'"}.mw-parser-output code.cs1-code{color:inherit;background:inherit;border:inherit;padding:inherit}.mw-parser-output .cs1-lock-free a{background:url("//upload.wikimedia.org/wikipedia/commons/thumb/6/65/Lock-green.svg/9px-Lock-green.svg.png")no-repeat;background-position:right .1em center}.mw-parser-output .cs1-lock-limited a,.mw-parser-output .cs1-lock-registration a{background:url("//upload.wikimedia.org/wikipedia/commons/thumb/d/d6/Lock-gray-alt-2.svg/9px-Lock-gray-alt-2.svg.png")no-repeat;background-position:right .1em center}.mw-parser-output .cs1-lock-subscription a{background:url("//upload.wikimedia.org/wikipedia/commons/thumb/a/aa/Lock-red-alt-2.svg/9px-Lock-red-alt-2.svg.png")no-repeat;background-position:right .1em center}.mw-parser-output .cs1-subscription,.mw-parser-output .cs1-registration{color:#555}.mw-parser-output .cs1-subscription span,.mw-parser-output .cs1-registration span{border-bottom:1px dotted;cursor:help}.mw-parser-output .cs1-hidden-error{display:none;font-size:100%}.mw-parser-output .cs1-visible-error{font-size:100%}.mw-parser-output .cs1-subscription,.mw-parser-output .cs1-registration,.mw-parser-output .cs1-format{font-size:95%}.mw-parser-output .cs1-kern-left,.mw-parser-output .cs1-kern-wl-left{padding-left:0.2em}.mw-parser-output .cs1-kern-right,.mw-parser-output .cs1-kern-wl-right{padding-right:0.2em}
Macintyre, A.J.; Wilkie, A.J. (1995), "On the decidability of the real exponential field", in Odifreddi, P.G., Kreisel 70th Birthday Volume, CLSI
Franek, Peter; Ratschan, Stefan; Zgliczynski, Piotr (2011), "Satisfiability of Systems of Equations of Real Analytic Functions Is Quasi-decidable", Mathematical Foundations of Computer Science 2011, LNCS, 6907, Springer, doi:10.1007/978-3-642-22993-0_30
