上接《Y Combinator、lambda算子和不动点原理》 3. 哥德尔的不完备性定理 然而，漫长的 Y Combinator 征途仍然并非本文的最终目的，对于 Y combinator 的构造和解释，只是给不了解 lambda calculus 或 Y combinator 的读者看的。关键是马上你会看到 Y combinator 可以由哥德尔不完备性定理证明的一个核心构造式一眼瞧出来！ 3.1. 历史背景 让我们的思绪回到 1931 年，那个数学界风起云涌的年代，一个名不经传的 20 出头的学生，在他的博士论文中证明了一个惊天动地的结论。 在那个年代，希尔伯特的数学天才就像太阳的光芒一般夺目，在关于数学严格化的大纷争中希尔伯特带领的形式主义派系技压群雄，得到许多当时有名望的数学家的支持。希尔伯特希望借助于形式化的手段，抽掉数学证明中的意义，把数学证明抽象成一堆无意义的符号转换，就连我们人类赖以自豪的逻辑推导，也不过只是一堆堆符号转换而已（想起 lambda calculus 系统了吧：） ) 。这样一来，一个我们日常所谓的，带有直观意义和解释的数学系统就变成了一个纯粹由无意义符号表达的、公理加上推导规则所构成的形式系统，而数学证明呢，只不过是在这个系统内玩的一个文字游戏。 令人惊讶的是，这样一种做法，真的是可行的！数学的意义，似乎竟然真的可以被抽掉！另一方面，一个形式系统具有非常好的性质，平时人们证明一个定理所动用的推导，变成了纯粹机械的符号变换。希尔伯特希望能够证明，在任一个无矛盾的形式系统中所能表达的所有陈述都要么能够证明要么能够证伪。这看起来是个非常直观的结论，因为一个结论要么是真要么是假，而它在它所处的领域 / 系统中当然应该能够证明或证伪了（只要我们能够揭示出该系统中足够多的真理）。 然而，哥德尔的证明无情的击碎了这一企图，哥德尔的证明揭示出，任何足够强到蕴含了皮亚诺算术系统（ PA ）的一致（即无矛盾）的系统都是不完备的，所谓不完备也就是说在系统内存在一个为真但无法在系统内推导出的命题。这在当时的数学界揭起了轩然大波，其证明不仅具有数学意义，而且蕴含了深刻的哲学意义。从那时起这一不完备性定理就被引申到自然科学乃至人文科学的各个角落 … 至今还没有任何一个数学定理居然能够产生这么广泛而深远的影响。 3.2. 哥德尔不完备定理证明思路 哥德尔的证明非常的长，达到了 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 之 内 推导出来并不矛盾。所以别担心，一切都正常。 3.3. 哥德尔的证明方法 那么，剩下来最关键的问题就是如何用形式语言在 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 内证明，于是这就证明了哥德尔的不完备性定理 [8] 。 哥德尔的不完备性定理被称为 20 世纪数学最重大的发现（不知道有没有 “ 之一 ”:) ）现在我们知道为真但无法在系统内证明的命题不仅仅是这个诡异的 “ 哥德尔命题 ” ，还有很多真正有意义的明确命题，其中最著名的就是 连续统假设 ，此外哥德巴赫猜想也有可能是个没法在数论系统中证明的真命题。 3.4. 从哥德尔公式到 Y Combinator 哥德尔的不完备性定理证明了数学是一个未完结的学科，永远有需要我们以人的头脑从系统之外去用我们独有的直觉发现的东西。罗杰 · 彭罗斯在 《The Emperor's New Mind》 中用它来证明人工智能的不可实现。当然，这个结论是很受质疑的。但哥德尔的不完备性定理的确还有很多很多的有趣推论，数学的和哲学上的。哥德尔的不完备性定理最深刻的地方就是它揭示了自指（或称自引用，递归调用自身等等）结构的普遍存在性，我们再来看一看哥德尔命题的绝妙构造： G(n): UnPr( N(n) ) 我们注意到，这里的 UnPr 其实是一个形式化的谓词，它不一定要说 “X 在 T 内可证明 ” ，我们可以把它泛化为一个一般化的谓词， P ： G(n): P( N(n) ) 也就是说，对于任意一个单参的谓词 P ，都存在上面这个哥德尔公式。然后我们算出这个哥德尔公式的自然数编码 g ，然后把它扔给 G ，就得到： G(g): P( G(g) ) 是不是很熟悉这个结构？我们的 Y Combinator 的构造不就是这样一个形式？我们把 G 和 P 都看成一元函数， G(g) 可不正是 P 这个函数的不动点么！于是，我们从哥德尔的证明里面直接看到了 Y Combinator ！ 至于如何从哥德尔的证明联系到停机问题，就留给你去解决吧 :) 因为更重要的还在后面，我们看到，哥德尔的证明虽然巧妙至极，然而其背后的思维过程仍然飘逸而不可捉摸，至少我当时看到 G(n) 的时候， “ 乃大惊 ”“ 不知所从出 ” ，他怎么想到的？难道是某一个瞬间 “ 灵光一现 ” ？一般我是不信这一说的，已经有越来越多的科学研究表明一瞬间的 “ 灵感 ” 往往是潜意识乃至表层意识长期思考的结果。哥德尔天才的证明也不例外，我们马上就会看到，在这个神秘的构造背后，其实隐藏着某种更深的东西，这就是康托尔在 19 世纪 80 年代研究无穷集合和超限数时引入的对角线方法。这个方法仿佛有种神奇的力量，能够揭示出某种自指的结构来，而同时，这又是一个极度简单的手法，通过它我们能够得到数学里面一些非常奇妙的性质。无论是哥德尔的不完备性定理还是再后来丘齐建立的 lambda calculus ，抑或我们非常熟悉的图灵机理论里的停机问题，其实都只是这个手法简单推演的结果！ Reference [1] 《数学——确定性的丧失》 [2] 也有观点认为函数式编程语言之所以没有广泛流行起来是因为一些实际的商业因素。 [3] Douglas R.Hofstadter的著作《Godel, Escher, Bach: An Eternal Golden Braid》（《哥德尔、艾舍尔、巴赫——集异璧之大成》）就是围绕这一思想写出的一本奇书。非常建议一读。 [4] 《数学——确定性的丧失》 [5] 虽然我觉得那个系徽做得太复杂，要表达这一简洁优美的思想其实还能有更好的方式。 [6] 关于如何在lambda calculus系统里实现“+”操作符以及自然数等等，可参见 这里， 这里，和 这里。 [7] g9的blog（负暄琐话） http://blog.csdn.net/g9yuayon/ 上有一系列介绍lambda calculus的文章（当然，还有其它好文章:)），非常不错，强烈推荐。最近的两篇就是介绍Y combinator的。其中有一篇以javaScript语言描述了迭代式逐步抽象出Y Combinator的过程。 [8] 实际上这只是第一不完备性定理，它还有一个推论，被称为第二不完备性定理，说的是任一个系统T内无法证明这个系统本身的一致性。这个定理的证明核心思想如下：我们前面证明第一不完备性定理的时候用的推断其实就表明 Con/T -> G(g) （自然语言描述就是，由系统T的无矛盾，可以推出G(g)成立），而这个“Con/T -> G(g)”本身又是可以在T内表达且证明出来的（具体怎么表达就不再多说了）——只需要用排中律即可。于是我们立即得到，T里面无法推出Con/T，因为一旦推出Con/T就立即推出G(g)从而推出UnPr(G(g))，这就矛盾了。所以，Con/T无法在T内推出（证明）。 |
