Does choice always hold in a model of ZF with point-wise parameter-free definable sets?

Question

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.

Answer 1

The following fleshes out the comments above by Asaf and Andreas.

First, note that the idea you outline at the end will not work: it implicitly assumes that the relation "$\varphi$ defines $a$" is definable, which is not the case. (Indeed, if that did work it would imply that there are no pointwise-definable models of ZFC.)

To get choice from this scheme, we need something more flexible than outright definability. This is where ordinal definability comes in. It is a standard result that, for $M\models$ ZF and $a\in M$, the following are equivalent:

• There are $M$-ordinals $\alpha,\beta_1,...,\beta_n$ and a formula $\psi$ such that $a$ is the unique element of $(V_\alpha)^M$ such that $(V_\alpha)^M\models\psi(a,\beta_1,...,\beta_n)$.

• There is a formula $\varphi$ and ordinals $\gamma_1,...,\gamma_k$ such that $a$ is the unique element of $M$ such that $M\models\varphi(a,\gamma_1,...,\gamma_k)$.

The point is that the former expression is made within $M$ itself - ordinal definability is definable. Moreover, trivially definability implies ordinal definability, so any model of ZF + your scheme is a model of ZF + "every set is ordinal definable."

Now we can use a "well-order-the-formulas" idea. Specifically, in $M$ we well-order all tuples of the form $(\alpha,\beta_1,...,\beta_n,\psi)$ such that $\psi(-,\beta_1,...,\beta_n)$ defines a unique element of $(V_\alpha)^M$ in the sense of $(V_\alpha)^M$, and these lead to a definable well-ordering of the whole universe.