To eliminate quantifiers in the first-order theory of the p-adic field Qp, Ax and Kochen use a language containing a symbol for a cross-section map n → pn from the value group Z into Qp [1, pp. 48–49]. The primitive-recursive quantifier eliminations given by Cohen [2] and Weispfenning [10] also apply to a language mentioning the cross-section, but none of these authors seems entirely happy with his results. As Cohen says, “all the operations… introduced for our simple functions seem natural, with the possible exception of the map n → pn” [2, p. 146]. So all three authors show that various consequences of quantifier elimination—completeness, decidability, model-completeness—also hold for a theory of Qp not employing the cross-section [1, p. 453; 2, p. 146; 10, §4]. Macintyre directs a more specific complaint against the cross-section [5, p. 605]. Elementary formulae which use it can define infinite discrete subsets of Qp; yet infinite discrete subsets of R are not definable in the language of ordered fields, and so certain analogies between Qp and R suggested by previous model-theoretic work seem to break down.To avoid this problem, Macintyre gives up the cross-section and eliminates quantifiers in a theory of Qp written just in the usual language of fields supplemented by a predicate V for Qp's valuation ring and by predicates Pn for the sets of nth powers in Qp (for all n ≥ 2).
Automated reasoning-alternative methods
