If a metatheory proves consistency of a theory, will consistency of the metatheory suffice? I'm going to call a metatheory reasonable if it's consistent and whenever there exists a proof for a sentence $\phi$ from a theory $T$ the metatheory proves $T\vdash \phi.$
Suppose that some reasonable metatheory proves the consistency of a theory $T$. Can we deduce that $T$ is consistent?
My informal argument for this idea goes as follows. Suppose $T$ were inconsistent. Then there would exist a proof of $\bot$ from $T$. Then the metatheory would prove $T\vdash \bot$. But since the metatheory proves $T$ is consistent, the metatheory also proves $T\not\vdash\bot.$ But then the metatheory must be inconsistent, a contradiction. Does this argument work?
 A: This will work as long as the metatheory is able to verify proofs in $T$. There are a couple ways this could fail to be the case, one silly and the other a bit less silly:

*

*Our metatheory could be insufficient to perform basic calculations (that is, not $\Sigma_1$-complete). In my opinion, to put it mildly, this is a sign of a bad metatheory.


*More interestingly, even if our metatheory is really really strong the theory $T$ could be presented to us as something other than an explicit computably axiomatized theory. For example, maybe we ask our metatheory about the status of the theory $T$ which is defined as "$\mathsf{PA}$ if $\mathsf{CH}$ holds, $\{\perp\}$ if $\mathsf{CH}$ fails." The consistency of $T$ now hinges on $\mathsf{CH}$; our metatheory could be wrong about the consistency of $T$ not by virtue of failing to have enough computing power or by seeing "false computations" but instead by being wrong about what $T$ is in the first place.
Morally, though, the idea that no reasonable metatheory can falsely believe a given theory to be consistent is accurate.
