Boole's New Proof of Gödel's Incompleteness Theorem

前些日子查资料的时候发现逻辑学家 George Boolos (不是 boolean 类型的 George Boole) 曾经给出过 Gödel 定理的一个新证明. 看了之后觉得十分有趣.

Review of Gödel's Proof¶

关于 Gödel 的原始证明, 网上已有许多解释, 如刘未鹏的这篇文章. 这里再从数理逻辑角度简单回顾一下, 因为 Boolos 的证明用了许多 Gödel 的思想.

证明的第一步是建立 Gödel Numbering, 也即建立一套编码系统, 使得形式系统中任意公式可与自然数一一对应. 这种思想及其方法在有了计算机的今天是十分轻易的, 在 Gödel 的文章里, 他用了不同素数表示形式系统中的最基本符号, 从而实现了这一点, 这种方法后来被称为 Gödel Numbering.

第二步是证明一大堆 "函数" 都可以利用形式语言表述, 或者更严格地说, 证明它们是 "primitive recursive (原始递归)". 这是论文的主要篇幅所在, 从最基本的形式语言符号出发, 一直列举了 46 个函数的符号表示. 中间给出了 的形式化, 意为数 对应的命题可被数 对应的证明过程所证明. 有了它, 就可以给出 的形式化, 意为数 对应的命题可以被证明; 另一个重要的函数是 , 意为数 对应的命题里, 将自由变元用 取代, 可得到 对应的命题. 如果用编程的思想, 我们可以和容易的想出, 这三个函数的确是原始递归的, 因为的确可以写个程序来计算它们, 不过当时还没有这些概念.

第三步, 使用对角线法, 构造自指命题, 创造悖论. 令命题:

其中 是一自由变元. 这时候, 我们看看 , 也即把 的 Numbering 代入 , 设得到 , 那么 如下:

但是 成立当且仅当 !! 所以以上公式改写后:

我们已经看见了 self-reference.. 只需稍加变形:

也即:

从而, 是系统内不可被证明的真命题. 证毕.

Hofstadter 的旷世神书 GEB 里包括了证明的第一与第三点的通俗有趣描述.

Boolo's Proof¶

Boolo 也在试图用形式符号表达函数, 他表达出了一个函数 : 数 可被长为 的公式所 "named (表示)".

这里他对 "named" 的定义是: 如果有变元 的公式 成立当且仅当 , 则说 表示了 .

公式的长度, 指的就是表达这个公式所用形式符号的个数. 结合 Gödel Numbering 方法, 显然它也是一个原始递归函数.

有了 之后, 很容易构造出 , 意为: 数 可被某个长度小于 的公式所 "named (表示)".

然后就可以构造出 : 是最小的无法被长度小于 的公式所表示的整数.

(看到这里有没有觉得很眼熟..)

设公式 的长度为 , 令公式 :

其中 为自由变元, 则 的意思是: 是最小的无法被 个字符所表示的整数.

但是由于我们的 "表示" 是有着良好定义的, 且长度有上界的所有公式可能表示出的数的总数显然是有限的, 因而 "最小的无法被 个字符所表示的整数" 是唯一存在的, 设它是 , 则 成立当且仅当 , 于是 表示了 . 但 长度才为 , 的长度一定比 小 (其实 也未必够, 但既然我们定义出了 Numbering, 那总是无所谓的), 根据 的定义, " 表示 " 是不可证明的命题, 但它是真命题.

Remarks¶

两个证明其实都是在构造悖论. Gödel 证明使用了 Epimenides 悖论, Boolos 证明使用了 Berry 悖论. 通过形式化, 将悖论构造出来便可完成证明.

形式化的方法就是 Gödel Numbering 和形式化描述, 这两步是两人都用了的, 但这些步骤在有了计算机思想的今天是无比自然的.

Gödel 的第三步是巧妙的利用对角线法代换, 而 Boolos 并未使用对角线法. 他在它的那篇论文最后一段简洁地比较了两种方法的异同:

Both our proof and the standard one make use of Gödel numbering. Moreover, the unprovable truth in our proof and in the standard one can both be seen as obtained by the substitution of a name for a number in a certain crucial formula . There is, however, an important distinction between the two proofs. In the usual proof, the number whose name is substituted is the code for the formula into which it is substituted; in ours it is the unique number of which the formula is true.

In view of this distinction, it seems justified to say that our proof, unlike the usual one, does not involve diagonalization.

References¶

Gödel 1931 英文版 pdf: On formally undecidable propositions of Principia Mathematica and related systems I

Boolos 的论文: "A new proof of the Gödel Incompleteness Theorem"(1989), Notices of the American Mathematical Society 36: 388–90; 676.

我没找到 pdf, 但这篇论文收录在了 Boolos 的著作 "Logic, Logic, Logic" 中, 这本书有 pdf 可以搜到.

旷世奇书 GEB: Gödel, Escher, Bach: an Eternal Golden Braid