According to [4, p. 1154], a complete L-theory T eliminates imaginaries just in case for every L-formula φ(x1,… , xm, y1, …, yn), every model M of T, and every ā Є Mn, there is a subset A of M's domain with the following property: if N ≽ M and f is an automorphism of N, then if and only if Among the several equivalent conditions discussed in [4, p. 1155], one may single out the following: if T is a complete theory in which two distinct objects are definable, T eliminates imaginaries just in case every T-definable n-ary equivalence relation may be defined by a formula where g is a T-definable n-ary function taking k-tuples as values (for some natural number k). Say that an L-structure M eliminates imaginaries just in case Th(M) does. If L is the language of rings with unit, [4, p. 1158] shows that any algebraically closed field eliminates imaginaries, and [2, p. 629] points out that any real-closed field eliminates imaginaries.

This note arose out of my efforts to understand results of van den Dries, Denef, and Weispfenning on definable Skolem functions in the elementary theory of Qp. The first person to prove their existence was van den Dries, who devised and applied a model-theoretic criterion for theories, admitting elimination of quantifiers, which also admit definable Skolem functions [3]. The proof, though elegant, does not describe how one defines the Skolem functions. In the particular case of Qp, Denef found an ingenious, easily described method for writing out the definitions [2, pp. 14–15]. Unfortunately, his argument directly applies only in the following special case: if and there is a fixed m ≥ 1 such that for all , then can be given as a definable function of . While this special case includes many of interest, van den Dries' theorem seems more general. Weispfenning suggested how his results on primitive-recursive quantifier elimination could produce algorithms yielding definitions of Skolem functions in the specific theories van den Dries considered [10, pp. 470–471]. Though these algorithms provide a more concrete version of van den Dries' theorem, and do not suffer the lack of generality of Denef's result, Weispfenning's argument is extremely subtle and applies only to certain theories of valued fields.

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).

In his Singular points of complex hypersurfaces Milnor proves the following “curve selection lemma” [10, p. 25]: Let V ⊂ Rm be a real algebraic set, and let U ⊂ Rm be an open set defined by finitely many polynomial inequalities: Lemma 3.1. If U ∩ V contains points arbitrarily close to the origin (that is if 0 ∈ Closure (U ∩ V)) then there exists a real analytic curve with p(0) = 0 and with p(t) ∈ U ∩ V for t > 0. Of course, this result will also apply to semialgebraic sets (finite unions of sets U ∩ V), and by Tarski's theorem such sets are exactly the sets obtained from real varieties by means of the finite Boolean operations and the projection maps Rn+1 → Rn. If, in this tiny extension of Milnor's result, we replace ‘R’ everywhere by ‘Qp’, we obtain a p-adic curve selection lemma, a version of which we will prove in this essay. Semialgebraic sets, in the p-adic context, may be defined just as they are over the reals: namely, as those sets obtained from p-adic varieties by means of the finite Boolean operations and the projection maps . Analytic maps are maps whose coordinate functions are given locally by convergent power series.