Abstract
A definably complete structure K is an expansion of an ordered field, such that every bounded definable subset of the dom(K) has a least upper bound. The class of all definably complete structure in a given language is recursively axiomatized. Classic examples of definably complete structures are: any expansion of the real ordered field; any o-minimal expansion of a real closed field.
We prove some basic properties of definably complete structures, such as, for example: some basic calculus results, Uniqueness of the solutions of linear differential equations, Implicit function theorem, Taylor's theorem, Newton's method, the transfer of the existence of nonsingular zeroes of so called "standard functions". In the same setting, we then prove a stratification theorem for "noetherian varieties", which in turn allows us to prove a finiteness result for "Khovanskii varieties".
The results mentioned above are mostly motivated by the problem of the decidability of the real exponential field. In particular, they allow us to provide a simple candidate for a recursive axiomatization.