For just any first-order theory: What are the sets I am supposed/allowed to think of when thinking of models as sets (of something + additional structure)?
Provided:
I can think of models of any theory (other than set theory) as of sets from the (ZFC-based) von Neumann universe.
I can think of models of any theory as of sets of terms and formulas.
But what are the sets I am supposed/allowed to think of when thinking of models of (ZFC) set theory itself?
According to Godel's incompleteness theorem, ZFC cannot prove its own consistency. Therefore, it is relatively consistent with ZFC that there are not any set models of ZFC. In this case, there is still a proper class model of ZFC, namely the von Neumann universe, V, itself, among others (i.e. L, forcing extensions of V). However, the fact that V is a model of ZFC cannot be proven formally within ZFC. Indeed, truth in V cannot be defined in V due to a result of Tarski.
If we allow for some stronger axioms, then we can get set models of ZFC. For instance, if there exists an inaccessible cardinal, $\kappa$, then $V_\kappa$ is a set model of ZFC.
You're supposed to think of sets. Definitely.
Here's an analogy you might find helpful: let's use the name "ZFC-" for the axioms of ZFC but without the axiom of infinity. Now, if I suddenly decreed everything that isn't a member of $V_\omega$ is no longer a set, ZFC- would still be satisfied. That is, the members of $V_\omega$, taken as a collection, are a model of ZFC-.
If we wrap those members up into a set (which happens to be $V_\omega$ itself), that set is considered a model of ZFC-. Technically we also have to provide a relation (set of ordered pairs) that tells us what $\epsilon$ means, but if $\epsilon$ in the model means the same thing as $\epsilon$ in the "outer" set theory we can just mention that fact and proceed.
So, now that you know that $V_\omega$ is a model of ZFC-, perhaps you can imagine what a model of ZFC might look like. It's a really, really, really big set -- let's call it "M" -- such that all the sets inside it, taken together, are enough to satisfy the axioms of ZFC. But you don't need "M" itself to satisfy ZFC.
That's what a model of ZFC looks like.
This answer is going to be a bit too informal, but I hope it helps.
Imagine we have the collection of all sets. Let us call them the real sets, and their membership relation the real set membership. The empty set is "actually" empty, and the class of all ordinals is "actually" a proper class.
Now that we have the real sets we can use them as the "ontological substratum" upon which everything else will be built from. And this, of course, includes formal theories and their models.
A model of any first-order theory is then only a real set. This applies to your favorite set theory too. So the models of your set theory are only real sets (but the models don't know it, just as they don't know if their empty sets are actually empty or if their set membership is the real one).
This view fits well, for example, with the idea of moving from a transitive model to a generic extension of it or to one with a constructible universe: we are simply moving from a class of models to another one, each one consisting of real sets.
But this view also leaves us with too many entities, and maybe here we have an opportunity to apply Occam's razor. It looks like we have two kind of theories: one for the real sets, which is made of things that are not sets (we can formalize our informal talk about them, but that does not make essentially any difference), another one for the models of set theory, which is made of sets.
The real sets and the theory of the real sets belong to a world where there are real sets, but there are also pigs and cows, and human languages and many other things. We don't need all that to do mathematics, do we? So why not diving into the wold of the real sets and ignore everything else?
If this story sounds too platonistic, I am sure it must have a formalistic counterpart.
With my question:
How to think like a set (or a model) theorist.
I expected to obtain an official view about all this stuff. I somehow succeeded on this, but as you can see, I'm still working on it.
Here is a related answer to a related question which I also find useful:
From comment: how do we get from "the abstract" to "the concrete"?
In my partly informed opinion, not by formal model theory! The ability of set theory to describe its own models is one of the pillars of its success in the foundations of mathematics, but while its model theory helps us to understand the structure of set theory, it mostly doesn't help us understand what believing in the axioms of set theory commits us to.
I think Goedel's constructible universe helps us do that, particularly since it helps us understand the cumulative hierarchy. Fränkel-Mostowski models do too: permutability of urelements cast useful light on what's at stake with the axiom of choice. But while these two results are model-theoretic, they don't have much to do with the current direction on modelling set theory in itself.
We get more insight from looking at set theory from below: what is lost with weaker set theories like KP, IZF, and CZF? This gives me more feeling of getting at the concrete commitments made by set theory.
Suppose You start with something easier. Lets start with Peano Arithmetic. It is defined by some certain set of axioms, and definitely it does not say anything about numbers at least from formal point of view! It only says about some "hypothetical objects" for which several operations is defined, for example successor of existing object. In fact, objects which obeys PA axioms may not be a numbers at all ( numbers as we use of course) and it is a matter of taste, from that point of view, if we say: if some structure obeys PA axioms we should call it natural numbers.
That is the matter of model theory: every structure in which PA axioms are satisfied is called the model of Peano Arithmetic, and among them, natural numbers are some kind of natural and intuitive model for PA axioms.
Now lets start with ZFC. ZFC has its own axiom set called Zermelo-Frankel axioms. In fact from conservative and educational point of view everything is ok, relation $x \in y$ has meaning "x is element of y" but when You want to say something about models of ZFC definitely You should drop that way of description. The much proper way would be to use some abstract symbol for this relation, say $xRy$, forgive the meaning "x is element of y" but use "x is in relation with y" instead. So $R$ is abstract binary relation used in ZFC axiom set!
Then You may look for structures which satisfies ZFC axioms, in pure formal sense. And of course, normal universe of sets satisfy it, so it is candidate for model of ZFC theory, beside fact that there is problem with Cantor paradox which destroys such structure ( "class od sets") from being the proper ZFC model....
What a luck! If set theory could be the proper model of ZFC, then it would be inconsistent, as for set theory( based on Tim Chow's article "A Beginner's Guide to Forcing")
"by a result known as the completeness theorem, the statement that ZFC has any models at all is equivalent to the statement that ZFC is consistent "
So if it had happened we may prove completes of ZFC inside ZFC which naturally lead us to inconsistency...
So objects You refer as "sets" in Your question are "near model" of ZFC theory which states about objects which obeys ZFC axioms in term of binary relation $R$. If You find other "universes" satisfying ZFC axioms, You may call them "sets". But in fact it relation to ZFC is exactly the same as between objects from nonstandard models of Peano Arithmetic and natural numbers, or as between non-isomorphic objects satisfying group theory axioms ( models of group theory axioms), that is nonisomorfic groups and so on.
