keeping track of proper classes vs sets when showing ZFC has a countable model (assuming ZFC is consistent) 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.
 A: 
Does the completeness theorem give us a model over a set anyway?

Yes.  The completeness theorem says that every consistent theory has a model, and in this context, "model" is defined to mean a model over a set.

If we pick a model over a proper class initially, can we use Löwenheim–Skolem?

This is a subtle issue--what does it even mean to have a model over a proper class?  The issue is that the usual recursive definition of what it means for a structure to satisfy a formula does not work when your structure is a proper class.  So, if you have a structure $(M,\epsilon)$ where $M$ is a proper class, you cannot even state $(M,\epsilon)\models ZFC$ in the language of ZFC.
However, for any individual sentence $\varphi$, you can state $(M,\epsilon)\models \varphi$, by carrying out the recursive definition "by hand" in the specific case of $\varphi$.  So typically, when people talk about "class models", what they mean instead is that there is a theorem scheme which says that for each axiom $\varphi$ of ZFC, you can prove that $(M,\epsilon)\models\varphi$.  Alternatively, you could assume that your class model has the special property that you actually can define a formula satisfaction relation for it, but this is rarely actually true in practice.
As for carrying out a Löwenheim–Skolem argument for class models, you can do this as long as you can define satisfaction with respect to all the formulas you care about.  (This means you can carry it out as usual if your class model has a satisfaction relation, or if it doesn't, you can only carry it out to get a submodel that satisfies finitely many particular axioms of ZFC, rather than all of ZFC.)  The issue with the axiom of choice that you point out can be avoided using Scott's trick.  For instance, every time the proof of Löwenheim–Skolem would have you make a choice of an element with some property, instead of choosing just one element, you can pick all the elements with the desired property that have minimal rank.  There may be uncountably many such elements so this may not give you a countable model, but it will at least get you down to a set-sized model.  Then, you can use ordinary Löwenheim–Skolem to get down to a countable model.
Note that in this weak (theorem scheme) sense of "class model", you do not even need to assume that ZFC is consistent in order to get a class model of ZFC: $(V,\in)$ is a class model of ZFC.  The argument above then shows that for any finite subset of the axioms of ZFC, you can prove there is a (set) model of those axioms.  This is known as the reflection principle. (Crucially, though, this is a separate theorem for each finite set of axioms, rather than a single theorem with a quantified variable representing an arbitrary finite set of axioms.  As a result, you cannot combine it with compactness to conclude that ZFC is consistent.)
