Proving proof system properties within the proof system itself?
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.