A quantifier elimination for the theory of \(p\)-adic numbers (Q1277096)

A lower bound for the decision problem in the first order theory of \(p\)-adic numbers has been known for a long time. As for the upper bound, the best algorithm known so far is that of \textit{P. J. Cohen} [Decision procedures for real and \(p\)-adic fields, Commun. Pure Appl. Math. 22, 131-151 (1969; Zbl 0167.01502)]; it is primitive recursive but not elementary. The analysed formula is expanded dramatically each time a quantifier is eliminated. A similar problem was faced before in the context of the first order theory of the reals \textit{Th} \(\mathbb R\). Consider, for instance, Cohen's real counterpart of his own algorithm for \textit{Th} \(\mathbb Q_p\). It treats the quantified variables one at a time and suffers from exponential growth at each step of the recursion. Consider the solution proposed in the real case by \textit{G. E. Collins} [Quantifier elimination for real closed fields by cylindrical algebraic decomposition, Lect. Notes Comput. Sci. 33, 134-183 (1975; Zbl 0318.02051)]. Every atomic formula in the language of \textit{Th} \(\mathbb R\) is a polynomial inequality, in other words, it states that some polynomial is a square. Collins' procedure partitions a space into a finite number of sets (Cells), in each of which every polynomial that appears in the sentence to be decided has constant sign. Then a point is chosen from each cell \(C\) to determine the sign that each of the polynomials involved has in \(C\). Now each existential (resp. universal) quantifier can be replaced by a finite disjunction (resp. conjunction) of the polynomial inequalities evaluated in the sample points. So, a block of quantifiers is eliminated in a single step. The decomposition of the space into cells can be done efficiently. Some analogies between the real field and the \(p\)-adic field \(\mathbb Q_p\) suggest that it is reasonable to expect that an elementary algorithm could be obtained by using Collins' method on the \(p\)-adics. In [\textit{P. Scowcroft} and \textit{L. van den Dries}, On the structure of semialgebraic sets over \(p\)-adic fields, J. Symb. Logic 53, 1138-1164 (1988; Zbl 0692.14014)] the authors state that the essential algebra needed for extending the method to the \(p\)-adic case is provided by J. Denef's study of a cylindrical algebraic decomposition for \( \mathbb Q_p\). Nevertheless, a deep difference between topological properties of the two fields (reals and \(p\)-adics) complicates the \(p\)-adic setting. The topology of \( \mathbb Q_p\) is totally disconnected, and no analogue of Sturm's theorem is known so far. This has serious implications for the quantifier elimination. The present paper studies Collins' method and uses Denef's ideas in addition. It is aimed at a better understanding of the complexity of the theory of \(p\)-adic numbers and stimulating further discussion on the subject.