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

Question

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.

Answer 1

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.