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?

  • 4
    $\begingroup$ 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. $\endgroup$ Nov 24, 2021 at 8:23

1 Answer 1


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.

  • 1
    $\begingroup$ would that result also hold if we remove Foundation axiom? $\endgroup$
    – Zuhair
    Nov 24, 2021 at 8:56
  • 1
    $\begingroup$ 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. $\endgroup$
    – Asaf Karagila
    Nov 24, 2021 at 9:00

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .