Add a primitive one place predicate symbol $\mathcal Df$, signifying "is parameter free definable", to the language of $\sf ZF$, and add the following:
Axiom scheme of definability: If $\varphi(Y)$ is a formula that doesn't use the symbol $“\mathcal Df"$, in which only the symbol $“Y"$ occur free, and never occur as bound, then:$$\forall X [\forall Y (Y \in X \leftrightarrow \varphi(Y)) \to \mathcal Df(X)]$$; is an axiom.
Axiom of definable choice:
$\forall X [\emptyset \not \in X \to \\\exists F (F:X \to \bigcup(X) \land \forall x \in X(\mathcal Df(x) \to F(x) \in x))]$
In English: For any family of non empty definable sets there is a function that sends each set in it to an element of that set.
Question: Now to which of the known forms of axiom of choice this would be equivalent?
IF not equivalent to any, then would it entail existence of non-measurable sets as $AC$ does.
Where by equivalent it is meant some choice statement $\varphi$ in the pure language of set theory [i.e.; doesn't use the symbol $\mathcal Df$] that is provable here, and such that on the other hand "$\sf ZF$ + Definability + $\varphi$" would prove definable choice.
Best Answer
Let $\mathcal{L}$ be the language of set theory, and let $\mathcal{L'}$ be the extended language with $\mathcal{Df}$. Let's write $\text{Def}$ for the definability schema, and $\text{DefC}$ for definable choice. You're looking for an $\mathcal{L}$-sentence $\varphi$ which is equivalent to $\text{DefC}$ over $\mathsf{ZF} + \text{Def}$.
I claim that if an $\mathcal{L}$-sentence $\varphi$ satisfies $\mathsf{ZF} + \text{Def} + \varphi\vdash \text{DefC}$, then already $\mathsf{ZF} + \varphi \vdash \text{AC}$.
To see this, let $M$ be any model of $\mathsf{ZF} + \varphi$. Then we can expand $M$ to an $\mathcal{L}'$-structure $M'\models \mathsf{ZF} + \text{Def} + \varphi$ by interpreting $\mathcal{Df}$ to hold of every set (note that $\text{Def}$ only says that certain sets satisfy $\mathcal{Df}$, it doesn't require that any sets fail to satisfy $\mathcal{Df}$). Thus $M'\models \text{DefC}$. But since $\mathcal{Df}$ holds of every set in $M'$, this implies that $M\models \text{AC}$. So by the completeness thoerem, $\mathsf{ZF} + \varphi \vdash \text{AC}$.
It follows that if $\varphi$ is equivalent to $\text{DefC}$ over $\mathsf{ZF}+\text{Def}$, then $\mathsf{ZF}+\text{Def}+\text{DefC}\vdash \varphi$, and since $\mathsf{ZF}+\varphi\vdash \text{AC}$, we have $\mathsf{ZF}+\text{Def}+\text{DefC}\vdash \text{AC}$. I don't believe the latter conclusion (since there should be a model of $\mathsf{ZF}$ which satisfies choice for all parameter-free definable sets but not all sets), so I would conclude that $\text{DefC}$ is not equivalent to any $\mathcal{L}$-sentence over $\mathsf{ZF}+\text{Def}$.