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

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 all sets are definable, then all sets are ordinal definable, then $V=\rm HOD$ holds, then global choice holds. – Asaf Karagila Nov 20 '19 at 21:47
• Although, as @Asaf pointed out, AC does follow from your scheme (by taking $\varphi(x)$ to be "$x$ is ordinal definable"), the idea in the last paragraph of the question won't work, because definability (unlike ordinal definability) isn't definable. – Andreas Blass Nov 20 '19 at 22:40
• The facts that one property (parameter-free definability) implies another (ordinal definability) and that the latter is definable do not entail that the former is also definable. (I think you may be using "special case" and "kind of" ambiguously.) – Andreas Blass Nov 22 '19 at 13:51
• In considering Andreas' comment, it may be helpful to first recall that subsets of computable sets need not be computable. (The analogy is: subset ~ subcollection and computable ~ 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.) – Noah Schweber Nov 22 '19 at 17:57
• It may also help to replace ordinal definability with definability-in-some-arbitrary-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 sense everything is a special case of parameter-definability!). – Noah Schweber Nov 22 '19 at 18:00

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.