Complexity of definable global choice functions

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.

New contributor
MCarl is a new contributor to this site. Take care in asking for clarification, commenting, and answering. Check out our Code of Conduct.
• 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 logic-related posts stretching back many years. If these are you, you can contact the moderators to merge your various user accounts into one. Commented Jun 9 at 14:07

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.