The notion of a definable set is not expressible in the language of set theory: there is no formula $\delta(x)$ that is equivalent with there being a formula $\phi(y)$ such that $x = \lbrace y : \phi(y)\rbrace$, i.e. for which

$$\delta(x) \leftrightarrow (\exists \phi \in \mathsf{Form})\ x = \lbrace y : \phi(y)\rbrace$$

is provable. (Please forgive my blunt use of the set-builder notation $\lbrace y : \phi(y)\rbrace$. I know there's the rub.)

The same holds for (unrestricted) definitions with parameters: there is no formula $\delta(x)$ that is equivalent with there being a formula $\phi(y,z_1,\dots,z_n)$ such that $x = \lbrace y : \phi(y,z_1,\dots,z_n)\rbrace$ for some $z_1,\dots,z_n$, i.e. for which

$$\delta(x) \leftrightarrow (\exists \phi \in \mathsf{Form})(\exists z_1,\dots,z_n)\ x = \lbrace y : \phi(y,z_1,\dots,z_n)\rbrace$$

is provable.

But the notion of ordinal-definable sets *is* expressible in the language of set theory (see Jech, p. 194), i.e. there *is* a formula $\delta(x)$ such that - bluntly said -

$$\delta(x) \leftrightarrow (\exists \phi \in \mathsf{Form})(\exists z_1,\dots,z_n)\ x = \lbrace y : \phi(y,z_1,\dots,z_n)\rbrace \wedge \mathsf{ON}(z_i) $$

is provable.

My questions are:

Are there other restrictions on the

parameterslike $\mathsf{ON}(z_i)$ (the formula that states that $z_i$ is an ordinal) that give rise to a definable notion of definability, i.e. a class of accordingly definable sets?Can these restrictions been characterized? What do they have in common, eventually? What is essential?

Are there restrictions $\Psi(\phi)$ on the

formulasthat comparably give rise to a definable notion of definability, i.e. there would be a formula $\delta(x)$ such that $$\delta(x) \leftrightarrow (\exists \phi \in \mathsf{Form})(\exists z_1,\dots,z_n)\ x = \lbrace y : \phi(y,z_1,\dots,z_n)\rbrace \wedge \Psi(\phi) $$ is provable.Or maybe some mixture $\Psi(\phi,z_1,\dots,z_n)$?

Question 3 includes: Can we - in a Goedelian way - define for a formula (as a set), that some of its arguments must fulfill some other formula?