I hope that this post isn't off topic, but I already asked math.stackexchange about first order formalizations of first order logic. There are provability logics, and extensions in modal logic's that seem to attempt to address this question, and model theory implies answering questions about metamathematics, but I'm looking for an explicitly first order theory that can be used to prove things about metamathematics.

Basically I'm wondering if there are first order formalizations of metamathematics. I'm interested in making proofs in first order logic about proof systems, such as the completeness and incompleteness theorems for first order theories in a fashion that is analogous to making a computer language compiler that can compile itself.

I understand that this probably should be possible, seeing it's generally agreed that you can represent most of mathematics in set theory, and represent set theory in first order logic, and I don't see any reason why encoding definitions about formal statements, provability, satisfiability, and other notions related to metamathematics would be unworkable.

There are formalizations of arithmetic both in the language of first order logic directly and in the language of set theory. Are there formalizations of metamathematical systems that I can use to make first order proofs about first order proofs similar to first order theories about arithmetic and set theory?