For example, in classical logic, because of the law of the excluded middle, all propositions must be true or false, so in order to prove that a proposition is actually independent of the theory, we need to use some metamathematical ideas. However, in intuitionistic logic, we can prove $\neg\neg p$, corresponding to the independence of the statement $p$, without having to use any metamathematical ideas.
Also, though I am just now learning about it, constructive type theories, with their reification of proofs as mathematical objects seems to me like it should be much deeper in metamathematical character. Moreover, this page claims Martin-Löf Type Theory was developed in the tradition of "metamathematical modeling".
In what sense do constructive type theories, or more generally, other theories like intuitionistic logic "model" metamathematical ideas? Is there some rigorous notion of (semi-) interpretability of metamathematical concepts in a theory?
Provability logic and Interpretability logic both use modal logic to study what a system can prove about its own metamathematical properties. According to this thesis it seems to be mainly focused on studying formal theories of arithmetic, though the Wikipedia article makes me think the theory is more general than that. Though, with some preliminary searching, I couldn't find any use of provability logic to deduce the "metamathematical awareness" of common foundational systems or logics themselves, so I would be interested in anyone could find some papers towards that direction of study.