Quantifier elimination in pairs of algebraically closed fields (Q1759771)

The author gives a natural and simple language, call it \(L^f\), for quantifier elimination in proper pairs of fields \((K,L)\), \(K\subsetneq L\), specifically algebraically closed fields. The language \(L^f\) is obtained from the language of pairs of rings by adding predicates for linear disjointness over the small field, and new functions giving the linear components over the small field of the first variable with respect to the other variables. Previous languages for quantifier elimination did not use new functions. The other main result is: Dense proper pairs of algebraically closed valued fields eliminate quantifiers in the language \(L^f\) augmented with the divisibility predicate \(x\mid y\) iff the valuation of \(x\) is at most the valuation of \(y\). There is also a simple description of definable closures. The author used these results in a previous paper [Ann. Fac. Sci. Toulouse, Math. (6) 21, No. 2, 413--434 (2012; Zbl 1283.12001)] to find some \(C\)-minimal expansions of algebraically closed valued fields which are not definably complete.