## FANDOM

78 Pages

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