Then Wilkie's theorem states that there is an integer n ≥ m and polynomials f1, ..., fr ∈ Z[x1, ..., xn, ex1, ..., exn] such that φ(x1, ..., xm) 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 Rexp, that is the real ordered field with the exponential function, is model complete.
This earlier theorem of Andrei Gabrielov dealt with sub-analytic sets, or the language Lan of ordered rings with a function symbol for each proper analytic function on Rm restricted to the closed unit cube [0, 1]m. Gabrielov's theorem states that any formula in this language is equivalent to an existential one, as above.
[2] Hence the theory of the real ordered field with restricted analytic functions is model complete.
[1] In particular the theory of the real ordered field with restricted, totally defined Pfaffian functions is model complete.