形式化というのは飽くまでも無矛盾性を示したり
或る命題が独立であることを示したり、或いは
証明が厳密に行われることを保障するために行うものなので、
別に循環論法だとかそういうことは無いと思う。

集合論やら述語論理やらを記号列に関する形式的なルールの集まりとして表現した時に、
そのルール自体は、元の理論で直接扱うようなものでは無いんです。