【专栏】康托尔、哥德尔、图灵——永恒的金色对角线（8）

哥德尔的不完备性定理

然而，漫长的Y Combinator征途仍然并非本文的最终目的，对于Y combinator的构造和解释，只是给不了解lambda calculus或Y combinator的读者看的。关键是马上你会看到Y combinator可以由哥德尔不完备性定理证明的一个核心构造式一眼瞧出来！

让我们的思绪回到1931年，那个数学界风起云涌的年代，一个名不经传的20出头的学生，在他的博士论文中证明了一个惊天动地的结论。

在那个年代，希尔伯特的数学天才就像太阳的光芒一般夺目，在关于数学严格化的大纷争中希尔伯特带领的形式主义派系技压群雄，得到许多当时有名望的数学家的支持。希尔伯特希望借助于形式化的手段，抽掉数学证明中的意义，把数学证明抽象成一堆无意义的符号转换，就连我们人类赖以自豪的逻辑推导，也不过只是一堆堆符号转换而已（想起lambda calculus系统了吧)。这样一来，一个我们日常所谓的，带有直观意义和解释的数学系统就变成了一个纯粹由无意义符号表达的、公理加上推导规则所构成的形式系统，而数学证明呢，只不过是在这个系统内玩的一个文字游戏。令人惊讶的是，这样一种做法，真的是可行的！数学的意义，似乎竟然真的可以被抽掉！另一方面，一个形式系统具有非常好的性质，平时人们证明一个定理所动用的推导，变成了纯粹机械的符号变换。希尔伯特希望能够证明，在任一个无矛盾的形式系统中所能表达的所有陈述都要么能够证明要么能够证伪。这看起来是个非常直观的结论，因为一个结论要么是真要么是假，而它在它所处的领域/系统中当然应该能够证明或证伪了（只要我们能够揭示出该系统中足够多的真理）。

然而，哥德尔的证明无情的击碎了这一企图，哥德尔的证明揭示出，任何足够强到蕴含了皮亚诺算术系统（PA）的一致（即无矛盾）的系统都是不完备的，所谓不完备也就是说在系统内存在一个为真但无法在系统内推导出的命题。这在当时的数学界揭起了轩然大波，其证明不仅具有数学意义，而且蕴含了深刻的哲学意义。从那时起这一不完备性定理就被引申到自然科学乃至人文科学的各个角落…至今还没有任何一个数学定理居然能够产生这么广泛而深远的影响。

哥德尔的证明非常的长，达到了200多页纸，但其中很大的成分是用在了一些辅助性的工作上面，比如占据超过1/3纸张的是关于一个形式系统如何映射到自然数，也就是说，如何把一个形式系统中的所有公式都表示为自然数，并可以从一自然数反过来得出相应的公式。这其实就是编码，在我们现在看来是很显然的，因为一个程序就可以被编码成二进制数，反过来也可以解码。但是在当时这是一个全新的思想，也是最关键的辅助性工作之一，另一方面，这正是“程序即数据”的最初想法。

现在我们知道，要证明哥德尔的不完备性定理，只需在假定的形式系统T内表达出一个为真但无法在T内推导出（证明）的命题。于是哥德尔构造了这样一个命题，用自然语言表达就是：命题P说的是“P不可在系统T内证明”（这里的系统T当然就是我们的命题P所处的形式系统了），也就是说“我不可以被证明”，跟著名的说谎者悖论非常相似，只是把“说谎”改成了“不可以被证明”。我们注意到，一旦这个命题能够在T内表达出来，我们就可以得出“P为真但无法在T内推导出来”的结论，从而证明T的不完备性。为什么呢？我们假设T可以证明出P，而因为P说的就是P不可在系统T内证明，于是我们又得到T无法证明出P，矛盾产生，说明我们的假设“T可以证明P”是错误的，根据排中律，我们得到T不可以证明P，而由于P说的正是“T不可证明P”，所以P就成了一个正确的命题，同时无法由T内证明！

如果你足够敏锐，你会发现上面这番推理本身不就是证明吗？其证明的结果不就是P是正确的？然而实际上这番证明是位于T系统之外的，它用到了一个关于T系统的假设“T是一致（无矛盾）的”，这个假设并非T系统里面的内容，所以我们刚才其实是在T系统之外推导出了P是正确的，这跟P不能在T之内推导出来并不矛盾。所以别担心，一切都正常。

那么，剩下来最关键的问题就是如何用形式语言在T内表达出这个P，上面的理论虽然漂亮，但若是P根本没法在T内表达出来，我们又如何能证明“T内存在这个为真但无法被证明的P”呢？那一切还不是白搭？

于是，就有了哥德尔证明里面最核心的构造，哥德尔构造了这样一个公式：

N(n) is unprovable in T

这个公式由两部分构成，n是这个公式的自由变量，它是一个自然数，一旦给定，那么这个公式就变成一个明确的命题。而N则是从n解码出的货真价实的（即我们常见的符号形式的）公式（记得哥德尔的证明第一部分就是把公式编码吗）。”is unprovable in T”则是一个谓词，这里我们没有用形式语言而是用自然语言表达出来的，但哥德尔证明了它是可以用形式语言表达出来的，大致思路就是：一个形式系统中的符号数目是有限的，它们构成这个形式系统的符号表。于是，我们可以依次枚举出所有长度为1的串，长度为2的串，长度为3的串…此外根据形式系统给出的语法规则，我们可以检查每个串是否是良构的公式（well formed formula，简称wff，其实也就是说，是否符合语法规则，前面我们在介绍lambda calculus的时候看到了，一个形式系统是需要语法规则的，比如逻辑语言形式化之后我们就会看到P->Q是一个wff，而->PQ则不是），因而我们就可以枚举出所有的wff来。最关键的是，我们观察到形式系统中的证明也不过就是由一个个的wff构成的序列（想想推导的过程，不就是一个公式接一个公式嘛）。而wff构成的序列本身同样也是由符号表内的符号构成的串。所以我们只需枚举所有的串，对每一个串检查它是否是一个由wff构成的序列（证明），如果是，则记录下这个wff序列（证明）的最后一个wff，也就是它的结论。这样我们便枚举出了所有的可由T推导出的定理。然后为了表达出”X is unprovable in T”，本质上我们只需说“不存在这样一个自然数S，它所解码出来的wff序列以X为终结”！这也就是说，我们表达出了“is unprovable in T”这个谓词。

我们用UnPr(X)来表达“X is unprovable in T”，于是哥德尔的公式变成了：

UnPr(N(n))

现在，到了最关键的部分，首先我们把这个公式简记为G(n)——别忘了G内有一个自由变量n，所以G现在还不是一个命题，而只是一个公式，所以谈不上真假：

G(n):UnPr(N(n))

又由于G也是个wff，所以它也有自己的编码g，当然g是一个自然数，现在我们把g作为G的参数，也就是说，把G里面的自由变量n替换为g，我们于是得到一个真正的命题：

G(g):UnPr(G(g))

用自然语言来说，这个命题G(g)说的就是“我是不可在T内证明的”。看，我们在形式系统T内表达出了“我是不可在T内证明的”这个命题。而我们一开始已经讲过了如何用这个命题来推断出G(g)为真但无法在T内证明，于是这就证明了哥德尔的不完备性定理。

哥德尔的不完备性定理被称为20世纪数学最重大的发现（不知道有没有“之一”）现在我们知道为真但无法在系统内证明的命题不仅仅是这个诡异的“哥德尔命题”，还有很多真正有意义的明确命题，其中最著名的就是连续统假设[1]，此外哥德巴赫猜想也有可能是个没法在数论系统中证明的真命题。

【注释】

[1]在数学中，连续统假设是关于无限集合的可能大小的假设，这一假设是由康托尔于1877年提出。

（待续；此文的修订版已收录《暗时间》一书，由电子工业出版社2011年8月出版。作者于2009年7月获得南京大学计算机系硕士学位，现在微软亚洲研究院创新工程中心从事软件研发工程师工作。）