In an article named 'Skolem’s Paradox' on SEP, there is a description of the Paradox I'm asking about here:
Skolem's Paradox arises when we notice that the standard axioms of set theory can themselves be formulated as (countable) collection of first-order sentences. If these axioms have a model at all, therefore, then the Löwenheim-Skolem theorem ensures that they have a model with a countable domain. But this seems quite puzzling. How can the very axioms which prove Cantor's theorem on the existence of uncountable sets be satisfied by a model which is itself only countable? How can a countable model satisfy the first-order sentence which “says that” there are uncountably many things?
I wonder if anyone really has constructed a countable model of set theory that falls in the trap of the Skolem's Paradox. That is, they constructed a countable model of the usual first-order set theory, and proved that in that very model, there is an element x such that the existence of an injective function from x to the set of natural numbers N in the model can be denied in that theory (and hence, x is uncountable). Of course, how they verified that the x above is really an uncountable 'set' seen from the theory/model may be done differently (, different from the way I describe above).
Some may suggest that one can use the method in the proof of the skolem theorem to generate such a model. But that method is not really 'constructive' enough-- we don't know how the elements in the model behave. So, in the spirit of being 'constructive', such a model is more preferred:
- its universe is computably enumerable (or at least decidable);
- the relations (as sets) in this model are also computably enumerable (or at least decidable);
- the collection of the relations in this model is also computably enumerable (or at least decidable).
If all 3 of the above conditions can't be met in one single model, then a model satisfying as many of them as possible is preferred.