In terms of model theory, Wilkie's theorem deals with the languageLexp = , the language of ordered rings with an exponential function ex. Suppose φ is a formula in this language, then Wilkie's theorem states that there is an integern ≥ m and polynomials f1,...,fr ∈ Z such that φ 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 structureRexp, 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 fieldK is the set of points in Kn where a finite collection of exponential polynomials simultaneously vanish. Wilkie's theorem states that if we have any definable set in an Lexp structure K = , sayX ⊂ Km, then there will be an exponential variety in some higher dimensionKn such that the projection of this variety down onto Km will be precisely X.
Gabrielov's theorem
The result can be considered as a variation of Gabrielov's theorem. This earlier theorem, by 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 cubem. Gabrielov's theorem states that any formula in this language is equivalent to an existential one, as above. Hence the theory of the real ordered field with restricted analytic functions is model complete.
Intermediate results
Gabrielov's theorem applies to the real field with all restricted analytic functions adjoined, whereas Wilkie's theorem removes the need to restrict the function, but only allows one to add the exponential function. As an intermediate result Wilkie asked when the complement of a sub-analytic set could be defined using the same analytic functions that described the original set. It turns out the required functions are the pfaffian functions. In particular the theory of the real ordered field with restricted, totally defined pfaffian functions is model complete. Wilkie's approach for this latter result is somewhat different from his proof of Wilkie's theorem, and the result that allowed him to show that the Pfaffian structure is model complete is sometimes known as Wilkie's theorem of the complement. See also
