公理的集合論を組み立てていくときに
述語論理の完全性だとか、極大無矛盾理論の存在だとかは
無関係、必要ない情報なんじゃないかと思うのだけど

そうして、既に組み立てられた公理的集合論を用いて、
「論理式からなる集合」について一層詳しい性質を調べることは
別におかしくない