Has anyone ever really constructed a countable model of set theory that falls in the trap of the Skolem's Paradox? [closed]

Question

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:

1. its universe is computably enumerable (or at least decidable);
2. the relations (as sets) in this model are also computably enumerable (or at least decidable);
3. 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.

Answer 1

Countable models of ZFC are extremely far away from being computable. To see this, consider any Turing degree whose existence is provable in ZFC, by which I mean that we have a ZFC definition of a representative of that Turing degree. For example, the Halting problem is one (but there are far, far more complicated ones).

Our countable model of ZFC (which we externally view as being coded over natural numbers) contains an element it considers the natural numbers, and it contains an element it considers to be the representative mentioned above (eg the Halting problem). If we can enumerate the elements of the model, and decide the membership-predicate of the model, these two elements let us decide which natural numbers belong to our non-computable set.

So that attempt to get a more hands-on understanding of how a countable model can consider stuff to uncountable is doomed to failure. However, you can look at weaker theories than ZFC. One example would be the subsystem RCA_0 of second order arithmetic. This system is strong enough to state and prove Cantor's diagonalization argument for the real numbers. However, taking all natural numbers as first-order part together with all computable sets of natural numbers as second-order part gives us a concrete countable model of RCA_0.

What is going on here that is that what this model tells us when it says "The reals are uncountable." is from our external perspective just "There is no computable enumeration of all computable real numbers.".