A theory {\displaystyle T} is said to have definable choice (or strong definable choice) if the following condition holds: for every formula {\displaystyle \phi (x;y)}, there is a definable (partial) function {\displaystyle f(y)} such that if {\displaystyle M\models T} and {\displaystyle b\in M} and {\displaystyle \phi (M;b)} is non-empty, then {\displaystyle f(b)\in \phi (M;b)}, and moreover, {\displaystyle f(b)} depends only on {\displaystyle \phi (M;b)}, i.e., if {\displaystyle \phi (M;b)=\phi (M;b')}, then {\displaystyle f(b)=f(b')}.

An equivalent condition is that every non-empty definable set {\displaystyle C} contains a member definable over the code {\displaystyle \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 {\displaystyle 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 {\displaystyle b} with a code for {\displaystyle \phi (M;b)}. In general, definable choice is equivalent to definable skolem functions in {\displaystyle T^{eq}}.

To prove definable choice in a theory {\displaystyle 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). ::: ::: :::