When does every definable nonempty set have a definable element?
By F. G. Dorais and J. D. Hamkins
- arxiv: 1706.07285
The assertion that every definable set has a definable element is equivalent over ZF to the principle , 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 in which every -definable set has an ordinal-definable element. Similar results hold for and and other natural instances of .