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\neq\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)$.
Categories: math.LO