Proving proof system properties within the proof system itself? While reading about Frege proof systems in [1], I came across the completeness theorem and its proof, which involves a few lemmas introduced first. Here are the first two of those lemmas:
$$\begin{equation} \vdash \phi \supset \phi \tag{1} \end{equation}$$
$$\begin{equation} \Gamma, \phi \vdash \psi \space \text{if and only if} \space \Gamma \vdash \phi \supset \psi \tag{2} \end{equation}$$
The first one is easy to prove using the axioms and inference rule of Frege proof system. The proof of the second one uses induction. This confused me a bit and prompted the following questions:

Are proof systems &quot;self-contained&quot;, in the sense that their properties can be proven within themselves? Or are properties such as soundness and completeness &quot;external&quot; to the system? The rationale being part of the motivation for proof systems to formalize proofs and thus serve as a foundation of sorts for other math.
Is there some &quot;strange loop&quot; going on when using something like induction (which is defined on the natural numbers) to prove such properties? Also, $\Gamma$ is a set, which is not really part of this proof system vocabulary. For example, if you use a sound but incomplete proof system $P$ to prove the soundness and completeness of another proof system $Q$, does that imply that $Q$ can't &quot;express&quot; $P$ somehow, since that would be paradoxical?

Sorry if my question is ill-posed. I'm a beginner to this topic, so I would appreciate any advice on formulating the question correctly as well.

[1] Buss, Samuel R. (ed.), Handbook of proof theory, Studies in Logic and the Foundations of Mathematics. 137. Amsterdam: Elsevier. 811 p. (1998). ZBL0898.03001.
[2] https://en.wikipedia.org/wiki/Semantic_theory_of_truth
There is no loop. The purpose of a formal system is to make reasoning principles explicit and to explain more precisely how reasoning works. The word &quot;foundation&quot; in &quot;foundations of mathematics&quot; does not mean &quot;create a secure base for mathematics out of nothing&quot; – that would be an indifensible position.
There is absolutely nothing wrong with a logicians using sets to describe a formal system. Should a number theorist not be allowed to use numbers? Are logicians allowed to use strings of symbols? Where do you draw the line?
On the technical side of things, there are formal systems that can talk about their own syntax and proof rules. After all, that is the gist of Gödel's incompleteness theorems: he shows that as soon as a formal system contains arithmetic, it can speak about syntax and its own provability.