基本術語
理論，theory陳述，statement
在理論中可證明，provable in the theory
一致，consistent
可構造，can be constructed
Godel命題，Godel sentence
基本算術，elementary arithmetic
理論，是指由一些陳述構成的集合，其中可能有無窮多個陳述。理論中的某些被設定為公理而無需證明。某些陳述可由這些公理導出，這樣的陳述稱之為一個定理。定理等價於真(true)的陳述。一個公理體系的全部出發點實際上不僅僅包含公理，還包含其基本的記號以及定義。由此可知Godel定理中的證明一詞的含義和我們通常理解的並不相同。
可以證明，確切地說，在某個給定的理論體系中是可以證明的，其含義是指，可以由該理論體系的基本記號、定義以及公理，使用標準一階邏輯導出。一個理論被稱為一致，是指在這個理論中，不能證明互相矛盾的陳述。
可以構造的陳述，是指，存在一些機械的過程，可以由給定的公理、原始記號、定義以及一階邏輯，構造出該陳述。
真的但是不可證明的陳述被稱為“Godel命題”。事實上，存在無窮多個這樣的“Gedel命題”。基本算術體系，是指在自然數集合上，賦予加法和乘法兩種運算的理論體系。
通常對於Godel不完備定理的討論，嚴謹的說法是其定理否定了Hilbert計畫。不嚴謹的說法比比皆是，比如認為Godel不完備定理證明了機器能力的局限等等。
Hilbert計畫起源於以證明了不動點定理而聞名的荷蘭數學家Brouwer提出的一個數學哲學觀點，稱之為直覺主義。Brouwer認為存在性的證明是不完美的，或者說是值得懷疑的。比如其本人所證明的不動點定理，單位球到自身的連續映射必定有一個不動點。定理斷言存在一個不動點，然而無論是該定理還是定理的證明都沒有告訴我們這個不動點到底是空間中的哪個點。換言之，這個證明不是一個構造性的證明。我們再舉個例子來看構造和非構造證明。 Weierstrass構造了一個連續然而處處不可導的函式，這是一個構造性的證明，我們可以明確的看到這個函式。Banach則證明了，幾乎所有連續函式函式都是處處不可微的。這個證明就是非構造性的。雖然這種函式很多，但由Banach的證明，我們一個這樣的函式都沒有看到。在Brouwer看來， Banach定理是無意義的。Brouwer後來更是走向極端，宣稱放棄他賴以成名的不動點定理，因為它不是構造性的。再如，微分方程解的存在性， Brouwer認為必需把解構造出來才是有意義的。通常證明存在性的方法是，假定不存在，然後導致矛盾。然後由這個矛盾得到存在性。這當然是無懈可擊的證明。但是對於Brouwer來說，既然他已經反對了這種非構造新證明，他就必須反對這種證明方式。因為這樣的證明必然導致非構造性的存在性。從邏輯上看，通過矛盾來反證的基礎是排中律。排中律的含義是一個陳述P, 則P或者NotP(P的否定)必有而且只有一個成立。放棄排中律給證明帶來了很大的困難。放棄排中律得到的形式邏輯體系是不完備的。放棄排中律導致一個命題否定兩次不一定回到原命題，即NotNotP不一定和原命題P等價。這是很糟糕的。為此，Brouwer在他的直覺邏輯體系中又增加了否定之否定即原命題這一條。這一行為被諷刺為“Brouwer荒謬之荒謬”。
Brouwer進一步認為，全部數學理論應該建立在其直覺邏輯的基礎之上。Brouwer由此否認幾乎全部的數學，事實上只有少數理論可以由 Brouwer的直覺邏輯體系得到。雖然Brouwer的觀點看起來不那么惹人喜歡。但這不代表其沒有影響力。Brouwer的觀點激怒了很多的數學家，包括Hilbert. 作為回擊，Hilbert提出一個計畫，希望由有限、組合的方式，先證明最簡單的算術是一個內部一致的理論，然後以此為基礎證明數學分析的一致性，爾後進一步證明整個數學的一致性。Hilbert計畫中的證明就是純粹構造式的。由前面的分析可知，這個計畫中的數學證明沒有排中律參與。
用現在的語言來敘述，Hilbert計畫實際上是要尋求一些算法，這些算法可以構造出真的算術命題。Penrose舉過一個例子。1966年美國數學家羅伯特.伯格爾(Robert Berger)證明了平面上能夠按某些給定的基本圖形拼圖(tiling)的多米諾問題(Domino Problem)，卻不可能由預先設計好的計算程式給出來。也就是說，只能一步一步用人的腦筋去拼合，這實際上就是直接證明了存在一個不可計算的數學方法。但是也可以用機器的電腦一步一步拼接出來，沒有任何理由可以說明機器一定不能拼出來。
另一個非構造性的例子，複變函數理論中對於代數基本定理的證明。我們知道可以由Cauchy不等式來證明，也可以由簡單的代數拓撲來證明，其完全不同的證明方式不下5個。但這些證明都不告訴我們多項式的解到底是什麼。而Galois證明的代數方程一般無根號解實際上就是在某種程度上否認了可構造解的存在性。
我個人認為可構造性是理解Godel不完備定理中的關鍵。
直覺主義
對於直覺主義，一個更好的稱呼是：有限可構造主義。Kronecker是最早的直覺主義者，他只接受整數，認為自然數是上帝創造的，整數是直覺上清楚的因而是可以接受的。Kronecker認為其他都是人造的，可疑的，因而是不可接受的。基於其哲學觀點，Kronecker以其全部力氣反對Cantor的集合論。Kronecker甚至認為應該從數學中將無理數砍掉，因為無理數不能夠通過有限多個步驟構造出來。
Poincare對直覺主義有不少的嘲諷。不述。
H.Weyl也是持有直覺主義觀點的數學家。
Brouwer給出了直覺主義的最系統的闡述。簡而言之，直覺主義的觀點就是通過有限多個步驟可以構造，才是有意義的。直覺主義認為數學定理的正確性和有效性存在於人類的智力中。
無限，確切的說，完成了的無限，實的無限，是直覺主義不允許的。比如，下述的兩個陳述：
1，素數只有有限多個；
2，素數有無限多個。
在一個正常人看來，這兩個陳述必有而且只有一個成立。但是在Brouwer看來不然，他認為這兩個陳述都是沒有意義的。
再如，直覺主義認為，無限多個自然數中必有一個取到最小值這樣的命題也是沒有意義的。
我們可以如此總結直覺主義，摒棄排中律，否定實無限，堅持可構造性。
當然，直覺主義並不完全否定無限。但直覺主義認可的無限是指潛在的沒有完成的無限。比如數學歸納法中的無限，由n到(n+1), 在直覺主義看來，這不代表無限，僅僅是一個符號而已。
Hilbert計畫其實就是要完成直覺主義。
一致性
理論的一致性也就是無矛盾，確切的說該理論中不能導出互相矛盾的兩個命題。如何證明一個理論體系是無矛盾的呢？舉幾個例子。非歐幾何的無矛盾性是通過歸結到歐氏幾何來完成的。亦即通過Poincare模型或者Klein模型，在歐氏幾何中重新解釋其中的某些術語，這些術語可以與非歐幾何的術語一一對應。因而只要歐氏幾何無矛盾，則非歐幾何也是一致的。這是相對一致性。因為歐氏幾何的一致性還需要證明。
歐氏幾何的一致性可以由解析幾何實現為三維歐氏空間上的代數體系的無矛盾性。進而可以歸結為實數系統的一致性。再進一步，由實數理論，又可以歸結為自然數體系的一致性。這些都是相對一致性。
所以剩下的就是證明自然數體系的一致性。
上述的歸結過程必然需要在某個地方終止，也就是說不可能一直使用相對一致性。終止過程對應的理論的無矛盾性不再可以通過其他的理論來證明，只能在其自身範圍內完成。所以，問題是如何在自然數體系內完成其一致性的證明。
Hilbert在1922年提出他的計畫，並認為很快就可以得到這個一致性的證明。Hilbert的計畫是，由形式化來完成這個任務。
附，Poincare的直覺主義和Weyl,Brouwer,Kronecker的直覺主義完全不是一回事。所以上一個帖子中特別提出，後面幾個人的直覺主義可以叫做有限可構造主義。Poincare也諷刺羅素等人的邏輯主義，認為這些人是要把數學歸結為同義反覆。
形式體系
一個形式體系的構成要素為：初始符號、形成規則、初始公式/公理、變形規則。
我們來看一個簡單的形式體系。下述的形式體系記作SFT. (simple formal theory).
初始符號只有一個：X
公理A：X
所謂形成規則是指由初始符號如何構成有意義的字元串。對SFT而言，不需要形成規則，或者說所有的字元串都是有意義的。
變形規則，一共兩條：
D1, 可由X變形為XX.
D2, 可由XX變形為Xx.
由公理X出發，通過變形得到的就是這個形式體系中的定理。例如，由公理A與變形規則D1可證明定理XX. 再用一次D1可證明定理XXX. 注意到變形規則D2並不產生新的定理。
容易看出這個簡單體系的全部定理為，
X, XX, XXX, XXXX, …
顯然可以簡單的給上述定理一個編號。比如，X=0, XX=1, XXX=2, …於是我們看到這個形式體系可以實現為自然數體系。而變形規則D1表示計算自然數n的後繼n’=n+1.
有很多人認為，形式體系中的定理比如SFT中的XXXX, 是沒有意義的，僅僅是一個符號串而已。只有將之實現為自然數或其他具體的體系時，才被認為是有意義的。我個人認為形式體系仍然是有意義的。形式體系和具體的公理體系之間的關係，可以用理論物理與客觀世界之間的關係來類比，雖然則兩種關係並不完全一致，但其中包含的核心精神是相同的。
為了更好的理解形式體系。我們進一步分析上述簡單體系。
首先，SFT體系中的全部定理我們已經列出了，除此以外都不是。比如X(XX)不是SFT體系中的定理。因為括弧不是這個體系中的符號。
其次，定理XXX的證明是由初始公式X使用兩次變形規則D1得到的。
我們給出一個另外的證明。假設XXX不是定理，並由此導致矛盾。這個矛盾就說明了XXX是一個定理。考慮XX, 若XX是定理，則由變形規則D1可知XXX為定理。既然我們假設XXX不是定理，所以必然有XX也不是定理。同樣的論證可知，X也不是定理。但這與SFT 體系的初始公式相矛盾。這就證明了XXX確實是一個定理。
顯然的確給出了XXX是一個定理的證明。
但是這個證明在形式主義看來是不合法的，或者說是沒有意義的。因為形式體系中的證明只能由已經證明的定理通過變形規則得到。
再論形式體系
我們已經指出在形式體系中，新定理只能通過對已經證明的定理使用變形規則得到。沒有其他的證明方式。這是一種很強的構造性。即使純粹演繹邏輯的三段論也是不允許的，除非在變形規則中包含了三段論。Hilbert的形式體系與Brouwer的直覺主義相比而言，對於證明有更加嚴格、狹窄的含義。不僅僅其中沒有排中律，而且規定了定理只能通過變形規則得到。新的定理只能通過已經被證明的定理變形得到。這是一種很強的構造性。
形式體系的其他例子
Lorenzen體系。
初始符號：a,b
形成規則，也稱為語法規則：由a,b構成的有限長度的字元串。
初始公理：ab
變形規則
L1, 若X是一個定理，則aXa也是一個定理。
L2, 若X是一個定理，則Xb也是一個定理。
這是一個稍稍複雜點的體系。容易決定這個體系中哪些有意義的字元串是可由初始公理變形得到的定理。
象棋。
初始符號：象棋的棋子以及棋盤以及一個放置死掉棋子的簍子。這裡每一個符號都只有一個。雖然其中卒有10個-每一方各5個，但我們認為這10個卒是互不相同的，同時這些卒的走法是相同的。
初始公理：棋子最初放置在棋盤上的位置。註：通常的比賽中棋子一開始處於固定的位置。但我們也可以研究殘局，這時棋子的位置就依賴於殘局的選取了，並且一部分棋子在簍子中。
語法規則：棋子在棋盤以及簍子中，棋盤上每一個位置只能放置最多一個棋子，但可以不放。
變形規則：象棋的棋規。比如，兵卒一次只能移動一步，沒過河以前不能橫著移動；馬只能跳“日”字；象只能飛“田”字；以及紅黑棋子輪流移動；吃子法則-將某些子放入簍子中；棋局終止法則，等等。
因而象棋是一個形式體系。這個體系中有很多有意義但不是定理的棋子放置方式。比如一方的象在另一方的半個棋盤內。
算術體系的形式化
算術體系的形式化。我們通常使用的算術體系是在一種樸素的水平上進行的。直到Peano給出算術的公理體系，這種狀況才發生了變化。Peano給出5條公理來描述算術，從而使得算術建立在公理體系之上。我們僅僅敘述Peano的第4個公理：對任意自然數m,n, 若m’=n’,則m=n.此處，m’表示m的後繼，亦即m+1.
但這還不是形式化體系。形式化體系將所有的對象都當作一個符號或者符號串。對算術體系，其中的符號為：
邏輯符號: $\forall$表示任意，$\neg$表示邏輯非，$-->$表示邏輯蘊涵。
括弧: (表示左括弧,)表示右括弧。括弧充分反映了形式化的特點，亦即所有的對象包括括弧都要被形式化。
逗號:,
等號，$P_1^2$表示等號=
變元符號，$x_1,x_2,…$一共可數無限多個變元。
常元符號，$a_1$表示數0.
函式符號，$f_1^1$表示後繼運算，亦即$f_1^1(x_1)=x_1+1$. $f_1^2$表示求和，為二元函式，即$f_1^2(x_1,x_2)=x_1+x_2$. $f_2^2$表示乘積，即$f_2^2(x_1,x_2)=x_1x_2$.
注意，對形式體系而言，上面的說法是不嚴謹的。比如\forall並具有什麼特別的含義，僅僅是一個符號而已。我們給出的解釋語言是為了理解起來方便一些。
這樣，Peano的公理4就可以用形式化的語言敘述為，
(\forall x_1)(\forall x_2)((f_1(x_1)=f_1(x_2))-->(x_1=x_2))
同樣Peano的其他公理以及加法、乘法公理也都可以明確表述出來。
當然還需要給出語法規則和變形規則。我們略掉這些繁瑣的細節。
現在我們有兩個體系，其一是用Peano公理表述，其二是用形式化的語言表述的算術體系。前者可以看作後者的一個模型、一個解釋。通常的自然數1,2,3在形式化體系中表示為
f_1^1(a_1),f_1^1(f_1^1(a_1)),f_1^1(f_1^1(f_1^1(a_1)))
這種書寫方式比較累贅，在不引起混淆時，人們依然採用通常的記號1,2,3來表示這些對象。同樣的記號也用在函式$f_1,f_2,f_3$上。
這樣的一個形式化體系稱為一階算術，或者基本算術。其中只有求和以及相乘兩種運算。在這樣的算術體系中，素數是沒有意義的概念。這個體系中全部的記號、定義、規則都已經給出了，不能再加入新的對象。加入新的定義，比如定義素數，得到的將是另一個形式體系。當然新的形式體系可以看作基本算術體系的一個擴張。
Godel不完備性定理之一
一共有兩個不完備性定理。
Godel的第一個不完備定理：在包含基本算術且一致的形式體系中，存在一個命題P, 使得，P以及notP都不是該形式體系中的定理。或者可以等價地說該形式體系不是完備的。
為了準確的理解這個定理，我們作一些解釋。
一個形式體系包含基本算術，是指，可以將基本算術體系嵌入到這個形式體系中。
命題P是指符合語法規則的一個陳述。
notP是指命題P的否定，亦即“命題P是錯誤的”。
形式體系中的定理，是指可由形式體系中的公理，經過有限多次變形得到的命題。
形式體系中的命題如果是一個定理，則稱為一個可以證明的命題。因而在一個形式體系總，證明一詞的含義是指，可由初始公理通過有限多次使用變形規則得到。和我們通常理解的證明並不相同。
一致，是指不存在命題P,使得P以及notP都是該形式體系中的定理。
由這些解釋，Godel不完備定理也常常被敘述為
Godel第一不完備定理的第二個敘述方式：在包含基本算術且一致的形式體系中，存在一個命題P, 使得，P以及notP都不能在形式體系內部得到證明。
我們進一步作一些解釋。無論如何，一個命題或者正確，或者錯誤。正確的命題，稱為真的命題。而錯誤的命題則稱為假的或者非真的命題。考慮Godel不完備定理中的命題P. 如果P是真命題，則我們得到該形式體系中的一個真的但不可證明的命題，這個命題就是P. 如果P是假命題，則notP是真命題，因而我們仍然得到該形式體系中的一個真的但不可證明的命題，這個命題就是notP.
敘述方式
因而我們得到Godel不完備定理的另一個敘述方式
Godel第一不完備定理的第三個敘述方式：在包含基本算術且一致的形式體系中，存在真的但不可證明的命題。
很多人對於Godel不完備定理的討論都以此為出發點，但卻很少去深究這個看起來簡單明了的敘述方式中每一個詞語的準確含義。這是導致Godel不完備定理被誇大到不恰當的程度的一個主要原因。另一方面，Godel定理中的用語，特別是“真”、“證明”這兩個詞的意義與我們通常看到的並不相同，這也是造成混亂的一個重大原因。究其緣由，應該與Hilbert有關。因為這些基本術語來源於Hilbert形式化計畫。而Hilbert本人深信，其形式化計畫最終可以給出數學嚴格性的終極證明。事實上，如果Hilbert形式化計畫不是被否定，而是得到了肯定的話，我想將沒有任何人可以任何理由反對數學具有徹底的完全的一致性和完備性。既然是Hilbert提出了這個計畫，以及這個計畫的基礎知識和準備工作，也是Hilbert為之命名，同時Hilbert又深信這個計畫最終可以得到數學嚴格性的終極證明，因而原本應該稱作“可構造”的，卻被Hilbert命名為“可證明”。關於Godel定理或者說形式體系中 “證明”這個詞語的來源，在此要特別說明，純屬個人揣測，至少迄今我沒有見到任何文獻提及此事。
將Godel不完備性定理中的“證明”一詞換作不容易引起混淆的“構造”，可以給出
Godel第一不完備定理的第四個敘述方式：在包含基本算術且一致的形式體系中，存在真的但不可構造的命題。
如果我們見到的Godel定理是這樣敘述的，肯定會減少很多不必要的混亂。
不好意思，又來批判Penrose,記得以前有人曾專門發起一個批判Penrose的粒子物理學的運動。:)
對於Godel不完備定理，有大量荒謬的推論。其中之一是以此來證明人工智慧是不可能的，或者機器不可能具有思考能力。比如Penrose在其《The Emperor's New Mind》中的論證。這些論證通常如下進行。
機器是Turning機。
由不完備定理，存在真的、不可證明的命題。因為形式體系與Turing機本質上是等價的。因而這些命題不能由機器證明。
但是人可以證明這些命題。所以人的思維不能被機器或者一個公理體系充分表達。因而人不是會計算的機器，所有的機器也不能擁有和人一樣的智力。
上述論證中的每一個都可以承認，除了最後的結論。
Penrose的書出版於1989年。但是Turning早在1947年就已經指出上述論證的錯誤。事實上，Godel不完備定理需要的條件：體系的內部一致性。然而人類是極其容易犯錯誤的。人類的直覺極易犯錯。比如那些最牛的邏輯學家：Frege,Curry,Church,Rosser先後提出了龐大的公理體系，但是後來被證明是錯誤的。如果允許電腦犯錯，那么Godel定理的條件不再成立，其結論也就沒有意義了。
《皇帝新腦》
附，順便說幾句Penrose的《皇帝新腦》一書。
Penrose的《皇帝新腦》一書，出版於1989年，中文版出版於1993年。中文版的前言稱該書的出版是國際書界的一件大事，劍橋大學在幾年後曾專門為此書召開了一次學術會議。本書的內容從人工智慧、邏輯到物理學、宇宙學以及神經科學，當然還有哲學。Penrose的目標是討論哲學、科學上最重大的問題之一，人類的意識問題。Martin.Gardner為此書寫的前言中稱Penrose的書，是到該書出版為止，對於強人工智慧做出的最有力的攻擊。 Penrose極力反對強人工智慧。強人工智慧認為機器可以具有人的意識和智慧型。弱人工智慧認為機器可以表現得像一個人，但是不具有人的意識和智慧型。還有一種更強的觀點，聲稱人就是一台機器。Penrose對於強人工智慧的攻擊從幾個方面進行。其一，基於Searle中文屋子這個思想試驗。其二，基於 Godel不完備性定理。Penrose又一次展示了大無畏的革命精神。對於Penrose的論證，我只有一個評語：慘不忍睹。有興趣的讀者可以自己去翻閱該書的前幾章，並以挑出其中的邏輯漏洞來訓練自己的推理能力。當然效果不一定好，因為那些漏洞比較簡單。難以想像Penrose為什麼老犯這些低級錯誤。
而那些數理邏輯專家則見獵心喜，有不少針對Penrose的反駁意見。首先，Penrose是大人物，對之搞批鬥很有意義；其次， Penrose犯了低級錯誤，批判起來容易。這和物理學家批判Penrose的粒子物理，何其相似。簡直都有點搞笑了。
Penrose引用的Searle中文屋子的思想試驗被Martin.Davies在《邏輯的引擎》一書的最後一章批得體無完膚。而他基於Godel不完備定理的論證又被Turning早在40年前就批判了。真的很慘。
通常很多人認為Godel定理中的那個命題是很抽象而且不能具體寫出來的。這是嚴重的錯誤。在基本算術體系中，可以明確地寫出來一個真的但不可證明的命題。比如Goodstein定理。可參考
http://www.answers.com/topic/goodstein-s-theorem
我們在所有的帖子中都在使用“構造”這樣的說法，並一直在解釋這是形式體系中“證明”一詞的真正含義。構造，也可以叫做，算法，二者表達的是同一個含義，都表示在有限多個步驟之後得到結論。
荒謬推論
荒謬的推論1
Hawking等人認為，Godel不完備性定理表明終極理論是不可能的。Hawking的錯誤比起Penrose來更加不著邊際，看起來就像犯了不完備恐懼症，或者可以叫做不完備焦慮症。物理學甚至數學都不是形式體系，Godel定理的條件並不滿足。Hawking的觀點可以參考其本人在2002年的 Dirac講座上的演講
Hawking, "Gödel and the end of physics"
然而Hawking不是孤立的，Freeman Dyson持有類似觀點。Freeman Dyson在紐約書評上為Brian Greene的The Fabric of the Cosmos寫道：
Gödel’s theorem implies that pure mathematics is inexhaustible. No matter how many problems we solve, there will always be other problems that cannot be solved within the existing rules. … because of Gödel's theorem, physics is inexhaustible too. The laws of physics are a finite set of rules, and include the rules for doing mathematics, so that Gödel's theorem applies to them. [NYRB,May 13, 2004].
按照Dyson的論證，很容易推論出TOE是不存在的。
又比如Scientific America的一個senior, John Horgan在其所著The End of Science一書中寫道：
Gödel's theorem denies us the possibility of constructing a complete,consistent description of physical reality.
以及Stanley L. jaki, A Late Awakening to Gödel in Physics.
我反對這些人的論證，並不代表贊同有一個TOE. 僅僅是想表明，Godel定理不蘊含這些誇張的推論。
荒謬的推論2
有人認為，Godel定理給出了人類知識的絕對上限。對此，可以對比Heisenberg不確定原理。Heisenberg不確定原理給出了人類對於世界的認識的一個絕對的界限嗎？沒有。因為那就是世界的本來面貌。客觀世界的不確定性與我們測不測沒有任何關係。
荒謬的推論3
有人認為，Godel定理告訴我們有一些真的數學定理是永遠無法證明的。甚至有人猜測Goldbach猜想或者Riemann假設就是這樣的命題。想一想在Wiles之前有不少人把Fermat問題也作為其中的一個命題就知道這純屬無稽之談了。反面的例子，比如Gooodstein定理，這是一個被嚴格證明了的數學定理，但在形式系統中不可“證明”。
由於“存在不可證明的數學定理”，某些後現代主義據此懷疑客觀實在性。所以當我們在沾沾自得的用Godel不完備定理得到某些炫目的結論時，應該想到自己僅僅是全世界各種各樣的具有不完備情結的人之一。
基督教會則據此為自己辯護：theologians can be comforted in their failure to systematize revealed truth because mathematicians cannot grasp all mathematical truths in their systems either. 看來教會對數學家的評價很高嘛。不完備定理還被用來證明上帝的存在性，因為只有他能決定哪些是真理。然而我們也可以反過來使用不完備定理，並以此證明上帝不是全能的。
荒謬的推論4
Godel本人的錯誤。在1960的Gibbs講座上Gödel本人宣稱：“either mind infinitely surpasses any finite machine or there are absolutely unsolvable number theoretic problems.” 可以看出Godel使用了隱含假設：精神不能杯機器實現，然而這是無法證明的，至少Godel沒有給出一個可以和他的不完備定理的證明同樣堅實的證明。
這個系列基本上到此為止。一個簡單的後記。寫這個系列的一個原因是Godel定理本身是很有趣的，但遭到了廣泛的誤解和誇張。另外，寫這個系列是作為曾經計畫寫的一些其他內容，比如熱力學第二定律中的小機率這個部分以及機率論中的各種機率分布函式，並沒有完成，也沒有打算繼續寫這些相關內容。因而將 Godel定理的討論作為一個補償。Godel定理與其他領域也有關係，比如計算機理論特別是Turning機的停止問題，以及資訊理論中也有相應的表現形式。有興趣的讀者可以自己作進一步的了解，當然也可以發貼上來討論。
主要參考資料
http://www.cs.auckland.ac.nz/CDMTCS/chaitin/georgia.html
http://www.cscs.umich.edu/~crshalizi/notebooks/godels-theorem.html
http://www.ncsu.edu/felder-public/kenny/papers/godel.html
Penrose, The emperor’s new brain, 1989.
馬丁·戴維斯（美）,邏輯的引擎—第一推動叢書·第四輯.張卜天譯.
http://www.ltn.lv/~podnieks/gt1a.html#BM1_4
http://www.cscs.umich.edu/~crshalizi/notebooks/godels-theorem.html
http://www.answers.com/topic/goodstein-s-theorem
Stanley L. Jaki, A Late Awakening to Gödel in Physics
Stephen Hawking, "Gödel and the end of physics" http://www.damtp.cam.ac.uk/strings02/dirac/hawking/
劉新文,哥德爾的遺產及哥德爾百年紀念, http://www.logic-china.info/events/symposiums/2006-godel.htm
二零零七年三月三日 發表於繁星客棧
http://www.changhai.org/forum/
