Complexity of definable global choice functions

Question

It is well-known that $L$ has a $\Sigma_{1}$-definable global choice function; it is also known that there are other transitive class models of ZFC with this property. I wonder about the complexity that such definitions must have; more specifically, whether, for any $n\in\omega$, there is a transitive model of ZFC with a $\Sigma_{n+1}$-definable choice function, but no $\Sigma_{n}$-definable choice function. I assume that this must be known, but I fail to find a reference for this.

Answer 1

There is no such phenomenom for $n\geq 2$.

The reason is that if a model of ZFC has a definable choice function, of any complexity, then it actually has one of complexity $\Delta_2$. This is because the existence of a definable choice function implies $V=HOD$, but the HOD global well order has complexity $\Delta_2$.

Specifically, the HOD order is defined so that $x\leq y$ if and only if the least $\theta$ for which $x$ is definable in $V_\theta$ from ordinal parameters is smaller than that of $y$, or they are the same, but $x$ is definable by a smaller formula, or they are the same, but $x$ is definable with lexically earlier parameters. This is a global well order. And it has complexity $\Delta_2$, since the question of whether it holds or fails can be correctly observed inside any sufficiently large $V_\delta$. From the well order, you get a global choice function by picking the least element, and these choices also are certified in each instance inside any large enough $V_\delta$.

An essentially similar argument shows that even without V=HOD, if an object is definable from ordinal parameters, then there is a $\Delta_2$ definition of it with ordinal parameters. Namely, if it is definable at all, by some formula $\psi(x,\vec\alpha)$, then by reflection this definition works inside some $V_\theta$. And so with $\theta$ as an additional parameter (and the other parameters below $\theta$), we have a $\Sigma_2$ definition: the $x$ such that $V_\theta$ thinks $\psi(x,\vec\alpha)$. This definition has complexity $\Delta_2$, since it is correctly verified inside any larger $V_\delta$.

(Some time ago I wrote a blog post, Local properties in set theory, which some readers may find helpful for the complexity calculations I am using here. The basic fact is that a property is $\Sigma_2$ when it can be verified correctly inside some $V_\theta$.)

Incidentally, to my way of thinking, this complexity calculation and the observations around it are important for the property of V=HOD to be expressible in set theory in the first place. After all, taking V=HOD literally as the assertion that every set is definable from ordinal parameters, it would appear to be an external model-theoretic property about the universe. Why should it be expressible in the first-order language of set theory? Well, the reason it is is because of the reflection argument we gave above. But now the subtle point comes in that if an $\omega$-nonstandard model satisfies V=HOD, in the sense that every object is definable from ordinals inside some $V_\theta$, then the issue is that the defining formula used for this might be a nonstandard formula. Such a formula would not serve as an actual definition in the external model-theoretic sense. Nevertheless, there is no problem, since we can take the Gödel code of the formula as an additional ordinal parameter, and then define the object as: the thing thought to fulfill that formula in $V_\theta$ with those other parameters. So the internal version of V=HOD and the external version are ultimately equivalent.