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](http://en.wikipedia.org/wiki/Ordinal_definable_set) *is* expressible in the language of set theory (see Jech, p. 194), i.e. there *is* a formula $\delta(x)$ such that - [bluntly said](https://mathoverflow.net/a/146754/2672) - 


$$\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:



> 
> 1. 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?
> 2. Can these restrictions been characterized? What do they have in common, eventually? What is essential?
> 3. 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.
> 4. 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?



Ways to define "definability"
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. 


