论《数学原理》及相关系统中形式上不可判定的命题
在任何足够丰富的算术系统中，都存在它永远无法证明的真命题。
哥德尔证明：任何大到足以进行普通算术的规则手册，都必定留下一些永远无法被证明的真命题——而且，它永远无法为自己担保。
把这个想法拆开看
数十年来，数学家追逐着一个美丽的梦——常被称作希尔伯特纲领：写下一套严丝合缝的初始规则，使得原则上，关于数字的每一个真命题，都能仅凭一步步碾过这些规则而抵达。哥德尔证明，这个梦不可能实现。任何强大到足以处理普通算术的系统，都必定包含一些在它内部为真、却无法被证明的命题。
他的方法，和他的结论一样令人吃惊。他找到一种办法，把每一个公式、每一个证明都变成一个数——于是「关于数字」的句子，可以暗地里是「关于系统能证明什么」的句子。凭借这一点，他构造出一个语句，解码后它说：「这句话在这里无法被证明。」如果系统证明了它，系统就证明了一件假事；如果证不出，这句话就为真、却够不着。无论哪种情形，都有一道缝隙——而靠加规则去补，只会再裂开一道新的。
它从哪里来
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.