I've heard the claim that ZFC has a countable model in ZFC if ZFC is consistent. As far as I can tell, this is a straightforward consequence of Gödel's completeness theorem and the Löwenheim–Skolem theorem.
I'm curious, though, how careful one needs to be about bookkeeping details related to sets and proper classes when formulating the argument ... or if the issue just doesn't come up for an obvious reason that I'm missing.
So, my question is twofold
- Does the completeness theorem give us a model over a set anyway?
- If we pick a model over a proper class initially, can we use Löwenheim–Skolem?
When I nonstandardly say a model over X, I mean a model whose universe is X. I nonstandardly say a model in X when the fundamental set theory used to construct it is the set theory X.
ZFC is a first order theory with one relation symbol $\in$, by Gödel's completeness theorem it has a model. I'm not sure whether this theorem promises us the existence of a model over a set or if the promised model could be a model over a proper class instead.
Also, ZFC does not have any finite models, since $\emptyset, P(\emptyset), P(P(\emptyset)), \cdots$ are all distinct, where $P$ denotes the powerset.
Suppose for the sake of argument that we conclude that ZFC has a model over a proper class (using ZFC as the raw material for building the model). In that case, we interpret $\in$ as $\in$ in ZFC. So, we've built a trivial model, let's call it $M$. The universe of $M$ is the class of all sets in ZFC. It's possible that by applying the completeness theorem, we could have gotten a model over a set, which would make this problem go away. I'm not sure. Suppose we decided to pick $M$ as our model even if it's an inconvenient choice.
The second prong of the argument, as far as I can tell, is an application of the (downward) Löwenheim-Skolem theorem. The downward Löwenheim-Skolem theorem does not address the [proper class]-set boundary explicitly, so I'm wondering how the argument works. This question invokes Löwenheim-Skolem as an explanation for the existence of countable models.
In the proof of the Löwenheim-Skolem theorem sketched in the Wikipedia article, we use the axiom of choice repeatedly to select elements of the universe that have to be included in the new universe for the model we're constructing.
A strict reading of the axiom of choice promises nothing about the ability to make arbitrary choices over proper classes (and a choice function cannot have a proper class as a domain), so I'm not sure how to get from my trivial self-model of ZFC $M$ to any model whose universe is a set, let alone a countable set.