Definability and fast quantifier elimination in algebraically closed fields (Q798314)

A celebrated theorem of Tarski asserts the existence of a primitively recursive procedure for elimination of quantifiers in algebraically closed fields. The present work - an extended version of papers by \textit{J. Heintz} and \textit{R. Wüthrich} [SIGSAM Bull. 9, No.4, 11 (1975)] and by \textit{J. Heintz} [Fundamentals of computation theory '79, Proc. Conf., Berlin/Wendisch-Rietz 1979, 160-166 (1979; Zbl 0439.03003)] - is devoted to the theorem above and to related definability problems from the point of view of complexity. The main result proved in this paper shows that there exists a quantifier elimination procedure for algebraically closed fields with a time bound which is polynomial in degree and maximum length of the coefficients of the polynomials appearing in the input formula but double exponential in the number of variables of the input formula. A closely related question concerning the cardinality of the finite sets definable by prenex first order formulas in the language of fields is also investigated. The main parameters occurring in the answer to this question are the sum of the degrees of the polynomials, the total number of variables, and the number of bounded variables in the formulas under consideration. The method is based on a version of Bezout's theorem without multiplicities, called by the author the Bezout-inequality.