Is there any current development of a first order formalization of metamathematics? 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?
 A: Possibly, what I am currently doing can be considered as research in this direction, and I will share about it below.
First, what is metamathematics? I would treat this as a theory in a language which can serve as a metalanguage of the languages used in mathematics. In my article I introduced a language called metalingua intended to serve as one metalanguage common to different languages. Since then, I developed further this language, so that it now has only one symbol of a binary operation. I talk below about this language and its set theoretic interpretation, but first will  talk about my understanding of what is meaning (sense) in a natural language which is richer than any artificial language used by mathematicians.
I call meaning of a word the set of all things denoted by it ("referents of the word"). So, a noun denotes objects, a verb denotes actions, an adjective denotes qualities of objects, an  adverb denoted qualities of actions, etc. Thus, "meaning of a word" is a set. I treat punctuation signs as operators, i.e. notations of operations, over expressions, and due to my treatment of "meaning" as a set, the punctuation signs denote operations over sets.  A text in a natural language is a sequence of words and punctuation signs and, therefore, it denotes a set, which can be calculated proceeding from the meanings of words which are sets.
With this treatment, the next question which appears naturally, is whether there is a small number of operations over sets through which all other operations over sets can be expressed? The answer turned out to be simple - such a binary operation was introduced by Tarski and Givant and is called "adjunction". Currently I am working on axioms of the algebra with this operation and constants to play the role of quantifiers. You might want to look into my questions - this this.
and this
We can also discuss about this in more detail if you drop a message to my email indicated in my profile.
