Formalizing the meta-language of First order Logic and studying it as a formal system

It is completely standard to study formalized metatheories. Historically, this is particularly of interest from the point of view of mathematical finitism - most proof systems for first-order logic are completely finitistic, based only on symbol manipulation, and so their formalization is somewhat straightforward.

Formalization of the metatheory is also of interest to help us see the mathematical techniques required to prove theorems of logic such as the completeness theorem.

Rather than making a formal metatheory that quantifies directly over strings, as suggested in the question, it has been more common to work with Primitive Recursive Arithmetic, whose basic objects are natural numbers. There is a tight link between formulas and natural numbers, as I explained in this answer. PRA is often studied as a quantifier-free theory, with a large collection of function-building symbols; it is typically considered to be "the" formal standard for a finitistic theory.

We know for example, that a formalized version of the incompleteness theorem is provable in PRA.

PRA cannot talk about infinite sets, and so cannot talk about infinite models. To look at logical theorems such as the completeness theorem, we need to move to slightly stronger theories. We could use ZFC set theory, but that is far more than we need to study the countable logical theories that arise in practice. It has been common to use theories of second-order arithmetic, which can talk about both natural numbers and sets of natural numbers, to study the completeness theorem. We know that, in this context, the completeness theorem for countable theories is equivalent to a theory of second-order arithmetic known as $\mathsf{WKL}_0$, relative to a weaker base theory.

The way to get into this subject is to first learn quite a bit of proof theory, after you have a strong background in basic mathematical logic. There are not any resources I am aware of that are readable without quite a bit of background. Even introductory proof theory texts often assume quite a bit of mathematical maturity and exposure to mathematical logic, and are written at a graduate level. So there is no royal road to the area, unfortunately, although much beautiful work has been done.

To get a small sense of what exists, you can read about the formalization of the incompleteness theorem in Smorynski's article in the Handbook of Mathematical Logic. That article only describes one part of a much larger body of work, however. The overall body of work on formalized metatheories is spread out in many places, and described from many points of view. You can find some of these in the Handbook of Proof Theory, and in the following texts:

• Petr Hájek and Pavel Pudlák, Metamathematics of First-Order Arithmetic, Springer, 1998
• Stephen G. Simpson, Subsystems of Second-Order Arithmetic, Springer, 1999
• Ulrich Kohlenbach, Applied Proof Theory: Proof Interpretations and their Use in Mathematics, Springer, 2008

All of these are intended for graduate or postgraduate mathematicians.