Is ZF + Def a conservative extension of ZFC+HOD? If not, what are counter-examples?

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

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
• 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. Jun 27, 2023 at 20:45
• @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