This posting is generally related to a prior posting titled ["Are all constructible from below sets parameter free definable?"](https://mathoverflow.net/questions/448130/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?
> 
> 
> 



Does adding definability axiom expressed in infinitary language to ZF, let all models be pointwise definable?
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.


