Is proving metatheorems circular logic?

Question

I am currently learning mathematical logic, and I came across a dilemma. In proving metatheorems (theorems about formal systems), almost all the proofs for said metatheorems used mathematics (induction, set theory, etc). Since most of mathematics is justified by first order logic, which itself is a formal system, wouldn't using mathematical methods to prove metatheorems be circular logic? Not only that, but the proof for the deduction theorem, which itself is an if~then~ proposition, uses the deduction theorem itself. Is this practice natural? I apologize in advance if I am missing something basic or obvious. Thanks for all the help.

Answer 1

I understand your discomfort, I also felt the same when I began to study logic. Right on the beginning of propositional logic, one is faced with a combinatorial remark: the number of rows in the truth table of a formula with $n$ propositional variables is $2^n$. A little later, when reading about the language of first-order logic and its semantics, you must know what is an infinite countable set (because so is the alphabet of FOL), what is a function, what is a relation, etc. As far as I understand, this apparent circularity is insurmountable: when you formalize logic, and mathematics, you must know what it is being formalized. This is the reason why one must study logic and set theory in parallel: each one "depends" (in some sense) on the other. But this is not really a circular reasoning, because the formalized theory and the informal knowledge of the concepts being formalized are in different levels (theory vs. metatheory).