I'm trying to understand Skolem's paradox, and also some related ideas about definable numbers. I'm pretty new to learning about model theory. I'll lay out what I think I'm understanding, and maybe you all can let me know if I've got it wrong.
Skolem's paradox is basically that there are countable models of first-order set theory which can model uncountable sets. To make what follows a little more specific, let's say $M$ is a countable, transitive model of $ZFC$.
So, in the domain of $M$ we can have some $r$ which models the reals, and some $n$ which models the natural numbers. For any countable set $x$ definable in $ZFC$, there is an isomorphism from that set to the natural numbers. For $M$ to model "$x$ is countable" there must then be an isomorphism (in $M$) from some $x'$ to $n$, where $x'$ models $x$. Conversely, in order to model "the Reals are uncountable", there must not be an isomorphism in $M$ between $r$ and $n$. Nevertheless, from our perspective external to $M$ we can say that $r$ is countable, because the entirety of $M$ is countable. Skolem's paradox is resolved by realizing that the definition of countability that exists within $M$ is not the same as this external definition. $M$ has to provide correct first-order statements about countable sets in $ZFC$, but it doesn't need to provide correct (from the external viewpoint) statements about the elements of $M$ itself.
Correct so far?
Now, from the external perspective we can say that $r$ contains far fewer elements than the reals, since $r$ is countable and the reals are uncountable. But this isn't a problem because $M$ can't see that it's missing some elements of the reals. Nevertheless, for any $y$ that can be defined and proven to be real in $ZFC$, $M$ should model "$y$ is an element of the reals". But $M$ can only do this for countably many choices of $y$. So, it seems that if we could define a large enough set of reals (uncountably many, in fact), then we would run out of space in $M$ to contain all such statements. Luckily, we can only define at most countably many reals. So, we are able to avoid Skolem's paradox here (i.e., avoid an actual contradiction) only because most of the reals (all but countably many) are undefinable. Is that correct?
Related to this, in this MathOverflow answer (https://mathoverflow.net/a/44129) it's pointed out that there are models of $ZFC$, including countable, transitive models of $ZFC$, for which all the reals are definable. If what I wrote above is correct, then perhaps similarly here one could say that (from an external perspective) these models exclude uncountably many of the reals, but because the excluded reals are themselves undefinable, there's no way for the model to know they are missing -- so internally it can say it includes all the reals. Is that an accurate statement?
I suppose one issue with the above statements is that it may not be possible to define precisely which reals are "definable". But maybe that's OK (as far as the above statements are concerned) so long as we can still say that "uncountably many undefinable reals must exist", and that (from the external perspective) all the reals "missing" from $r$ must be in this set of undefinable reals.
