A theory T is said to have definable choice (or strong definable choice) if the following condition holds: for every formula ϕ(x; y), there is a definable (partial) function f(y) such that if M ⊨ T and b ∈ M and ϕ(M; b) is non-empty, then f(b) ∈ ϕ(M; b), and moreover, f(b) depends only on ϕ(M; b), i.e., if ϕ(M; b) = ϕ(M; b′), then f(b) = f(b′).
An equivalent condition is that every non-empty definable set C contains a member definable over the code ⌜C⌝.
Definable choice is a stronger condition than the existence of definable skolem functions. Definable choice implies elimination of imaginaries: given an equivalence relation E, definable choice yields a canonical representative of each equivalence class. Given elimination of imaginaries, definable choice is equivalent to definable skolem functions: in the definition of definable choice, one can replace b with a code for ϕ(M; b). In general, definable choice is equivalent to definable skolem functions in Teq.
To prove definable choice in a theory T, it suffices to prove definable choice in subsets of (the first power of) the home sort. This can be used to show, for example, that any o-minimal expansion of RCF has definable choice (hence eliminates imaginaries). ::: ::: :::