Models of set theory

How can one talk of a semantics or model of set theory (lets say ZF or ZFC) when the definition of a structure (and potential model) needs a carrier set in the first place (by its definition)?

I already answered a similar question at length on MathOverflow so let me try a short answer, suitable for this forum.

You mistakenly assume that it is the business of model theory or logic to somehow "produce" set theory out of nothing. Logic and model theory are just two branches of ordinary mathematics -- they do not precede them, although they are a bit peculiar because their object of study is mathematics itself (its methods, its possiblities, its limitations). Therefore, model theorists and logicians are "allowed" to use all the usual tools of mathematics (numbers, sets, topological spaces, and so on).

When logicians speak of "foundations" of mathematics, they may give the impression that they are "building the cathedral" starting from its foundation. But it is much better to view what they are doing as a study of how the cathedral is built and how we can improve it. For instance, logicians have observed the fact that almost all of modern mathematics can be expressed in the language of set theory, but this does not mean that we need to "secure" set theory before the rest of mathematics can be done. History is my witness: geometry, algebra, and analysis existed before set theory and logic came along.

P.S. I will not deny that historically a primary objective of logic was in fact to secure foundations, especially the kind of logic that Bertrand Russell did in his Principia mathematica. However, at least since Gödel we have known that such an endeavor must fail. In any case, I am expressing here my personal view that attempts to secure absolute foundations of mathematics are a bit like attempts to prove there is god. Ultimately it comes down to an act of faith.

One can talk about $\sf ZFC$ in much weaker theories, like $\sf PRA$ or other fragments of arithmetic. These are sufficient to develop internally the basics rules of logic, and talk about axiom schemas and so on.

Then talking about models of $\sf ZFC$ is the same as talking about models of any other theory. Since $\sf ZFC$ is just a bunch of axioms, now defined internally as sets with certain properties, and a model of $\sf ZFC$ is just a set satisfying these axioms.

(And these don't exist in the meta-level of $\sf PRA$ or whatever, but models of group theory, ring theory or vector spaces don't exist in $\sf PRA$ either.

So if all that bothers you, ask yourself how we can talk about natural numbers before we have $\sf PRA$ and how we can talk about $\sf PRA$ before we have the natural numbers.)

As you may be aware, by the Godel Incompleteness Theorem, it can not be proved in, for example, $\mathsf{ZFC}$ that there are models of $\mathsf{ZFC}$, one usually assumes $\mathsf{ZFC}$ is consistent and result are usually states as "If there exists a model of $\mathsf{ZFC}$, then ...". Another way to think of this is (again assuming the consistency of $\mathsf{ZFC}$, one assumes that we are working in a single fixed model $V$ and studying all the models that that $V$ has.

Another possible approach for studying models of $\mathsf{ZFC}$ is work in an axiom system that implies the existence of models of $\sf{ZFC}$. The common approach to this is augmenting $\sf{ZFC}$ with large cardinal axioms such as the inaccessible, measurable, etc. Then there actually exists a set model of $\sf{ZFC}$ and possible much more.

Finally, another common approach is rather than study model of the full $\sf{ZFC}$, one can instead study $\{\in\}$-structures satisfying certain axioms and having certain properties (like transitivity). By the usual compactness argument in logic, one can get nice models for finite amount of $\text{ZFC}$. For those who are doing independence results in set theory, models of finite amount of $\sf{ZFC}$ is often sufficent (essentially due to the fact that proofs of theorems are finite). This is a common approach to models used in forcing.

It should also be noted that sometimes in proving independence result, one works with "models" that are not even sets at all. These are really proper classes (or you could think of them as just formulas). The common examples are the well-founded $\text{WF}$ and Constructible $L$. Although these are not sets, they are used to prove independence results through relativization.

I suggest reading the appropriate sections of Kunen's Set Theory for the various mathematical formal approach to handling models of set theory.