不完全性定理
正文
在證明不完全性定理時,主要是使用算術化方法,即先把形式系統中所使用的各符號都逐一給以一個自然數編號，然後依次對各公式也給以一個編號，再後又對各公式序列，例如證明中所使用的公式序列給以一個編號。凡屬編號必須滿足下列條件，即給出符號或公式或公式序列後，可以唯一地決定其編號。反之，當給出一個自然數後，則可以決定其是否用作編號，如果是，就可以唯一地決定其是符號的或者是公式的，還是公式序列的編號。滿足這種條件的編號，叫做哥德爾編號。利用編號可以把有關形式系統的各性質用算術函式算術公式來表示。例如，可以作出一個算術公式 prov(a,b)，使得prov(a,b)成立若且唯若編號為a的公式序列是對編號為b的公式的證明,這也表明證明關係是可以算術化的。有了這些（以及別的）算術函式算術公式後，就容易作出不可判定語句。根據不完全性定理的證明過程，還可以推得下列結論：如果包含皮亞諾自然數論為子系統的形式系統 U是協調的，則表示" U是協調的"這個事實的算術公式不可能在系統 U內證明，這個結果叫做第二不完全性定理。它也是證明論中很重要的結果。
雖然證明關係、可證性、協調性等等是可以算術化的，但由不完全性定理卻可推得：真假性是不能算術化的，亦即不可能找到一個算術公式tr(a)使得tr(a)成立，若且唯若以a為編號的公式A為真，也就是說,在系統U內下列公式tr(a)凮A（這裡a為A的編號）是不可證的。這是不完全性定理的另一內容，它是由A.塔爾斯基首先給出的（見不可定義性理論）。
