About intuition.
Aristotle introduced a notion of consequence along the following lines. Suppose $A$ and $B$ are sentences, each of them either true or false. We study the relation :
(1) 'If A is true, then B has to be true too'.
Many logicians reckoned that the main use of logic is derive conclusions from premises, with the obvious goal that if we start from true premises, and we use “logical rules”, we will derive true conclusions. This idea of logic gives rise to the relation :
(2) 'From A, we can prove B'.
Now we try to translate all this into modern terms.
(1) translates into the relation of logical consequence $A \vDash B$ :
'For every interpretation $\mathcal I$, if A is true under $\mathcal I$, then B is true under $\mathcal I$.'
We “generalize” it putting in place of the sentence A a set $\Gamma$ of sentences :
$\Gamma \vDash \varphi$
which means that :
'For every interpretation $\mathcal I$, if all of $\Gamma$ are true under $\mathcal I$, then $\varphi$ is true under $\mathcal I$.'
Lastly, we have the “special acse” when $\Gamma = \emptyset$ : $\vDash \varphi$ means that the sentence $\varphi$ is valid (in propositional logic it is a tautology) when it is true under every interpretation.
In this case, we call it also logical (or universally) valid sentence, meaning that it is true “under all possible circumstances”.
For (2) [see Neil Tennant, Natural logic (1978), page 5], we have that, in order to demonstrate the validity of an argument one needs a proof.
A proof of an argument is a sequence of steps starting from its premisses, taken as starting points, to its conclusion as end. Within a proof each step, or 'inferences', must be obviously valid.
A system of proof is a codification of these obviously valid kinds of inference, which we call rules of inference. A proof in accordance with these rules must, in order to meet the demands of certainty, satisfy the following conditions :
(i) It must be of finite size.
(ii) Every one of its steps must be effectively checkable.
A system of this type is a logical calculus (i.e.proof systems) formalizing the relation of derivability :
$A \vdash B$
which is :
'B is derivable using only the logical rules of the calculus, starting from A as premise’.
We “generalize” it putting in place of the sentence A a set $\Gamma$ of sentences :
$\Gamma \vdash \varphi$.
Lastly, we have the “special case” when $\Gamma = \emptyset$ : $\vdash \varphi$ means that the sentence $\varphi$ is theorem of the calculus (it is provable) when it is derivable from no premises.
Obviously there must be no invalid proofs in our system : the system must be sound.
Moreover we wish to be able to prove any valid argument expressible in the language. The system, that is, must be complete (or adequate).
Soundness : if $\Gamma \vdash \varphi$, then $\Gamma \vDash \varphi$ (with the particular case : if $\vdash \varphi$, then $\vDash \varphi$)
Completeness : if $\Gamma \vDash \varphi$, then $\Gamma \vdash \varphi$ (with the particular case : if $\vDash \varphi$, then $\vdash \varphi$).
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.
Best Answer
There's nothing special about formalizing any area of logic. As with formalizing any subject it's quite difficult, but it's not inherently more difficult than any other area of math.
Here are some examples I found with a quick google search:
This CSSE thread discusses formal proofs of the compactness and completeness theorems.
This paper looks at formalizing the independence of CH.
Here's a treatment of the incompleteness theorems.
And so forth. Indeed, the whole starting point of "modern metalogic" is the realization that it can be construed as just another area of mathematics.