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?