I may not be understanding your question, but here goes:

In most cases (aside from some metamathematics of set theory itself) the metalanguage is implicitly understood to be ZFC. So Gödel's first incompleteness theorem while a metatheorem of arithmetic is a theorem proper of ZFC.

The idea behind Gödel's second incompleteness theorem (as an improvement in his first incompleteness theorem) is that arithmetic itself can be used as the metalanguage. Gödel coding allows you to represent formulas in any recursive language as natural numbers. This can be extended to code proofs as natural numbers. Many of the properties proofs you might want to talk about in your metatheory can be expressed as arithmetic (in fact, primitive recursive) properties of their corresponding Gödel codes. So for example, one can define a formula $\phi(x)$ in the language of arithmetic such that $\phi(n)$ is true if and only if $n$ is a Godel code of a *valid* proof in a given recursively-axiomatizable proof system. One can also prove (as theorems of some weak fragments of arithmetic) basic proof theoretic facts like:

"If $T \vdash \phi$ and $T \vdash \psi$, then $T \vdash \phi \wedge \psi$"

The choice of proof system doesn't so much matter, as proof systems tend to be entirely syntactic, and any recursive syntax can be interpreted in the natural numbers, with all syntactic operations and relations interpretable as arithmetically-definable functions and relations on natural numbers. One important observation is that our metatheory does not need to refer to or have access to the standard model $\mathbb{N}$ of arithmetic, because if $P(x)$ is a primitive recursive predicate, then the truth of $P(n)$ for any standard natural number will be the same in *any* model of arithmetic. This is the reason we can go as far down as PRA for Godel's incompleteness theorem.

It's also possible to compare two theories, entirely using arithmetic as your metalanguage, so long as those theories are recursively-axiomatizable. The idea is you represent a recursively-axiomatizable theory as a natural number which codes a primitive recursive function whose range is the set of Gödel codes of axioms of that theory.

Gödel's first incompleteness theorem requires more metatheory than the second incompleteness theorem, because the "punch" of the theorem (that this unprovable sentence G is *true* in the standard model of arithemtic) requires a metatheory which can recognize that G is in fact true. But the second incompleteness theorem does not require this, so arithemtic itself can be the metalanguage.

formalized proofs, which are simply natural numbers that satisfy special properties about their factorization. If you are looking for a system where a proof means "a proof as in real life", that is, a string of symbols of the logic you work inside, then how are you planning to refer to these proofs with the variable symbols of the logic they belong to without doing some kind of coding? How are you planning to quantify over proofs? $\endgroup$7more comments