(1.1) A well-known example of a theory with built-in Skolem functions is (first-order) Peano arithmetic (or rather a certain definitional extension of it). See [C-K, pp. 143, 162] for the notion of a theory with built-in Skolem functions, and for a treatment of the example just mentioned. This property of Peano arithmetic obviously comes from the fact that in each nonempty definable subset of a model we can definably choose an element, namely, its least member.

(1.2) Consider now a real closed field R and a nonempty subset D of R which is definable (with parameters) in R. Again we can definably choose an element of D, as follows: D is a union of finitely many singletons and intervals (a, b) where – ∞ ≤ a < b ≤ + ∞; if D has a least element we choose that element; if not, D contains an interval (a, b) for which a ∈ R ∪ { − ∞}is minimal; for this a we choose b ∈ R ∪ {∞} maximal such that (a, b) ⊂ D. Four cases have to be distinguished:

(i) a = − ∞ and b = + ∞; then we choose 0;

(ii) a = − ∞ and b ∈ R; then we choose b − 1;

(iii) a ∈ R and b ∈ = + ∞; then we choose a + 1;

(iv) a ∈ R and b ∈ R; then we choose the midpoint (a + b)/2.

It follows as in the case of Peano arithmetic that the theory RCF of real closed fields has a definitional extension with built-in Skolem functions.