Positive elimination in valued fields (Q884991)

Quantifier elimination is well-known in the following four cases: algebraically closed fields, real closed fields, algebraically closed valued fields, and real closed valued fields with convex valuation ring; see e.g. [\textit{A. Prestel}, Einführung in die mathematische Logik und Modelltheorie. Vieweg Studium, 60. Braunschweig/Wiesbaden: Friedr. Vieweg \& Sohn (1986; Zbl 0616.03001)]. In the cases without valuation, there also exists a ``positive quantifier elimination along projective variables''. In the present article, the author generalizes this to the cases with valuation. More precisely, positive constructible (or ``basic'') sets are defined to be unions and intersections of sets of the form \(C_f := \{x\mid f(x) = 0\}\), \(P_f := \{x\mid f(x) \geq 0\}\) (only in the real closed cases), and \(V_{g,h} := \{x\mid g(x) | h(x) \}\) (only in the valued cases). We call such a basic set ``projective in the variable \(Y\)'' if all the involved polynomials \(f, g, h\) are projective in \(Y\) and if in addition in the case \(V_{g,h}\), we have \(\deg_{Y}g = \deg_{Y}h\). Positive quantifier elimination can now be stated as follows: The projection to \(K^n\) of a basic subset \(A \subset K^n \times (K^m\setminus \{0\})\), projective in the last \(m\) variables, is again basic. The main goal of the article is to prove this in the valued cases. In fact, this is a corollary of the following, more general theorem: The projection to \(K^n\) of a basic subset \(A \subset K^n \times \mathcal{O}_v^m\) is again basic. Here, \(\mathcal{O}_v\) is the valuation ring. Note that in the last theorem, no projectivity condition is needed anymore.