/ Number Theory

哥德尔,语法,和围棋(上)

作者:Bill Wadge. 译者:Mr. Kua,2017.05.01


“上帝是存在的,因为数学是自洽的。魔鬼也是存在的,因为我们不能证明数学是自洽的。”

-- 安德烈·韦伊


在八十多年前,柯尔特·哥德尔证明了这样一个定理,用通俗的话说 -- 没有一套不变的事实(比如 23 + 14 = 37)和规则(比如 x + y = y + x )的集合能证实(或证伪)可数集上所有的算术定理。

这个结论,即著名的哥德尔定理,带来了数不胜数的直接和潜在影响。比如,这个定理表明没有任何计算机程序可以断定一条关于算术的陈述正确与否。这意味着我们永远都不会知道关于算术的一切,虽然随着时间的推移我们会知道的越来越多。然而,这个定理也表明,我们对于算术陈述的知识将不能纯靠操纵纯粹事实和纯粹的规则,还需要依赖其他的来源,比如实验。

更有趣的是:这种事实与规则的限制在其他领域也不断重复出现,包括游戏,自然语言甚至心理学。

你可能会问,对于像数学这样的纯理论学科来说,数学家们又能从实验中学到什么呢?虽然实验有它的用处,比如,有助于猜想的形成。但是没有被证明的猜想又怎能对数学知识的整体带来价值呢?

Ex falso quodlibet. - "from falsehood, anything (follows)"

这都依赖于我们应该如何定义“实验”。几乎所有传统的数学可以在一个叫做ZFC的公理系统中做出推演,有时候你可能需要用到“选择公理”(注2)。很明显,ZFC需要自洽,否则我们将自相矛盾地推演出任意(相反)的逻辑陈述 (注:参考“爆炸原理")。

然而哥德尔的工作暗示了,ZFC的自洽性无法在ZFC系统自身中得到证明;换句话说,ZFC的自洽性不是传统数学中可以引申出的定理。然而我们相信它的自洽性是存在的,因为我们自己就在使用ZFC。有那么多数学工作者能靠在ZFC系统下发表论文获奖拿奖金,如果ZFC是不自洽的,那么我们想证明什么就能证明什么,这奖金不是可以白拿么?所以我们强烈地倾向于认为ZFC是自洽的(误)。

但是,有人会说,相信不代表懂得。ZFC的自洽性不是真正的数学知识。那些从ZFC系统里的事实和规则推导出来的结果都也已经被污染了。所以,严格上来说,我们不应说我们“知道”四色定理的答案,尽管已经有了对该定理的证明,我们能做的也仅仅只是“相信”它。

既然证明ZFC自洽太难,我们只能从那些更简单的系统中寻找安慰,比如皮亚诺算术公理(PA)。PA包括了一些简单的规则,基本上就是一些算术操作符的归纳性定义。让我们回顾一下数学归纳法:要对所有的n证明P(n),首先证明P(0)为真,然后我们证明在P(n)为真的前提下可以推出P(n+1)为真。似乎很有道理也很可靠对不对?但是我们怎么证明数学归纳法真的可靠呢?

简单地说,我们知道归纳法可行因为(1)它看上去没错。(2)它从来没有出过错。(是不是感觉到了什么?)

这不是形式化的(Formal)的数学证明,我们只是调用了自己的直觉,相信自己的经验而已。

然而我认为我们还是有权利说归纳法是可靠的。因为同样地,我们在经验和直觉的基础上相信着万有引力定律,万有引力定律也从来没有失效过。

再举个例子,我们如何确定 x + y = y + x?甚至,我们如何确定23+14真的等于37?对于学习算数的儿童而言,这一切都不是如我们看起来那样显然。

换句话说,我们会发现,数学其实和物理一样都存在着经验主义的成分。ZFC已经存在了一个世纪,你可以认为我们使用ZFC就像做了一个世纪的实验。这个实验的假设存粹建立在ZFC是自洽的基础之上,一个世纪以来目前为止还没出过问题。

除了ZFC之外,还有其他形式化的集合论可以在其上建立数学理论。其中之一就是冯·诺伊曼-博内斯-哥德尔集合论,简称GB,它的优势是只有有限数量的公理(ZF虽然公理数目是无限的,但只有有限的公理模式)。GB集合论和ZF系统是等自洽的(如果其中一个是自洽的则其他都是),所以我们可以放心地使用它。

另外一个形式化系统是,奎因新基础集合论(NF), 其与ZFC并不等自洽,这意味着上文所说的世纪实验并不一定就是唯一真理。NF看起来似乎也不错,从未导出过矛盾的结论,但是我们使用它的经验远远少于ZFC,所以信心也就不那么足。

OK,你们可能不禁要问这些枯燥的东西跟博弈/自然语言/心理学有什么关系?让我们在下一篇博客中阐述吧!
(有余力的读者可以自己想象一下哟。)


注:文章开头引用韦伊的话不完全正确。


该译文由作者授权发布于此,在原文基础上有加注和删改,此为上篇。
原文地址(Original Link):https://billwadge.wordpress.com/2017/04/18/godel-grammar-go-the-limits-of-rules-and-facts/) ,