>>8
＞完全性定理の証明を形式化したとき
＞論理式に選択公理が入ってるってこと。

この人の「形式化」という言葉の使用法は独特ですね。

どうも、数学の命題を必要な前提条件をつけた上で
一階述語論理の論理式で書き表す行為を「形式化」
とよんでいるようです。

それはともかく、この言葉、実際は不要ですね。
なぜなら単純に
「完全性定理を証明するのに選択公理が必要」
と書けばいいだけなので。