A theory is said to have **definable choice** (or *strong definable choice*) if the following condition holds: for every formula , there is a definable (partial) function such that if and and is non-empty, then , and moreover, depends only on , i.e., if , then .

An equivalent condition is that every non-empty definable set contains a member definable over the code .

Definable choice is a stronger condition than the existence of definable skolem functions. Definable choice implies elimination of imaginaries: given an equivalence relation , 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 with a code for . In general, definable choice is equivalent to definable skolem functions in .

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