>>632
好みの問題だけど多少表記を変えます。

式Aのゲーデル数(の数項)を"A"と書くことにして
φ(x)が「Tの公理である」を表す式だとすると
AがTの公理 ⇒ T |- φ("A")
AがTの公理でない ⇒ T |- ¬φ("A")

また不動点定理より、ある論理式Bがあって
T |- B <-> ¬φ("B")

そして
(1) 論理式BはTの公理ではない。 T |- ¬φ(B"))
(2) 論理式Bは証明できる。 T |- B
で、別に問題は生じないです。