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, 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.

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.

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, 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?

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, 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.