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 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.

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.

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.

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 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$.

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.

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 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.