論《數學原理》及相關系統中形式上不可判定的命題
在任何足夠豐富的算術系統中，都存在它永遠無法證明的真命題。
哥德爾證明：任何大到足以進行普通算術的規則手冊，都必定留下一些永遠無法被證明的真命題——而且，它永遠無法為自己擔保。
把這個想法拆開看
數十年來，數學家追逐著一個美麗的夢——常被稱作希爾伯特綱領：寫下一套嚴絲合縫的初始規則，使得原則上，關於數字的每一個真命題，都能僅憑一步步輾過這些規則而抵達。哥德爾證明，這個夢不可能實現。任何強大到足以處理普通算術的系統，都必定包含一些在它內部為真、卻無法被證明的命題。
他的方法，和他的結論一樣令人吃驚。他找到一種辦法，把每一個公式、每一個證明都變成一個數——於是「關於數字」的句子，可以暗地裡是「關於系統能證明什麼」的句子。憑藉這一點，他構造出一個語句，解碼後它說：「這句話在這裡無法被證明。」如果系統證明了它，系統就證明了一件假事；如果證不出，這句話就為真、卻夠不著。無論哪種情形，都有一道縫隙——而靠加規則去補，只會再裂開一道新的。
它從哪裡來
1930 年，在哥尼斯堡的一場會議上，24 歲的庫爾特·哥德爾，平靜地宣布了一個掀翻數學地基的結果——而就在此時，大衛·希爾伯特正重申著他那份自信滿滿的綱領，要把整個數學安放在確定的地基上。哥德爾的論文次年發表在維也納的一份期刊上，密布著一種讓算術談論自身的新技術。這一領域花了好些年才消化它；今天，它被公認為邏輯史上最重要的定理之一。
它為何重要
哥德爾為「證明所能做到的事」劃下了一道永久的界線。沒有任何形式系統，能同時做到完備、相容、又能為自己背書——一個令人謙卑的極限，同時重塑了數學與哲學。而它核心處那記妙招——被嚴格化了的自指——也成了計算機科學的種子：同一個想法表明，有些問題，任何程式都永遠解不開。
一句絆倒自己的話
想想那句古老的悖論：「這句話是假的。」若它為真，它就是假的；若它為假，它就是真的——它永遠打轉。哥德爾的天才，在於換掉了一個詞：他的句子說的不是「假的」，而是「不可證」。這小小的一改，把一個無用的悖論變成了一條精確的定理——那句話最終為真，卻不可證。在下方親手把它造出來，看著陷阱合攏。
你會在哪裡再遇見它
哥德爾的自指，迴響遠在邏輯之外。它是阿蘭·圖靈那個證明的直系祖先——沒有任何程式，能在一般情形下判定另一個程式會不會停機，這是理論計算機科學的基石；而每當一項任務被證明「無法自動完成」時，它的影子便會浮現。這也正是為什麼：沒有任何一套規則，無論多麼精巧，能成為數學真理的最終定論。
數學的形式化
定理 VI——不可判定的命題
To every ω-consistent recursive class κ of formulae there correspond recursive class-signs r, such that neither v Gen r nor Neg (v Gen r) belongs to Flg(κ) (where v is the free variable of r).
一個斷言自身不可證的命題
The analogy of this argument with the Richard antinomy leaps to the eye. It is closely related to the “Liar” too; for the undecidable proposition [R(q); q] states that q belongs to K, i.e. … that [R(q); q] is not provable. We are therefore confronted with a proposition which asserts its own unprovability.