Does adding definability axiom expressed in infinitary language to ZF, let all models be pointwise definable?

Question

This posting is generally related to a prior posting titled "Are all constructible from below sets parameter free definable?"

If we work in infinitary language $\mathcal L_{\omega_1, \omega}$, then we can define parameter free definable, denoted "$D$", as:

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

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

Axiom of definability: $\forall x Dx$

Let $\sf ZF + Def$ be the theory that extends $\mathcal L_{\omega_1, \omega}$ with axioms of $\sf ZF$ (written in $\mathcal L_{\omega, \omega}$) and the axiom of definability.

Is $\sf ZF +Def$ consistent ?

If so then does $\sf ZF + Def$ have all of its models being pointwise definable models?

Answer 1

Yes, the theory is consistent, if ZF is consistent, because there are pointwise definable models of ZF. Any such model is a model of your theory, which is therefore satisfiable and hence consistent.

And yes, clearly every model of your theory is pointwise definable (in the first-order language), because that is precisely what your axiom of definability asserts. The only way to make this axiom true in a model of ZF is for every set to be definable.

The models of ZF+Def are exactly the pointwise definable models of ZF.