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

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?

• @Michael Hardy, Thank you for correcting the title. Jun 8, 2023 at 16:53

1 Answer

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.

• So the usual upward Löwenheim–Skolem theorem fails drastically here. This is similar to the situation of characterizing the standard model of arithmetic in $\mathcal L_{\omega_1, \omega}$, where all models are countable! Thanks a lot. Jun 8, 2023 at 16:50