4 deleted 45 characters in body

I totally agree with the answers already given but I still want to say something to your question, which emphasizes probably the formalist side. To cut a long story short the foundation of model theory, for which you were asking for, is ZFC (at least ZFC is one possibility), but this doesn't mean that one must not use model theory to investigate ZFC itself. This might look circular but is in fact not:

As you know, one can code the symbols of first order logic within set theory and, as a consequence, the whole model theory can be carried out in ZFC. Thus the Löwenheim-Skolem Theorem, the Compactness Theorem and so on are theorems of ZFC. (Note that when e.g. the Compactness Theorem talks about a “set of first order formulas”, it in fact talks about the set of the coded formulas, i.e. about a set of sets).

Now you can apply these results of model-theory to the coded axioms of ZFC (there is nothing wrong with that since ZFC is stated in first order logic and the set of the coded axioms is well defined); still everything is done in the frame ZFC.

The Theorem from logic, which states that if $T$ is a 'set' of formulas, $\psi$ another formula and $M$ a model such that $M \models T$ and $M \models \lnot \psi$, then T cannot prove $\psi$, is a theorem in ZFC (again $\psi$ and $T$ in this theorem are in fact coded, i.e. sets and moreover the metamathematical statement “there exits no proof from $T$ for $\psi$” is in fact a well defined statement about sets which mimics characteristics from proofs inside ZFC).

And this Theorem can now be used to state independence results about ZFC in ZFC. The only difficulty is that by Gödels celebrated result, one cannot prove inside ZFC the existence of a model of ZFC. Therefore one always assumes $Con(ZFC)$, i.e. the coded form of the assertion: “ZFC is consistent”, which is equivalent to “there exists a model of ZFC”. Then manipulate this given model to obtain a model for $ZFC+ { \varphi }$ where $\varphi$ is an arbitrary interesting statement.

We can now prove things like: If ZFC is consistent then so is ZFC+ “Continuum Hypothesis fails” which is the famous result of Cohen shown by models but within ZFC.

3 added 260 characters in body

I totally agree with the answers already given but I still want to say something to your question, which emphasizes probably the formalist side. To cut a long story short the foundation of model theory, for which you were asking for, is ZFC (at least ZFC is one possibility), but this doesn't mean that one must not use model theory to investigate ZFC itself. This might look circular but is in fact not:

As you know, one can code the symbols of first order logic within set theory and, as a consequence, the whole model theory can be carried out in ZFC. Thus the Löwenheim-Skolem Theorem, the Compactness Theorem and so on are theorems of ZFC. (Note that when e.g. the Compactness Theorem talks about a “set of first order formulas”, it in fact talks about the set of the coded formulas, i.e. about a set of sets).

Now you can apply these results of model-theory to the coded axioms of ZFC (there is nothing wrong with that since ZFC is stated in first order logic and the set of the coded axioms is well defined); still everything is done in the frame ZFC.

The Theorem from logic, which states that if $T$ is a 'set' of formulas, $\psi$ another formula and $M$ a model such that $M \models T$ and $M \models \lnot \psi$, then T cannot prove $\psi$, is a theorem in ZFC (again $\psi$ and $T$ in this theorem are in fact coded, i.e. sets and moreover the metamathematical statement “there exits no proof from $T$ for $\psi$” is in fact a well defined statement about sets which mimics characteristics from proofs inside ZFC).

And this Theorem can now be used to state independence results about ZFC in ZFC. The only difficulty is that by Gödels celebrated result, one cannot prove inside ZFC the existence of a model of ZFC. Therefore one always assumes $Con(ZFC)$, i.e. the coded form of the assertion: “ZFC is consistent”, which is equivalent to “there exists a model of ZFC”. Then manipulate this given model to obtain a model for $ZFC+ { \varphi }$ where $\varphi$ is an arbitrary interesting statement.

We can now prove things like: If ZFC is consistent then so is ZFC+ “Continuum Hypothesis fails” which is the famous result of Cohen shown by models but within ZFC.

2 edited body

I totally agree with the answers already given but I still want to say something to your question, which emphasizes probably the formalist side:

As you know, one can code the symbols of first order logic within set theory and, as a consequence, the whole model theory can be carried out in ZFC. Thus the Löwenheim-Skolem Theorem, the Compactness Theorem and so on are theorems of ZFC. (Note that when e.g. the Compactness Theorem talks about a “set of first order formulas”, it in fact talks about the set of the coded formulas, i.e. about a set of sets).

Now you can apply these results of model-theory to the coded axioms of ZFC (there is nothing wrong with that since ZFC is stated in first order logic and the set of the coded axioms is well defined); still everything is done in the frame ZFC.

The Theorem from logic, which states that if $T$ is a 'set' of formulas, $\psi$ another formula and $M$ a model such that $M \models T$ and $M \models \lnot \psi$, then T cannot prove $\psi$, is a theorem in ZFC (again $\psi$ and $T$ in this theorem are in fact coded, i.e. sets and moreover the metamathematical statement “there exits no prove proof from $T$ for $\psi$” is in fact a well defined statement about sets which mimics characteristics from proofs inside ZFC).

And this Theorem can now be used to state independence results about ZFC in ZFC. The only difficulty is that by Gödels celebrated result, one cannot prove inside ZFC the existence of a model of ZFC. Therefore one always assumes $Con(ZFC)$, i.e. the coded form of the assertion: “ZFC is consistent”, which is equivalent to “there exists a model of ZFC”. Then manipulate this given model to obtain a model for $ZFC+ { \varphi }$ where $\varphi$ is an arbitrary interesting statement.

We can now prove things like: If ZFC is consistent then so is ZFC+ “Continuum Hypothesis fails” which is the famous result of Cohen shown by models but within ZFC.

1