哥德爾揭示了在多數情況下,你永遠不能找出公理的完整集合.每一次你將一個命題作為公理加入,將總有另一個命題出現在你的所能形式證明的範圍之外.你可以加入無窮條公理到公理列表中,確保所有命題都可證明為真或假,但此時將沒有機械的方法判定給定是否是系統的一條公理.

下面普及一些與哥德爾不完備性定理有關的一些定義

1. 形式系統

最早的數學定理都是用自然語言寫的，但隨著數學的內涵越來越豐富，自然語言在表達數學概念時顯得越來越啰嗦，比如要描述一個物體的運動過程，七言萬語的文字絕對比不上一個公式的簡潔直觀（為了簡化表達，數學家們開始越來越多地用符號來表達數學概念，這種情況發展到極端後自然語言被徹底地拋棄，數學完全的符號化,這種語言就稱為形式語言!比如我們高中學過的邏輯與命題裡面的各種邏輯連詞，謂詞等等

數學家又發現人的推理過程是可以看做符號變換的。比如『已知命題A，又已知命題A能推出B，那麼B成立』這條規則可以抽象為 A, A→ B ? B [1]。這樣一來數學證明可以完全變成機械的符號變換遊戲，哪怕你不懂這些符號什麼意思，只要你記住規則，就能證明出一個個數學定理。這聽起來非常誘人，於是數學家制定了形式語言的語法，把符合語法的句子稱為命題，又選出一組命題稱為公理，最後制定了一組推理規則，這樣給你公理，根據推理規則，你就可以推出許多被稱為定理的命題。這套系統就被稱為形式系統。從公理推出定理的過程就被稱為證明，推出命題否定形式的過程自然就被稱為證偽

仔細想想，這裡面其實有個問題：我們怎麼確定這套推理系統是對的呢？換句話說，我們怎麼知道推出的命題是真命題呢？理論上說，數學可以完全無視現實世界，從任意的公理出發推出任何命題，但我們還是希望我們研究的數學能解決現實問題，所以我們要確保我們的形式系統確實是在描述我們想要的數學理論。為了解決這個問題，數學家為形式語言建立了語義，換句話說，就是把形式語言的符號翻譯成我們已知的東西[2]，這樣如果推出的命題翻譯過來是錯的，那麼我們就需要修改推理規則，直到其語義符合預期。而符合語義的命題我們就稱為真命題。後來邏輯學家發現，一種叫一階語言的形式語言有非常好的性質，用一階邏輯表達的形式系統，不管你給公理什麼語義，只要公理都為真，那麼所有能推出的命題都是符合這個語義的真命題，所以現在大部分形式化的數學理論都用一階語言表達，包括目前數學的基礎：ZFC公理集合論。

2. 希爾伯特計劃

既然形式系統這麼好，那麼能不能把所有數學都形式化呢？以後也不用費腦子證明了，直接扔給機器窮舉，一噸噸的數學定理就造出來了。

希爾伯特覺得：能！

他暢想了一個美好的未來，所有的數學理論全都用一種形式語言來描述，並且這套系統滿足如下四個性質——

完備性：任意一個符合這個形式系統語法的句子，也就是一個命題，都能證明或證偽。

一致性：這個系統不會同時推出一個命題和它的否定。

可判定性：如果給定任意定理，可以用演算法在有限步內判定真偽。

保守性：證明可以不依賴『理想對象』（比如不可數集合）。

而且更重要的是，這四個性質還要在這個系統內被證明。

這個想法倒是非常美好，但就在希爾伯特退休後一年，即1931年，哥德爾的兩條不完備定理直接宣判了希爾伯特計劃的死刑。

3. 哥德爾不完備定理

第一不完備定理

一個包含皮亞諾算術的形式系統如果是一致的那麼是不完備的。

第二不完備定理

對於一個包含皮亞諾算術的形式系統，該系統的一致性不能在系統內部證明。

先來解釋一下皮亞諾算術是什麼。皮亞諾算術是一套用一階語言描述的形式系統，它被用來刻畫自然數以及基本的自然數算術，比如加法、乘法和乘方。那『包含皮亞諾算術的形式系統』是什麼意思呢？直觀上理解，就是說從這個形式系統中，可以推出一組命題，這些命題可以描述自然數以及算術。比如ZFC集合論就是包含皮亞諾算術的系統，你可以用 {1}, {2} {3}... 來表示1、2、3……，用集合操作來模擬自然數上的運算，所以有些命題是不能在ZFC中證明或證偽的，ZFC也不能證明自己是一致的；再比如圖靈機也是一個包含自然數的形式系統，而停機問題可以理解為這個系統里無法被證明和證偽的命題。

哥德爾的兩個不完備定理直接戳破了希爾伯特的夢想：包含算術的形式系統不可能完備，而且這個系統本身的一致性不能在系統內被證明。後來圖靈的停機問題又摧毀了希爾伯特對可判定性的期待。

一些延伸:

1. 所有的理論都是不完備的嗎？

顯然不是的。比如平面幾何，你不能從平面幾何推出皮亞諾算術，因為平面幾何是個完備的理論。而且哥德爾給出的『包含皮亞諾算術』的限制其實都很強了，給一個弱得多的限制，理論依然是不完備的。哥德爾提出第一不完備定理後不久，Rosser就給出了一個更強的（更強的意味著限制更弱）不完備定理：一個系統只要包含羅賓遜算術就足以產生不完備性了（羅賓遜算術只有加法和乘法）。哥德爾當時強調皮亞諾算術（原文其實更模糊，是『基本算術』），主要是針對希爾伯特計劃。希爾伯特想把所有數學都形式化成一套系統，然後把證明歸結成基本的自然數算術，再在這個系統內證明自然數算術是一致的，這樣就完成整個數學的形式化，結果被哥德爾無情打臉。

另外，哥德爾不完備定理其實還有個隱藏限制，那就是形式語言的公式集必須是遞歸集合，換言之，你的公式必須可以從有限個符號經過有限步構造出來。如果你用像實數那麼多的符號來表示，哥德爾不完備定理就失效了，但這毫無意義，因為人類沒辦法寫出這種語言。同樣的，如果你能造出『實數計算機』，那停機問題也可以解決了。

2. 那我不用形式語言描述理論，是不是可以避免不完備性？

這麼說倒也沒錯。哥德爾的證明是先把形式語言編碼成自然數，然後證明『所有自然數代表的公式集合』是比『能推出的所有公式的編碼集合』更大的集合[6]，所以總有公式是證明不出來的。如果理論用自然語言描述，自然語言沒有確定的語法，也就無法編碼了。但是如果你不能精確定義語言，你也無法精確定義『證明』、『真』這樣的概念，又怎麼保證你證明得對呢？而且用形式語言和用自然語言描述的理論本質是一個東西[7]，這就好比一個命題不管你用漢語說還是英語說，真假都一樣。所以形式系統的不完備性也可以當做直覺上數學理論的不完備性。

另外用形式語言可以起到區分元理論和對象理論的作用。元理論是指描述這個形式語言的理論，而對象理論是用這個形式語言來描述的理論。其實我剛才說『一個命題不管你用漢語說還是英語說，真假是一樣』是不準確的，比如『這句話是漢語』這句話，翻譯到英語就是假的，但是這句話其實是一個元理論的命題，它描述了寫『這句話是漢語』的語言本身，所以它不是漢語這個系統內的命題。再比如上一段中『哥德爾的證明是先把形式語言編碼成自然數，然後證明「所有自然數代表的公式集合」是比「能推出的所有公式的編碼集合」更大的集合』這句話，句中的『證明』和形式系統里的『證明』就不是一個層面的詞。如果數學命題都用自然語言描述，就會出現很多元理論和對象理論混淆的情況。

3. 哥德爾不完備定理用了哪些公理呢？

根據哥德爾在他自己的論文On Formally Undecidable Propositions of Principia Mathematica and Related System中所說，他是在羅素和懷特海一起創立的PM形式系統里進行證明的[8]，用到的元數學概念是自然數算術。

4. 不完備定理依賴算術又說算術是不完備的，這不是循環論證嗎？

這得從哥德爾本人的哲學立場說起。哥德爾是個柏拉圖主義者，在柏拉圖主義者眼裡，數學對象都是永恆存在於獨立於現實世界的理念世界裡的。既然數學天然存在，那推理就不是數學定理存在的前提，而是發現數學的工具。這就好比人們根據天王星的軌道偏差推理出海王星的存在，不能說海王星因為人的推理而存在。所以，雖然哥德爾用了算術知識來證明不完備定理，但不能說不完備定理依賴算術而存在。這隻表示哥德爾相信他用的知識是必然正確的，他用這些知識推理出一個對數學世界普遍成立的規律。

但很多數學家認為數學就是從公理中推出來的，是人類思維的創造。如果站在這個立場，那哥德爾確實有循環論證之嫌：他在算術里討論了一個元算術的性質。所以這個定理更多地被視為哲學或邏輯學定理而不是數學定理[9]。注意這不是說哥德爾證錯了，只是說哥德爾已經到數學和哲學之間模糊的邊界了，甚至可以說他是在數學外觀察數學。至於到底什麼是數學，現在沒人能回答得了，大部分數學家也不在乎這個問題，ZFC作為數學基礎已經足夠好了，空談主義並不能幫助數學家解決實際問題。順便一提，現在倒是有不少計算機科學家在做數學基礎的研究……

一般來說，不管什麼哲學立場，不管討論多麼基礎的對象理論，元理論都會包含一點基本的算術，否則我們連定義符號、語法都不行，形式化更無從談起。

5. 計算機是個不完備的形式系統，但是人能證出哥德爾不完備定理，是不是說明人腦比計算機強？

這是個廣為流傳的誤解。計算機是可以證明哥德爾不完備定理的，Lawrence C. Paulson就用Isabelle這個軟體證明了哥德爾不完備定理[10]。雖然目前計算機只能處理形式化的數學，但是你可以先形式化一些基礎的結論，然後把其他數學理論在這個形式系統里再形式化一遍，最後證明這些形式系統內的形式系統有不完備性。順便夾個私貨，作為物理主義者，我相信人腦理論上是能用圖靈機模擬的，但是能不能造出來、或者造出來能不能被人理解就不好說了。

6. 物理學需要數學，哥德爾不完備定理是不是意味著我們永遠無法理解宇宙？

這個問題不好說。我傾向於認為哥德爾不完備定理和物理沒多大關係。首先，物理定律只是在用數學，而不是創造數學。假設你發現了宇宙最基本的定律，幾個方程組可以求出一切物理量，那你也不需要用這個方程組推出自然數、有理數等概念，只要它們能描述你觀察到的一切現象就行。再者，宇宙里所有粒子或別的什麼基本單元也可能是有限的，你給它們用自然數編號，哪怕一個粒子用一個公式描述，那也是遞歸集，並不會有不完備性。

最後選取不同的數學基礎，可以把語言翻譯到不同的數學對象上。由於目前ZFC是大多數數學家公認的基礎理論，所以標準語義都把變數翻譯到一個被稱為論域的集合上，把函數和關係符號翻譯成論域上的函數和關係，這樣的標準語義也被稱為模型。研究標準語義的理論被稱為模型論

遞歸集是指『某元素是否存在於該集合中』可以用演算法判斷出來的集合。至於什麼叫『演算法』，[0]里提到的數理邏輯教材都有講。另一個相似的概念是遞歸可枚舉集，指在集合中的元素可以用演算法判斷出來，但判斷元素不在集合中可能會讓演算法死循環

推薦閱讀：

相关文章