Is the use of the meta-meta-theory allowed in proving an independence result?

Question

I am wondering about the use of a meta-meta-theory in proving statements of the form "$\phi$ is independent of $\mathcal{T}$" in mathematical logic.

Short question: Is using a result from the meta-meta-theory, for example a nonstandard model of the meta-theory, allowed in proving/disproving the independence of a result in the theory itself?

Long question:

Assume for the sake of this post that we are working in the framework of model theory, and that we are using ZFC to develop all of the ideas (languages, structures, theories, and so on). Call this meta-theory mZFC (distinguished from the theory of ZFC which is a formal set of statements in mZFC). Consider the question of whether ZFC proves the continuum hypothesis, i.e. $$ \text{Does } ZFC \vDash CH ? \;\; \text{Does } ZFC \vDash \lnot CH ? $$ My understanding (which could be incorrect) is that we can construct specific models of $ZFC$ in $mZFC$, call them $M$ and $M'$, such that $M, M' \vDash ZFC$, but $M \vDash CH$ and $M' \vDash \lnot CH$, showing that the above statements are both false, i.e. that CH is independent of ZFC.

Now, it seems that since we have shown $CH$ to be independent of $ZFC$, that in future work we could reasonably assume that the meta-theory $mZFC$ satsifies (or does not satisfy) $mCH$ (since models of the meta-theory exist either way). For instance, hypothetically we could prove the independence of some other sentence $\phi$ from $ZFC$ by constructing models $N, N' \vDash ZFC$ which do and do not satisfy $\phi$--but whose existence depends on $mCH$! Specifically, I am imagining a situation where we deliberately construct a model $N$ such that $\aleph_0 < |N| < 2^{\aleph_0}$.

Would such a construction be considered a valid proof that $\phi$ is independent of $ZFC$, or would it be considered a proof of some other (more meta) result? If the former, is there a standard way to distinguish exactly how many levels of meta were used in an independence result--or is multiple meta levels equivalent to just one?

I hope my question is not too confusing! Thanks.

Answer 1

Yes, in principle you could prove a result of the form "If CH holds then theorem T is independent of system S". Here we assume CH in the meta-theory.

There is a limitation on the utility of this method, though. Shoenfield's absoluteness theorem shows that $\Sigma^1_2$ sentences are absolute between $V$ and $L$ in set theory. If $S$ is an effective system, a statement of the form "$T$ is independent of $S$" is much less than $\Sigma^1_2$. So, if such a statement holds at all, it holds in $L$, where CH always holds. Therefore, if we could prove "If CH holds then theorem $T$ is independent of system $S$", we could actually just prove "$T$ is independent of system $S$", because the latter statement is absolute to $L$ and $L$ satisfies $CH$.

So the method does not help when the metatheoretic principle in question is CH. But the method can work for some stronger properties that are not absolute to $L$, such as large cardinal properties.

There are easy examples of this. For example, if we assume in the metatheory that there is a model of ZFC + "there is a Woodin cardinal" (the existence of such a model is not provable in ZFC), then we can prove in the metatheory that Con(ZFC + "there is a Woodin cardinal") is independent of ZFC. But, unless we assume the consistency of ZFC + "there is a Woodin cardinal" in the metatheory, then for all we know the metatheory might believe that theory is inconsistent, in which case the metatheory will not prove that Con(ZFC + "there is a Woodin cardinal") is independent of ZFC.

It is necessary to be careful with terminology, though. The metatheory we work in defines what it means to be "standard". So it is hard to see what a "nonstandard model of the metatheory" should really be. Perhaps you could imagine a "meta-metatheory", but in that case you should really take the "meta-metatheory" as your metatheory and the "metatheory" as your object theory. Or, as I do above, you can just take additional axioms in the metatheory, which is equivalent to adding additional hypotheses to theorems you prove in the metatheory.