A theory $T$ is said to have definable choice (or strong definable choice) if the following condition holds: for every formula $\phi (x;y)$ , there is a definable (partial) function $f(y)$ such that if $M\models T$ and $b\in M$ and $\phi (M;b)$ is non-empty, then $f(b)\in \phi (M;b)$ , and moreover, $f(b)$ depends only on $\phi (M;b)$ , i.e., if $\phi (M;b)=\phi (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 $\ulcorner C\urcorner$ .

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 $\phi (M;b)$ . In general, definable choice is equivalent to definable skolem functions in $T^{eq}$ .

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