Can ZF prove choice over families of sets of ordinal definable sets?

39 Views Asked by At

Suppose that $X$ is a family of sets of ordinal definable sets.

Can ZF prove the existence of a choice function over $X$?

To put the question formally:

Is the following a theorem of ZF? $$\forall X : \forall y \in \bigcup X (y \text{ is ordinal definable}) \\ \to \exists f (f: X \setminus \{\emptyset\} \to \bigcup X, \forall x (f(x) \in x)) $$

1

There are 1 best solutions below

0
On BEST ANSWER

The class $\sf OD$ is just the closure of $\{V_\alpha\mid\alpha\in\rm Ord\}$ under Gödel operations (see Jech's Set Theory section on "Ordinal Definable Sets").

This means there is a definable well-ordering of $\sf OD$ by means of recursive construction of the definition.

Therefore, if $\bigcup X\subseteq\sf OD$, then there is a definable choice function from $X$.