ZFC or NBG set theory have a countable model by Löwenheim-Skolem. But I never found an example of one with real tangible sets. Of course I do not look for a consistency proof.
I am seeking to see how countably many objects can span an uncountable universe.
I fancy myself to came across such a countable model of NBG (lets call it $\mathcal{D}$) and want to know, whether something similar is already well known.
This is the idea:
- Take enough axioms of NBG $\Delta=\{ext, set, pair, inf, union, power, subst, reg\}$
- Build equivalence classes of the formulars of NBG language with one free parameter. $\varphi \equiv \psi \leftrightarrow \Delta \models \forall x \varphi(x) = \psi(x)$
- Make these equivalence classes $[\varphi]$ the objects of the domain.
- Ext would read $\Delta \models (\forall x \;x \in [\varphi] \leftrightarrow \mathcal{M}(x) \land \varphi(x))$ with $\mathcal{M}(x)$ being the unary relation 'x is a set'
I do not understand yet, why incompleteness is an issue. If $\varphi \equiv \psi$ is logically independent it means, that for two classes A,B A=B is independent. But this is similar to CH.
A few more examples:
$\emptyset = [ x \neq x]$
$\varphi_\omega:=\forall v \big(\emptyset \in v \land \forall u \big( (u \in v) \rightarrow (u \cup \{u\}) \in v \big) \, \big)\rightarrow x \in v $
$\omega = [\varphi_\omega]$
Inf reads: $\mathcal{M}(\omega)\land \omega \neq \emptyset$
Because of Reg: $[x \in x] \equiv \emptyset$
If I did not make a mortifying mistake this gives a nice countable model of NBG-AC. And no: neither $\epsilon$ nor $\mathcal{M}(x)$ are decidable.
The model is also canonically embedded as a submodel into any model of NBG, but it is not transitive.
If you are interested you can find the painstaking proofs here: A countable Model of Set theory
There's a pretty good reason that no "easily-visualizable" model of $\mathsf{ZFC}$ exists: since (we hope) $\mathsf{ZFC}$ captures at least "core mathematical reasoning," a truly simple process for building a model of $\mathsf{ZFC}$ would itself be something that could be carried out and verified in $\mathsf{ZFC}$, and this would contradict Godel's second incompleteness theorem (see also Jech's proof for finitely-axiomatizable set theories - while $\mathsf{ZFC}$ isn't finitely axiomatizable it has a conservative extension which is, namely $\mathsf{NBG}$, so Jech's argument still applies).
Put another way, if we did have a "simple" model of $\mathsf{ZFC}$ at hand, that would be good evidence that $\mathsf{ZFC}$ is not enough to capture as much of mathematics as we want it to.
Of course, the above is subjective. Here are some concrete observations:
No model of $\mathsf{ZFC}$ is computable (as noted in the comments above). On the other hand, looking at computability-theoretic complexity is extremely coarse: since $\mathsf{ZFC}$ is a computable theory, building a model of $\mathsf{ZFC}$ is no harder than building a nonstandard model of $\mathsf{PA}$, and in particular is strictly simpler than the halting problem (see this survey of Diamondstone/Dzhafarov/Soare on PA-degrees for more on this).
Admittedly, the low-complexity models constructed in the previous bulletpoint are extremely odd in many ways. For example, they are not even $\omega$-models (= their versions of the natural numbers are not isomorphic to the actual natural numbers). Indeed, if $M$ is a countable $\omega$-model of $\mathsf{ZFC}$ then $M$ computes every hyperarithmetic set; on the other hand, the Gandy Basis Theorem (a more technical analogue of the Low Basis Theorem used implicitly in the previous bulletpoint) says that we can find such an $M$ which is still much simpler than the "higher analogue" of the halting problem.
Those models are still wild, though, in that they are ill-founded. What if we want a well-founded countable model of $\mathsf{ZFC}$? Well, here the picture sharpens considerably: assuming of course that such a model exists in the first place, there is a simplest such model in two senses: there is a unique-up-to-unique-isomorphism $W$ with the properties that
$W\models\mathsf{ZFC}$ and is well-founded;
for every well-founded $A\models\mathsf{ZFC}$ there is a unique $\Delta_0$-elementary embedding of $W$ into $A$; and
given any countable well-founded $A\models\mathsf{ZFC}$, we can compute $W$ from $A$.
Incidentally, this $W$ is just "The first level of the $L$-hierarchy satisfying $\mathsf{ZFC}$, if such exists."