An effective version of Wilkie's theorem of the complement and some effective o-minimality results

Wilkie (Selecta Math. (N.S.) 5 (1999) 397) proved a “theorem of the complement” which implies that in order to establish the o-minimality of an expansion of R with C ∞ functions it suffices to obtain uniform (in the parameters) bounds on the number of connected components of quantifier free definable sets. He deduced that any expansion of R with a family of Pfaffian functions is o-minimal. We prove an effective version of Wilkie’s theorem of the complement, so in particular given an expansion of the ordered field R with finitely many C^∞ functions, if there are uniform and computable upper bounds on the number of connected components of quantifier free definable sets, then there are uniform and computable bounds for all definable sets. In such a case the theory of the structure is effectively o-minimal: there is a recursively axiomatized subtheory such that each of its models is o-minimal. This implies the effective o-minimality of any expansion of R with Pfaffian functions. We apply our results to the open problem of the decidability of the theory of the real ÿeld with the exponential function. We show that the decidability is implied by a positive answer to the following problem (raised by van den Dries (in: Logic: From Foundations to applications, Oxford Science Publ., Oxford University Press, New York, 1996, p. 137)): given a language L expanding the language of ordered rings, if an L-sentence is true in every L-structure expanding the ordered field of real numbers, then it is true in every o-minimal L-structure expanding any real closed field.