It is wellknown 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.

$\begingroup$ By the way, I'm not sure if this is relevant, but I happened to notice that there are several users named "M Carl" with logicrelated posts stretching back many years. If these are you, you can contact the moderators to merge your various user accounts into one. $\endgroup$– Joel David HamkinsCommented Jun 9 at 14:07
1 Answer
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 modeltheoretic property about the universe. Why should it be expressible in the firstorder 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 modeltheoretic 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.