>>361
　まあ、ゲーデルの完全性定理くらいなら、メタ言語の推論体系は、集合論を
使うといってもせいぜい２階の述語論理（ただしメタ言語に排中律を用いる）
くらいで済むと思うけど、∀x(0+x=x)の証明不可能性を超準モデルで証明とい
うことになると、どうなんだろう？
　だいたい、メタ言語で排中律を使うと、それだけで議論が超越的になり、例
えば「〜は証明可能である」というメタ定理が証明されても、実際に証明を書
き下す方法が与えられるとは限らなかったりする。
　まあ、数理論理学を「数学を使って」議論するのは、他の数学的対象を数学
を使って議論するのとどこが違うんだ、考察の対象が論理学だからといって排
中律の使用に対してガタガタ言ってもしょうがないだろう、という声が聞こえ
てきそうだが、やはりタカが文字列に関する議論で、「排中律」やらツォルン
の補題やらを使うのはちょっと大げさすぎる気がして、個人的には好きになれ
ないのは事実。
　まあ、所詮趣味の問題に過ぎないのだが。