Background/Motivation
My framework is first order logic and ZF.
A uniquely definable set is one uniquely satisfying a predicate, for instance, the empty set is uniquely defined by the unary predicate $∀y.(y \notin x)$.
When reading about internal set theory (IST), I learnt that
- every uniquely definable set is standard
- every infinite set contains a non-standard element
I can conclude that every infinite set must have an element that is not uniquely definable. Since IST is a conservative extension of ZF, I would expect the same to be true in ZF. Sadly, I didn't find any sources on this. And since the predicate ‘‘uniquely definable’’ cannot really be formulated in ZF, I do not really know how to go about proving this.
Question
Does every infinite set have an element that is not uniquely definable in ZF, and how can I prove this?
Welcome to Math.SE!
I. The assertion that every set uniquely definable by a ZF-formula is standard in IST (which you pithily, but possibly even more confusingly, summarize as "every uniquely definable set is standard") is a convenient informal summary of the following fact about IST:
In your reasoning, you pretend that this fact is an actual implication saying "if the set $x$ is uniquely definable then it's standard" inside IST. Then you pretend that you can take the contrapositive of this implication to get that "if the set $x$ is non-standard then it's not uniquely definable". You then combine this with "every infinite set contains a non-standard element" (which, unlike the previous assertion, is a genuine theorem of IST) to get the fake conclusion that "every infinite set contains an element that is not uniquely definable".
But you cannot conclude that every infinite set must have an element that is not uniquely definable, since the highlighted fact above is not in fact an implication of the form $$\forall x. \mathrm{uniquely\_definable}(x) \rightarrow st(x)$$ and therefore does not have a contrapositive asserting that nonstandard elements are not uniquely definable. The issue is not that the predicate "uniquely definable" cannot be formulated in ZF: it's that you never had such a predicate at all. Not in ZF, not in IST. The phrase every set uniquely definable by a ZF-formula is standard in IST abbreviated something different.
That should answer your question.
II. That said, set theorists sometimes talk about so-called pointwise definability, which might seem related to the "unique definability" used above. For the sake of completeness, I'll briefly explain this notion here.
When you have a model $(V,\in_V)$ of ZF set theory, it makes sense to talk about pointwise definability of elements of the model: $a \in \mathcal{V}$ is defined by a ZF-formula $\varphi(x)$ if and only if $a$ is the only element of $\mathcal{V}$ that satisfies the formula $\varphi(x)$ when we interpret quantifiers in the formula $\varphi(x)$ as ranging over the set $V$, and occurrences of the symbol $\in$ in the formula $\varphi$ as the relation $\in_V$.
Given a model $(V,\in_V)$ of ZF set theory, the element $a \in V$ is pointwise definable by the ZF-formula $\forall y. \neg (y \in x)$ if and only if $\forall y \in V. \neg (y \in_V a)$ and $\forall x \in V. (\forall y \in V. \neg (y \in_V x)) \rightarrow x = a$ both hold.
Pointwise definability is a property that an element of a model of ZF set theory may have, and not a property that a ZF-set (as in, a set whose existence you prove using the ZF axioms) may have! It depends strongly on the model. E.g. in some models of set theory, the formula "$x$ is the set of all non-principal ultrafilters on $\mathbb{N}$" and the formula "$x$ has no elements" ($\forall y. \neg (y \in x)$) happen to pointwise define the same unique element $a \in \mathcal{V}$. In other models (such as models of ZFC) they don't.
This means that while pointwise definability might seem related at first glance to the "unique definability" posited above, it actually acts in a very different manner: it's only a relationship between elements of a model and ZF-formulas, and we can't talk about a given set being pointwise definable. We can talk about an element of a model being pointwise definable, but that requires fixing a model first.
A pointwise definable model of set theory is a model in which every element of the model is definable without parameters by some ZF-formula. It is a non-trivial result that such models can exist, in the sense that if some extension of ZFC set theory proves the consistency of ZF, then it also proves the existence of a pointwise definable model of ZF. If you want to learn more about such models, Hamkins' talks about the math tea argument provide a good starting point, but I should emphasize that none of the theory about pointwise definability is relevant to working in IST at all.