# Is Choice over definable sets equivalent to AC?

If we add the following axiom schema to $$\sf ZF$$, would the resulting theory prove $$\sf AC$$?

Definable sets Choice: if $$\phi$$ is a formula in which only the symbol $$y"$$ occurs free, then: $$\forall X (X=\{y \mid \phi\} \to \\\exists f (f:X \setminus \{\emptyset\} \to \bigcup X \land \forall x (f(x) \in x)))$$

If not, then which form of choice this is equivalent to?

• I think it implies choice. By absurd, suppose that it does not. Then, you can define the smallest ordinal $\alpha$ such that $V_\alpha$ doesn't have a choice function, and therefore $V_\alpha$ is definable by a unique first-order formula, and must have a choice function. Nov 24, 2021 at 8:23

Yes, for the silliest reasons. First note that if $$\alpha$$ is definable without parameters, then so is its second power set, so the scheme implies that $$2^\alpha$$ can be well-ordered.
Next, note that the least $$\alpha$$ whose power set cannot be well-ordered is definable. Indeed, that is the definition.
So we get that the power set of every ordinal is well-orderable, and therefore choice holds. You can play this game using the $$V_\alpha$$S instead, if using the power sets of ordinals feels awkward.
• It's complicated. If you work in ZFA+the atoms form a set, then the answer is yes (by using the argument via $V_\alpha(A)$ for the least $\alpha$). If the atoms are not a set, then you might not be able to uniformly definable that least $\alpha$ over any set of atoms. In general for ZF-Fnd, probably the answer is a lot more nuanced if you want to look for exact equivalence. I'd reckon that the equivalence does not hold over ZF-Fnd, though. Nov 24, 2021 at 9:00