Meta Theory when studying Set Theory What exactly serves as the meta theory in the study of set theory (for example in Kunen's text). It seems to involve a certain amount of number theory and a certain concept of what it means to be finite. 
Also: We usually use $\bigcup_{\alpha\in{ON}}R_{\alpha}$ as our set theortic universe $V$ (in the sense we believe that all sets we are interested in live there) where $R_{0}=\emptyset$, $R_{\alpha+1}= \mathcal{P}(R_{\alpha})$ and $R_{\alpha}=\bigcup_{\beta<\alpha}R_{\beta}$ when $\alpha$ is a limit ordinal. The study of independence results then seem to be based on relatavizing notions with this $V$ as our set theoretic universe. It seems that it is implicitly assumed that the $\omega$ in $V$ has no non-standard elemements (in the sense that there is no $n>a$ in $\omega$ where $a$ is obtained be repeatedly applying the successor operation to $0$.) Is this true and can it be formalized or is it something that is taken for granted? 
e.g. If the above were true then $ZFC\vdash{\neg{Con(\ulcorner{ZFC}\urcorner)}}$ would imply that $ZFC$ is inconsistent since we may look at the $ZFC$ axioms $\phi_{1},...,\phi_{n}\vdash\neg{Con\ulcorner{ZFC}\urcorner}$, then look at a ctm these axioms (which exists by reflection and downward Lowenheim Skolem) and recover the proof of the contradiction.
 A: There are generally two accepted approaches:

*

*You can use some arithmetical theory, e.g. $\sf PA$, or even a fragment which is sufficient to develop first-order logic and syntactic manipulation of proofs. Then one can define the language of set theory, write the axioms and proofs and so on. In fact $\rm Con(\sf ZFC)$ is in fact a statement about natural numbers rather than a statement about sets and models.
This is even true if one wants to introduce forcing. And I ran into a recent masters thesis in which this (usually folklore, I believe?) result is given in details.


*You can use $\sf ZFC$ itself. Then you have some universe of set theory (usually $\sf ZFC+\rm Con(\sf ZFC)$ and even more), but you are in fact working inside a set model of set theory within that universe. In that case you are free to use all sort of fun model theoretical tools, and forcing is done directly and so on.
However in many many instances we in fact omit the meta theory, and we just care about it sufficient to develop first-order logic. We often work within the universe. So there is no real model of set theory, there is a universe and we work with that. We can do forcing using the universe because we can define Boolean-valued models and prove independence results using that, and so on.
Let me quote from a Ph.D. thesis written by VanLiere,

Since these questions all have to do with first-order provability, we could take as our metatheory some very weak theory (such as Peano arithmetic) which is sufficient for formalizing first-order logic. However, as is customary in treatises about set theory, we take as our metatheory $\sf ZF$ plus the Axiom of choice in order to have at our disposal the infinitary tools of model theory.  We will also use locutions such as ... which are only really justifiable in some even stronger metatheory with the understanding that they could be eliminated through the use of Boolean-valued models or some other device.

This sums up quite nicely, I think, the very utilitarian approach to set theory. We really just need a weak theory sufficient for first-order logic, but it's easier and nicer to work with much stronger metatheories because they make our life so much easier.

About the second part, we often take the universe to have the same integers as the metatheory. This has some serious implications, e.g. the validity of $\rm Con(\sf ZFC)$ is inherited from the meta-theory. This is not always the case, and sometimes it is worth looking at non-standard models, or even models which do not agree on the integers with the universe or with the metatheory.
However whenever you see the term "transitive model" then you immediately know that the model and the universe agree on the integers, which has some strong implications on the truth values of some statements in the model. This is why arguing about transitive model is not enough to invoke the completeness theorem and have provability; but it is enough to establish independence.
This is again a utilitarian point. Transitive models are nice, and they have very nice properties that they inherit from the universe. When we are interested in independence, then working with transitive models is generally enough. So we do that, because we are utilitarians.
I should probably add another thing about utilitarianism here. Of course one can make all sort of crazy assumptions "because they would make life easier", but philosophically one is likely to agree that the consistency of $\sf ZFC$ is true if one is interested in investigating $\sf ZFC$ and its consequences, and so it's reasonable to add this assumptions to your list of axioms in the metatheory, and even more. Even if you end up working just with $\sf ZFC$ itself.
As the quote points out, some assumptions that we often use can only be justified by much stronger theories, but they are "philosophically sound" (i.e. working with $\sf ZFC+\lnot\rm Con(\sf ZFC)$ as a metatheory for investigating $\sf ZFC$ is really weird), and we can remove these extraneous assumptions by using slightly more complicated devices anyway.
