When does every definable nonempty set have a definable element?

Abstract

The assertion that every definable set has a definable element is equivalent over ZF to the principle $V=\text{HOD}$, and indeed, we prove, so is the assertion merely that every ${\Pi }_2$-definable set has an ordinal-definable element. Meanwhile, every model of ZFC has a forcing extension satisfying $V\ne \text{HOD}$ in which every ${\Sigma }_2$-definable set has an ordinal-definable element. Similar results hold for $\text{HOD}(\mathbb{R})$ and $\text{HOD}({\text{Ord}}^{\omega })$ and other natural instances of $\text{HOD}(X)$.

9 pages. Commentary concerning this article can be made at http://jdh.hamkins.org/definable-sets-with-definable-elements