When does every definable nonempty set have a definable element?

2017/06/22 by Dorais, François G., Hamkins, Joel David
#FOS: Mathematics #Logic (math.LO)

paper · doi:10.48550/arxiv.1706.07285

Abstract

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 Π₂-definable set has an ordinal-definable element. Meanwhile, every model of ZFC has a forcing extension satisfying V\neqHOD in which every Σ₂-definable set has an ordinal-definable element. Similar results hold for HOD(ℝ) and HOD(Ord^ω) and other natural instances of HOD(X).

Related

• ZFC proves that the class of ordinals is not weakly compact for\n definable classes
• Pointwise Definable Models of Set Theory
• Realizing the totally unordered structure of ordinals
• Ordinal definability in L[𝔼]
• Ordinal Definability and Combinatorics of Equivalence Relations