嚴羽

[拼音]：buwanquanxing dingli

[英文]：incompleteness theorem

證明論中的一條重要定理。由K.哥德爾於1931年證明，是數理邏輯發展史上的一個極為重要的定理。

設有一個以皮亞諾自然數論為其子系統的、自身協調的（即不自相矛盾的）形式系統，暫記為 U；在形式系統中凡不含自由變元的公式叫做語句；如果語句 A和塡A在某形式系統內均不可證，則A就叫做該形式系統的不可判定語句。不完全性定理說，任何一個上述的系統U都必有一個不可判定語句A。依照排中律，A和塡A之間必有一個是真語句，故不完全性定理可改為：任何一個上述的系統 U都必有一個真語句是不能推出的。如果一個系統對任何語句 A能夠推出A或推出塡A，則這個系統叫做完全系統，這樣不完全性定理又可改述為：任何一個上述的系統 U必是不完全的。

在證明不完全性定理時，主要是使用算術化方法，即先把形式系統中所使用的各符號都逐一給以一個自然數編號，然後依次對各公式也給以一個編號，再後又對各公式序列，例如證明中所使用的公式序列給以一個編號。凡屬編號必須滿足下列條件，即給出符號或公式或公式序列後，可以唯一地決定其編號。反之，當給出一個自然數後，則可以決定其是否用作編號，如果是，就可以唯一地決定其是符號的或者是公式的，還是公式序列的編號。滿足這種條件的編號，叫做哥德爾編號。利用編號可以把有關形式系統的各性質用算術函式算術公式來表示。例如，可以作出一個算術公式 prov(a，b)，使得prov(a，b)成立當且僅當編號為a的公式序列是對編號為b的公式的證明，這也表明證明關係是可以算術化的。有了這些（以及別的）算術函式算術公式後，就容易作出不可判定語句。

根據不完全性定理的證明過程，還可以推得下列結論：如果包含皮亞諾自然數論為子系統的形式系統 U是協調的，則表示“ U是協調的”這個事實的算術公式不可能在系統 U內證明，這個結果叫做第二不完全性定理。它也是證明論中很重要的結果。

雖然證明關係、可證性、協調性等等是可以算術化的，但由不完全性定理卻可推得：真假性是不能算術化的，亦即不可能找到一個算術公式tr(a)使得tr(a)成立，當且僅當以a為編號的公式A為真，也就是說，在系統U內下列公式tr(a)凮A（這裡a為A的編號）是不可證的。這是不完全性定理的另一內容，它是由A.塔爾斯基首先給出的（見不可定義性理論）。