Ways to define "definability" 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 parameters like $\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 formulas that 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?
 A: With respect to question 3: one way to do this is to restrict the quantifier complexity of the formulas. That is, for every constant $k$, one can define a formula $\delta_k(x)$ expressing “$x$ is definable by a $\Sigma_k$-formula with parameters”. Here, a formula $\phi(\vec x)$ is $\Sigma_k$ (in the Lévy hierarchy) if it can be written in the form $\exists y_1\,\forall y_2\,\exists y_3\,\dots Qy_k\,\theta(\vec x,\vec y)$, where all quantifiers in $\theta$ are bounded.
$\def\Tr{\mathrm{Tr}}$EDIT: Let me clarify how exactly $\Sigma_k$-formulas can be used to answer question 3. What I wrote above is true, but useless by itself, because definability of sets by formulas allowing arbitrary parameters is not an interesting notion (every set is trivially definable from itself as a parameter). But the Lévy hierarchy provides more than that:


*

*For every $k>0$, there is a truth definition for $\Sigma_k$-formulas, which is itself $\Sigma_k$. That is, there is a $\Sigma_k$-formula $\Tr_k(n,x)$ such that ZF proves
$$\phi(x)\leftrightarrow\Tr_k(\ulcorner\phi\urcorner,x)$$
for every $\Sigma_k$-formula $\phi(x)$, where $\ulcorner\phi\urcorner$ is the Gödel number of $\phi$. This is essentially optimal: if a class of formulas has a truth definition, it is up to equivalence included in some $\Sigma_k$ (because the truth definition itself is in $\Sigma_k$ for some $k$).

*If $k>0$, and $X$ is a class of possible parameters which includes $\omega$ and is closed under pairing (that is, $X\times X\subseteq X$), there is a formula $\delta(x)$ which expresses “$x$ is $\Sigma_k$-definable using parameters from $X$”, namely
$$\delta(x)=\exists n\in\omega\,\exists z\in X\,\forall y\,(y\in x\eq\Tr_k(n,\langle y,z\rangle)).$$
(Here, the pairing operation on $X$ does not have to be the standard Kuratowski pair. For example, one can define an injection $\mathrm{Ord}\times\mathrm{Ord}\to\mathrm{Ord}$, which allows us to take $X=\mathrm{Ord}$, so this generalizes ordinal definability. Also, I believe the assumption $\omega\subseteq X$ is redundant as long as $|X|\ge2$, because one can reconstruct a suitable copy of $\omega$ inside $X$ using the pairing operation.)
A: I am glad to see this question, Hans, which I believe gets right to the heart of the definability concept, on which some of your recent questions have focused. This is an excellent question.
First, let me say that I dispute your characterization of the OD sets. The claim that you state is not what is proved about OD, since your claim is not expressible, as it makes use of a Tarskian truth predicate (you quantify over the formulas $\varphi$, and then refer to the truth of $\varphi$), but we have no such truth predicate. Similarly, question 3 is problematic, since it also essentially refers to a truth predicate, and this is the typical pitfall of those who treat definability naively.
What is actually proved is this. We have a definable class OD, and then we prove, as a separate claim about each formula $\varphi$, that the set defined by $\varphi$ with ordinal parameters is in OD. And conversely, we can see directly that each set in OD is defined by a formula with ordinal parameters. 
The crucial thing that makes it work in the case of OD is the reflection theorem, which says of every formula $\varphi$ (as a separate theorem for each formula), there is a proper class club of ordinals $\alpha$ for which $\varphi$ is absolute between $V_\alpha$ and $V$. Thus, we define that $x\in \text{OD}$ just in case there is $\alpha$ such that $x$ is definable in the structure $\langle V_\alpha,{\in}\rangle$ with ordinal parameters (this is expressible since $V_\alpha$ is a set and so we may refer to truth in it). The point now is that if $x$ is ordinal definable by some formula in $V$, then this will reflect to some $V_\alpha$, and so $x$ will be placed into OD. And conversely, if we think that $x$ is ordinal definable in $V_\alpha$, then by using those parameters, plus $\alpha$, plus the Gödel code of the formula, we can define $x$ from ordinal parameters in $V$. 
In regard to question 3, the analysis shows that every set in OD is actually $\Delta_2$-definable from ordinals, since if $x$ is defined by some formula $\varphi(\cdot,\vec \alpha)$, then we may fix a $\beta$ above $\vec\alpha$ for which $\varphi$ is absolute between $V_\beta$ and $V$, and note that $x$ is definable inside $V_\beta$ by $\varphi(\cdot,\vec\alpha)$. But now we can define $x$ in $V$ using parameter $\beta$ as "the set defined in $V_\beta$ by $\varphi(\cdot,\vec\alpha)$." This can be expressed as a $\Sigma_2$ assertion and also as a $\Pi_2$ assertion, using parameters $\vec\alpha,\beta$ and $\varphi$. And so we thereby bring the complexity of the definition down. The amusing thing, now, is that we have thereby reduced definability to a case for which we do have a Tarskian truth predicate, since there is a $\Sigma_n$-expressible truth predicate for $\Sigma_n$ truth. 
One can generalize beyond ordinal definability, provided that one has these essential features. Namely, if $Z$ is a class of parameters, including the natural numbers, such that we have a definable map $z\mapsto M_z$, for $z\in Z$, which reflect truth from $V$, in the sense first, that the union of all $M_z$ is $V$, and that for any formula $\varphi$ there are sufficiently large $M_z$ where $\varphi$ is absolute between $M_z$ and $V$. We can then define that $x$ is $Z$-definable, if $x$ is definable in some $M_z$ using parameters from $Z$. 
In the case of ordinal definability, the structures are $\alpha\mapsto V_\alpha$. One could use regular-cardinal-definability, via $\kappa\mapsto H_{\kappa^+}$, but this would give the same OD notion. Although it will always be fine to refer to a larger definable class of parameters than the ordinals, there aren't any strictly smaller classes of parameters to my knowledge that give a distinct notion of definability than ordinal-definability. 
