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