Wilkie's theorem

In mathematics, Wilkie's theorem is a result by Alex Wilkie about the theory of ordered fields with an exponential function, or equivalently about the geometric nature of exponential varieties.

In terms of model theory, Wilkie's theorem deals with the language L_exp = (+,−,·,<,0,1,e^x), the language of ordered rings with an exponential function e^x. Suppose φ(x₁,...,x_m) is a formula in this language, then Wilkie's theorem states that there is an integer n ≥ m and polynomials f₁,...,f_r ∈ Z[x₁,...,x_n,e^x₁,...,e^x_n] such that φ(x₁,...,x_m) is equivalent to the existential formula

Thus, while this theory does not have full quantifier elimination, formulae can be put in a particularly simple form. This result proves that the theory of the structure R_exp, that is the real ordered field with the exponential function, is model complete.

In terms of analytic geometry, the theorem states that any definable set in the above language — in particular the complement of an exponential variety — is in fact a projection of an exponential variety. An exponential variety over a field K is the set of points in Kⁿ where a finite collection of exponential polynomials simultaneously vanish. Wilkie's theorem states that if we have any definable set in an L_exp structure K = (K,+,−,·,0,1,e^x), say X ⊂ K^m, then there will be an exponential variety in some higher dimension Kⁿ such that the projection of this variety down onto K^m will be precisely X.

...
Wikipedia