[FOM] Definable sets in ZFC

[Florian Rabe]

Dear FOMers,

I have some questions regarding definable sets. To be precise, let me say what I mean by "definable":

- Let ZF be the first-order language of set theory with the usual axioms. If the answer to any of my questions depends on the choice of axioms (e.g., with/without choice), I would be very interested in that as well.

- Call a set S definable if there is a ZF-formula F(x) such that "exists^! x.F(x)" is a theorem and F(S) holds. Here exists^! is the quantifier of unique existence.

Clearly, not all sets are definable because there are only countably many formulas F. Therefore, my questions:

1) What are some examples of non-definable sets?
   I'm particularly interested in sets that
   - can be described informally as in "the set S which ..."
   - are relevant in mathematical practice

2) Are the definable sets the same as the ones in Gödel's constructible universe?
   If not, what is their relation?

3) Do the definable sets form a model of ZF?

4) Is there a set containing
   a) exactly the definable sets?
   b) at least the definable sets?

5) Is there a ZF formula P(x) such that P(S) is true for
   a) exactly the definable sets S?
   b) at least the definable sets S (but not for all sets S)?

6) If an answer to 4a-5b is No, are there more expressive variants of ZF for which the answer is Yes?

I'm not sure which of these questions are trivial. I'd appreciate pointers to the literature as well.

Best,
Florian