Here, Noah Schweber writes the following:
Most mathematics is not done in ZFC. Most mathematics, in fact, isn't done axiomatically at all: rather, we simply use propositions which seem "intuitively obvious" without comment. This is true even when it looks like we're being rigorous: for example, when we formally define the real numbers in a real analysis class (by Cauchy sequences, Dedekind cuts, or however), we (usually) don't set forth a list of axioms of set theory which we're using to do this. The reason is, that the facts about sets which we need seem to be utterly tame: for example, that the intersection of two sets is again a set.
A similar view is expressed by Professor Andrej Bauer in his answer to the question about the justification of the use of the concept of set in model theory (here is the link, I can really recommend reading this answer). See also this answer. There he writes:
"Most mathematicians accept as given the ZFC (or at least ZF) axioms for sets." This is what mathematicians say, but most cannot even tell you what ZFC is. Mathematicians work at a more intuitive and informal manner.
Now we know that in ordinary mathematics (including model theory), one uses informal set theory. But what about set theory itself?
So now I wonder: When set-theorists talk about models of ZFC, are they using an informal set theory as their meta-theory? Is the purpose of ZFC to be used by set-theorists as a framework in which they reason about sets or is the purpose of ZFC to give a object theory so that we can ge an exact definition of what a "set-theoretic universe" is (namely, it is a model of ZFC)?
Best Answer
The main fact is that a very weak meta-theory typically suffices, for theorems about models of set theory. Indeed, for almost all of the meta-mathematical results in set theory with which I am familiar, using only PA or considerably less in the meta-theory is more than sufficient.
Consider a typical forcing argument. Even though set theorists consider ZFC plus large cardinals, supercompact cardinals and extendible cardinals and more — very strong object theories — they need very little in the meta-theory to undertake the relative consistency proofs they have in mind. To show for example that the consistency of ZFC plus a supercompact cardinal implies the consistency of ZFC plus PFA, there is a forcing argument involved, the Baumgartner forcing. But the meta-theory does not need to undertake the forcing itself, but only to prove that forcing over an already-given model of ZFC plus a supercompact cardinal works as described. And that can be proved in a very weak theory such as PA or even much weaker.
So we don't really even use set theory in the meta-theory but just some weak arithmetic theory. I expect that the proof theorists can likely tell you much weaker theories than PA that suffice for the meta-theory of most set-theoretic meta-mathematical arguments.