We've a formal system say First order Logic, we reason about it in our meta-language using our meta-logic. We study its properties as a mathematical object. We prove theorems like group theory. This makes us able to know the limits and the strength of the system (like completeness) or studying arithmetic in First order logic. For example, Godel first incompleteness theorem is a theorem in the meta-language.
Now, I wonder, Why not to formalize the meta language itself which we use to argue about FOL. Why? two reasons, the first is that proving things about this system means proving things about what we can know about first order logic. Some sentences of FOL could be unprovable in this formalized system and hence we can not prove somethings about FOL. Let's call this new system the "formalized meta-logic"
Second, we could by some trick be able to reflect the reasoning in the formalized meta-language inside FOL and hence it could give us somethings useful which is unexpected?
For a preliminary sketch of how this "formalized meta-logic" will look like, I think we would have similar logical connectives (denoted by other symbols to avoid confusion) which range over collection of formulas (or over formulas, according to what turns out to be more appropriate), meta-predicate, which represents "properties of formulas", constants that represents fixed formulas. so for example, Godel incompleteness theorem (in the meta-language of FOL) could be represented as a formal formula in this "formalized meta-logic".
So, my questions are:
$1$- Are there any trials in that directions? If the answer is yes, Could you provide me with some resources (texts\articles etc ...) so that I can read about it?
$2$- If no such formalization exist, Could it be done? if yes, Do you think it will be of any use other than mere curiosity? why or why not?
$3$- will such a system be related to higher order logics? If yes, How? I'm completely unfamiliar with those logics but I've been told that they quantify over collection of subsets of elements rather than elements itself.