>対角化定理
>https://ja.wikipedia.org/wiki/%E5%AF%BE%E8%A7%92%E5%8C%96%E5%AE%9A%E7%90%86
>|-_T (C⇔F(°#C))
ここでF(x)は一変数論理式であれば任意でよく（文CはF(x)に応じて定まる）、Tにおける証明不可能性述語¬Prov_T(x)を適用したとき
|-_T (G⇔¬Prov_T(°#G))
の文Gがゲーデル文で、これは「この文はTで証明できない」という文。
対角化定理はゲーデル文のような自己言及文の存在を主張している。