Tarski's exponential function problem

In mathematics, Tarski's exponential function problem, of mathematician and logician Alfred Tarski, asks whether the usual 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.

The problem

The ordered real field R is a structure over the language of ordered rings L_or = (+,·,−,<,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. The motivation for this problem comes from the study of Latin Squares. Call a collection of cells from a matrix a transversal if there is exactly one cell from each row and one from each column, and say that a transversal is latin if no two of its cells contain the same element. The multiplication table of every (finite multiplicative) group is a latin square, and we see that has a latin transversal if and only if it has a complete map (the cells indexed by form the transversal). If we do have such a latin transversal, then for every , the map given by is also a latin transversal, and the collection gives us pairwise disjoint latin transversals in the multiplication table of . This is precisely equivalent to the existence of a latin square orthogonal to this multiplication table.That is, given any L_or-sentence φ there is an effective procedure for determining whether

$\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 R_exp.

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 Rⁿ. 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 R_exp, 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(R_exp) 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 f₁,..., f_n, g, produces an integer η ≥ 1 that depends on n, f₁,..., f_n, g, and such that if α ∈ Rⁿ is a non-singular solution of the system

$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(α)| > η⁻¹.

References

• Kuhlmann, S. (2001) [1994], "Model theory of the real exponential function", Encyclopedia of Mathematics, EMS Press
• Macintyre, A.J.; Wilkie, A.J. (1995), "On the decidability of the real exponential field", in Odifreddi, P.G. (ed.), Kreisel 70th Birthday Volume, CLSI