Are results of relative consistency metatheorems?

Question

Suppose that $S, T$ are two theories in the language of set theory, and suppose I prove - using relativization of concepts, for example - that $\operatorname{Con}(S) \rightarrow \operatorname{Con}(T)$. This results seems to me, unless both theories are finite, to be a result in the metatheory, in the sense that it is impossible to prove that $\mathsf{ZF} \vdash \operatorname{Con}(S) \rightarrow \operatorname{Con}(T)$. It seems this way because, given a class model $\mathcal{M}$, $\mathcal{M} \vDash S$ is generally a statement that can't be formalized in $\mathsf{ZF}$. Does this sound right?

Answer 1

Yes. Consistency results are meta-theorems. They are not about implications of statements in the language, but rather about the properties of theories, which are objects of the meta-theory.

Now, in the comments you express some confusion about the meta-theory being $\sf PA$ or $\sf ZF$ or something else. In practice this does not matter. If you can interpret a theory $T$ in a theory $S$, then all proofs from $T$ can be translated as well. In particular, $\sf PA$ can be interpreted in $\sf ZF$, so whatever you can do in $\sf PA$ as a meta-theory, you can in fact do in $\sf ZF$. Actually, $\sf PA$ is far too strong for most of the things you want a meta-theory to do, and $\sf PRA$ (Primitive-Recursive Arithmetic) is actually enough.

But $\sf ZF$ offers us more. It offers us models and semantics, and Gödel's completeness theorem which tells us that $\operatorname{Con}(S)$ holds if and only if $S$ has a model. So it lets us play with objects, rather than with formulas and proofs. Because usually playing with objects is easier than playing with syntax. The important part is that $\sf ZF$ lets us take all the results we obtained semantically, and convert them back into something that was actually proved from $\sf PA$ or some subtheory thereof.

Of course, when you use $\sf ZF$ as your meta-theory for itself, you are not talking about class models, you are talking about set models. We go one step further down the rabbit hole. And that's fine.

Answer 2

Yes, they are metatheorems in the sense that they are theorems about formal systems. But notice there is a fuzzy line as to what to call a metatheorem. If $\phi$ is a sentence in the language of set theory and $\phi$ is a theorem of ZFC, then the (true) statement "$\mathsf{ZFC}\vdash \phi$" is a metatheorem that we prove in the metatheory, typically by producing and verifying a formal ZFC proof (well, what we actually do is give a natural language mathematical argument that is supposed to more-or-less clearly map to a formal ZFC proof). Typically when theorems are called out specifically as metatheorems, they are more complicated statements than $"\mathsf{ZFC}\vdash \phi$," so that it's important to take notice that we are doing something less trivial in the metatheory than simply verifying a proof.

$\mathrm{Con}(S)\to \mathrm{Con}(T)$ is one of these more complicated statements, where we actually have two distinct theories, and we're saying that if we can prove a contradiction from $T$ then we can from $S$ as well.

So yes, it's in the metatheory, but what's the metatheory? It's just the language we're using to study and prove things about the formal systems in question. We do this in natural language typically, but it can often be of interest to formalize the metatheory and ask questions like which axioms are needed to prove a given result about ZFC. To do this we need to code the ideas of formulas and proofs into some formal system, i.e. Godel encoding. (I won't say anything more on this since I see it was discussed in the comments.) Nothing precludes us from using ZFC to formalize the metatheory, although it is typically overkill for studying proofs in formal systems and weak theories of arithmetic suffice.

In particular, as Eric says in the comments, we can typically prove something like $\mathrm{Con}(S)\to \mathrm{Con}(T)$ in a system much weaker than ZF, so we can certainly prove it in ZF. Note that this is framable as an arithmetic statements about certain proof numbers existing, and ZF can talk about arithmetic through its natural numbers, so you can very readily express the statement in both systems (and thanks to ZF's greater expressiveness you have other more natural encoding options there too rather than just using numbers).

You are correct that $\mathcal M\models S$ and more generally the satisfaction relation $\mathcal M\models \phi$ cannot be expressed in ZFC for $M$ a proper class. I assume you have in mind demonstrating the premise of a theorem like "If for all $\phi\in S,$ ZFC can prove $\mathcal M\models \phi$ for some $\mathcal M$ (which is a proper class in this instance) then $\mathrm{Con}(\mathsf{ZFC}) \to \mathrm{Con}(S)$". But note the subtlety here... we aren't asked to show $\mathcal M\models \phi,$ we're asked to show that ZFC proves this. In other words that it holds in all (set!) models of ZFC. And the relativization of proper class to a set model is of course a set.