Does cardinal definable choice imply AC?

Question

Recall the definition of cardinal definable sets, to re-iterate:

$Define: X \text { is cardinal definable} \iff \\\exists \text { cardinal } \kappa \, \exists \text { cardinals } \lambda_1,.., \lambda_n <^\rho \kappa \ \exists \phi : \\ X=\{ y \in V_{\rho(\kappa)} \mid \phi^{V_{\rho (\kappa)}} (y,\lambda_1,..,\lambda_n)\}$

Where: $\lambda_i <^\rho \kappa \iff \rho(\lambda_i) < \rho(\kappa)$, and $\rho$ is the rank function; and "cardinal" is defined after Scott's as an equivalence class under bijection of sets of the lowest possible rank.

That every set is cardinal definable is proved consistent with the failure of choice (see here), on the other hand, it is also proved consistent with choice (see here).

Now, working in $\sf ZF$, if we say that every cardinal definable set admits a choice function, would that entail full $\sf AC$?

If we work in $\sf ZF-Reg.$, would cardinal definable choice imply $\sf AC$?

Answer 1

Over ZF yes, it does.

Let $X$ be any family of nonempty sets, and let $κ$ be cardinal such that $ρ(κ)>ρ(X)$, then $V_{ρ(κ)}\setminus\{∅\}$ is cardinal definable, hence has a choice function that induce a choice function on $X$.

In ZF-Regularity Scott trick doesn't work anymore, in fact Lévy has shown that it is consistent with ZF-Regularity that there is no assignment to each set a cardinality in any way (that is: it is consistent that there is no $C:V→V$ such that $C(x)=C(y)⇔|x|=|y|$ (even with parameters)).

In e.g. ZF-Regularity+AFA were you do have possible definition of cardinality for every set, similar idea to what I wrote above works: You start with with a set $X$, and define $X'=X\cap WF$ and $X^∘=X\setminus X'$, by the above $X'$ has a choice function, for $X^∘$ define $Y$ to be the class of accessible pointed graphs who are pictures for elements is in $Y$. Let $f:Y∩WF→X^∘$ be a function that sends $y$ to the unique element in $X^∘$ that $y$ is it's picture.

Note that $f''(Y∩WF)=X^∘$, and in fact that there exists a set $Z\subseteq Y∩WF$ such that $f''Z=X^∘$ (We don't need choice to get this $Z$, we can use Scott's trick, because $Y∩WF\subseteq WF$).

From the above $Z$ and $\bigcup Z$ are well-orderable, so let $x\in X^∘$, and $(G,E)∈Z$ be the minimal graph with the unique decoration $π$ such that $x\in\pi'' G$, and let $p$ be the minimal element (in $\bigcup Z$) such that such that $p E\pi^{-1}(x)$, and so $π(p)∈x$ and we have a choice function on $X=X'⊔X^∘$