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

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.

• What is $mCH{}$? Nov 11, 2015 at 9:02
• CH in the meta theory. It's made-up notation, maybe I should have clarified. Nov 11, 2015 at 9:03
• But CH is not a meta-theoretic statement. How do you interpret it? Nov 11, 2015 at 9:15
• @Wojowu CH is a meta-theoretic statement when the meta-theory is ZFC! By CH in the meta theory I just mean exactly the statement of CH in ZFC. I am only using mCH and mZFC to distinguish formal statements in the meta-theory ZFC from formal statements in the object-theory ZFC. Nov 11, 2015 at 10:11
• I don't understand why the construction of models of $\mathsf{ZFC}$ either satisfying (or refuting) a sentence $\phi$ depends on what metatheory satisfies the CH or not. ZFC is a first-order theory, and Löwenheim-Skolem theorem says that countable models are enough to check whether a sentence is independent of ZFC or not. Nov 11, 2015 at 12:04

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.