When does every definable nonempty set have a definable element?

摘要

The assertion that every definable set has a definable element is equivalent over ZF to the principle V=HOD, and indeed, we prove, so is the assertion merely that every ∏_2-definable set has an ordinal-definable element. Meanwhile, every model of ZFC has a forcing extension satisfying V≠HOD in which every ∑_2-definable set has an ordinal-definable element. Similar results hold for HOD(R) and HOD(Ord~ω) and other natural instances of HOD(X).