$\sf ZF + Def$ is the theory that extends $\mathcal L(=,\in)_{\omega_1,\omega}$ with axioms of $\sf ZF$ (written in $\mathcal L(=,\in)_{\omega, \omega}$) and the axiom of definability:-

$\textbf{Define: } Dx \iff \bigvee x= \{ y \mid \Phi \}$

where $\Phi$ range over all formulas in $\mathcal L(=,\in)_{\omega, \omega}$ in which only the symbol "$y$" occurs free, and the symbol "$y$" never occurs bound.

Axiom of definability: $\forall x Dx$

This theory has its models being exactly the pointwise-definable models of $\sf ZF$ [Hamkins]

Now, if one wants to confine matters to $\mathcal L(=,\in)_{\omega,\omega}$, i.e. the usual $\textbf{FOL}(=,\in)$, then one can add this rule to $\sf ZFC$:

$\textbf{Definability: }$ if $\phi_1,\phi_2, \phi_3,...$ are all formulas in which only symbol "$y$" occurs free, and "$y$" never occur bound, and that doesn't use the symbol "$x$", and $\psi$ is a formula in which only symbol "$x$" occurs free, and "$x$" never occur bound; then:

$\underline {[i=1,2,3,...; \\ \forall x \, (x=\{y \mid \phi_i\} \to \psi)]} \\ \forall x: \psi$

In English: if a parameter free formula holds for all parameter free definable sets, then it holds for all sets.

This was proved by Hamkins to be equivalent over $\sf ZFC$ to the set theoretic axiom $\sf V=HOD$.

The finitary version of definability doesn't manage to confine all of its models to be the pointwise-definable models of $\sf ZFC$. [see here]. But, it can be argued to be the finitary parallel of the infinitary version.

My question here is:

Are there finitary sentences (i.e. in $\mathcal L(=,\in)_{\omega,\omega}$) that are theorems of $\sf ZF + Def$ yet not provable in $\sf ZFC + \text { Definability rule}$ (or equivalently in $\sf ZFC+[V=HOD])$? Or is the former a conservative extension of the latter?

If there are such sentences, are there clear examples?


1 Answer 1


Any model of ${\sf ZFC}+V=\sf HOD$ has an elementary equivalent pointwise definable model.

If $M$ models $V=\sf HOD$, it has a parameter free definable well ordering, for each formula $φ$ consider the Skolem function that gives the least witness using that well ordering, the class $M_0$ of definable (without parameters) elements of $M$ will be closed under those Skolem functions, so $M\succ M_0$, because $M_0$ is elementary substructure of $M$, the definable elements of $M_0$ are exactly equal to those of $M$, so by construction $M_0$ is pointwise definable model that is elementary equivalent to $M$.

In other words, $\sf ZFC$+"being pointwise definable" does not prove anything that ${\sf ZFC}+V=\sf HOD$ does not prove in the language of FOST

  • $\begingroup$ so $\sf ZF + Def$ is a conservative extension of $\sf ZFC + Definability \ rule$, that's what you are saying, right? I don't know why I feel that this is not the case. $\endgroup$ Jun 27, 2023 at 20:45
  • $\begingroup$ I'm getting the impression that what you did is just proving that the Definability rule (which is an omega rule in finitary FOST) and V=HOD are equivalent, which is already mentioned in the posting. I don't think you proved that the infinitary expression of Definability is equivalent to the finitary version over the language of FOST. Not sure though? $\endgroup$ Jun 27, 2023 at 23:09
  • 1
    $\begingroup$ @ZuhairAl-Johar I have shown that $ZFC+Def$ is conservative to $ZFC+Definability\ rule$, if the former proves $\phi$ a statement in FOST and the latter does not, let $M$ be a witness (a model of the latter + $\lnot\phi$), then the $M_0$ I defined will be a model of $ZFC+Def+\lnot\phi$, which is a contradiction $\endgroup$
    – Holo
    Jun 28, 2023 at 7:25

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.