If one add to ZF the rule that all sets are parameter free definable. Would that prove the axiom of choice?

More specifically. IF we add the following omega rule to inference rules of the language of ZF.

if $\phi_0, \phi_1, \phi_2,...,$ are all formulas in the first order language of set theory, in which only the symbol $``y"$ occur free, and only free, and if $\varphi(x)$ is a formula in which only $x$ occurs free, and only free, then:

From the scheme: $i=0,1,2,3,... \forall x: x=\{y|\phi_i\} \to \varphi(x)$

We Infer:

$\forall x: \varphi(x)$

Would that prove the axiom of choice?

The idea is that if all sets are definable after parameter free formulas, then we can well order all sets after the Godel numbers of the formulas defining them, thus enacting choice.

subsetsofcomputablesets need not becomputable. (The analogy is: subset~ subcollectionandcomputable~definable. The collection of definable sets is always a sub-collection of the collection of ordinal-definable sets, but the definability of the latter in no way implies the definability of the former - just as a subset of a computable set need not be computable.) $\endgroup$ – Noah Schweber Nov 22 '19 at 17:57arbitrary-parameter. The point is that every set is trivially definable from a parameter (namely, use the set itself as a parameter), so "definability from arbitrary parameters" is definable (by "$x=x$"); but clearly there's no reason to believe that every "special case" of this property is also definable (since in a senseeverythingis a special case of parameter-definability!). $\endgroup$ – Noah Schweber Nov 22 '19 at 18:001more comments