Effective Model Completeness of the Theory of Restricted Pfaffian Functions

Pfaffian functions, introduced by Khovanskii in late 70s, are analytic functions satisfying triangular systems of first order partial differential equations with polynomial coefficients. They include for instance algebraic and elementary transcendental functions in the appropriate domains, iterated exponentials, and fewnomials. A simple example, due to Osgood, shows that the first order theory of reals expanded by restricted Pfaffian functions does not admit quantifier elimination. On the other hand, Gabrielov and Wilkie proved (non-constructively) that this theory is model complete, i.e., one type of quantifiers can be eliminated. The talk will explain some ideas behind recent algorithms for this quantifier simplification which are based on effective cylindrical cell decompositions of sub-Pfaffian sets. Complexities of these algorithms are essentially the same as the ones which existed for a particular case of semialgebraic sets.