Is it possible for there to be a model of ZFC with the property that, for every set $S$ in the model, there is a unary predicate in the language of ZFC such that $S$ is the is the only set satisfying the predicate?
I'm pretty sure I've been told the answer is "yes", but I am never able to find a reference when I want one. So this question (assuming it is answered in the affirmative) is to be that reference!
On
The minimal model $M$ is such a model. $M$ is defined to be $L_{\delta}$ (the $\delta$-th level of constructible hierarchy) where $\delta$ is least such that $L_{\delta}$ models ZFC. Assuming that there are standard models of ZFC, the minimal model exists.
Yes.
Perhaps slightly surprisingly, every pointwise definable model of ZF satisfies the Axiom of Choice (because if every set is definable, then in particular it is ordinal definable, and V=HOD implies AC). Intuitively one might think to look to the AC to find a candidate for an undefinable set, but actually it is the opposite that is the case: If we're looking at a situation where AC fails, then there must be an undefinable set somewhere.