I know of Joel David Hamkins's analysis of the so-called "math tea argument", namely that there are undefinable real numbers. Supposedly, he debunked this argument by constructing a countable model of set theory where all sets and all real numbers are definable. However, I don't think he really did, because he merely constructed a countable model. Even though the model thinks that it is not countable, it is countable in reality. I still think there are undefinable real numbers, but now I also think that this fact can't be asserted in the formal theory of ZFC. In much the same way that no formal theory can define its own truth predicate, so also no formal theory can define its own definability predicate. But I am interested to know, what have other mathematicians thought about this topic?
Set Theory – Are There Undefinable Real Numbers?
model-theoryreal numbersreference-requestset-theory
Related Solutions
There are several problems here:
There is not "the standard model of set theory". There are notions of "standard models" (note the plural), but there is no "the standard model". With respect to the real numbers there are several possible scenarios:
It might be the case that there is a standard model containing all the reals. This model, if so, has to be uncountable.
It might be that every real is a real number of some standard model, but there is no standard model containing all the reals.
It might be that there are real numbers which cannot be members of any standard model, and some that can be.
It might be that there are no standard models at all.
So this is really a delicate issue here. But in any case, one shouldn't qualify "standard model of set theory" with "the". At all.
The notion of "definable real number" often means definable over $\Bbb R$ as a real number in a language augmented by all sort of things we are used to have in mathematics, integrals, sines and cosines, etc. In that case, there are generally only countably many definable reals, since there are only countably many formulas to define reals with.
Once you add the rest of the set theoretic universe into play, you can have that every real number is definable. This is a delicate issue, and known to be consistent, see Joel Hamkins, David Linetsky and Jonas Reitz's paper "Pointwise Definable Models of Set Theory" (and Joel Hamkins' blog post on the paper which has a nice discussion on the topic).
And this brings us to the problem at hand. It might be the case that the collection of all definable reals is not itself definable internally. Namely, we can recognize whether a real number is definable or not; but there is no formula whose content is "$x$ is a definable real number". This can be the case because we cannot match a real number to its definition, and we cannot really quantify over formulas to say "There exists a definition".
But sometimes we are in a case where we can in fact identify the definable real numbers, either we know that they form a set (which was defined using some other formula) or that we managed to circumvent the inability to match a real to its definition by adding further assumptions that make things like that possible. And in those cases the set of definable reals, the Wikipedia article states, is a subfield of $\Bbb R$ of that model of set theory.
The question is what do you mean by a "model of ZFC". If you mean the axioms as we enumerate them, in the meta-theory, this may or may not be the same thing as those of the universe of sets in which we are looking. The same can be told about the inference rules of FOL.
But since we can code everything into integers, that means that if we have a model whose integers are standard (read: agree with the meta-theory), then these problems go away.
What does that mean? Well, if the model was a model of ZFC, then it proves the completeness theorem, and since the arithmetic statement "ZFC is consistent" is true, that means that we can find a model of ZFC, and that it is the same ZFC as our meta-theory's one.
You might want to argue that the relation of that model might not be "correct" in some way, but we can make this model internally countable and the relation is then coded by a subset of $\omega$. So it's all good.
Best Answer
I suppose we need to consider some context here. ZFC is a first order theory over the language $\mathscr{L}=\{\in\}$. It interprets $\in$ as just some binary relational symbol (so if $M\models ZFC$ is a model of ZFC, then $\in$ will be interpreted as some relation $R\subseteq M^2$ (in other words $\in^M=R$)). Notice that firstly, the relation $\in$ in ZFC doesn't necceserily be interpreted as the "meta-$\in$" with a cut domain (to avoid ambiguities I will denote "meta-$\in$" as $\in'$). I.e it isn't neccerily the case that in a given model $M\models ZFC$ we have that the $\in^M=\{(m_1,m_2)\in M^2: m_1\in' m_2\}$.
Now I say it to make some clearness here. When you define things in ZFC you define everything in accordance to the relation $\in$ (which will be interpreted as $\in^M$ in some particular model $M$). In particular you define cardinality in accordance to $\in$, you define it with some first order formula over the language, and it doesn't have to correspond to the meta-cardinality. They are two distict things.
(If we will assume that there's a transitive ($\in^M$ is the same as $\in'$ just cut to the $M$ and $\in^M$ is transitive on $M$) then there is pointwise definiable model of $ZFC$ (as we see in this article by Hamkins https://arxiv.org/abs/1105.4597). So the analogy isn't perfect but still I think it might be helpful. Also still definition of cardinality etc. depends also on that what are you quantifying over so still it can be diffrent than the "meta version" ).
In a pointwise definiable model at the same time can prove that based on it's internal definition of what "two sets has distinct cardinalities" we can prove that reals and natural numbers have same diffrent cardinality, but also we can show that in a sense of "meta-cardinality" they are diffrent. It also shows why we can have definiable reals, because the concept of cardinality might differ.
We can't define definiability within a theory as you notice, and that's one of the reasons why we can have models where even every set is definiable. Formal theories oftenly have many limitations, the fact that we can have all sets definiable (in some models) shows that we also here have some limitations, that ZFC on it's own doesn't impede diffrences between what it thinks and what works in the metatheory (if all would work the same way then from the fact that there are countably many formulas, couldn't have all reals definiable).