博文
正面回击：哥德尔定理和西蒙的哲学（3）
精选
|||
(3)哥德尔不完备定理和它们的证明思路
对这个证明一直也没有太大兴趣。因为争论，刚刚浏览了一本书《哥德尔证明》，作者是欧内斯特·内格尔（Ernest Nagel） 和 詹姆士 R. 纽曼 （James R. Newman）。这本书写得非常浅显清楚，有兴趣的朋友可以下载。
必须指出，哥德尔不完备定理和“数学的真理性”没什么关系，所以拿出逻辑命题来扯毫无必要。而郑波尽博主提出用哥德尔定理来充计算机科学的当家花旦，只说明我们的计算机科学家离真正的生生不息的信息时代距离遥远。而程代展老师说：“任何数学体系均有它既不能证明也不能证伪的命题。”，则实在是夸大了哥德尔的工作。
书接上回，言归正传。
数理逻辑的目标，是建立推理的自动化过程，即把我们的推理过程变成计算机的运算过程。这一点正好和数学家们想通过演算的方式来建立一般化的定理证明的目标相契合-1931年，显然不是一个可以真正建立机器证明的时代。
“事实上，这正是二十世纪初在数学家们心中的普遍信念必然会存在某种固定的，严格的规则集合，用一个完全不用思考的自动机，能够完全机械地产生所有的数学真理。数学家们为什么会相信这个？因为他们是证明概念的信奉者，而在十九世纪，证明概念的焦点变得越来越清晰，所谓一个证明似乎就是在一个形式公理系统内部进行严格符号操作而得到的必然结果。”（见《哥德尔证明》一书）把数学推导过程变成算数演算过程，是信念似的东西，在1900年，Hilbert在其著名的23个问题中，第六条甚至雄心勃勃地提出将物理学体系公理化。
这是个我们比较容易理解的想法：一个学科的体系，最基础的基石是一些公理-它们在非数学的学科也被称为定律，然后借助一些基本概念，采用形式逻辑进行推导，就可以得到这些个公理盖含的所有定理。这一点在欧式几何中体现得既清楚又美妙。虽然我们并不确知一个学科的所有定理-它们也许有无穷多-但是我们可以在公理的基础上进行证明，换言之，我们就剩下了定理证明的工作。进而言之，如果我们能够将证明过程变成算算术，变成加减乘除，只要不是无限多步运算，自是妙不可言。
但是，这个想法在1931年被哥德尔打破了。哥德尔证明了以下两个被统称为“哥德尔不完备性定理”的定理（摘自wikipedia中文版）：
Any effectively generated theory capable of expressing elementary arithmetic cannot be both consistent and complete. In particular, for any consistent, effectively generated formal theory that proves certain basic arithmetic truths, there is an arithmetical statement that is true,[1] but not provable in the theory (Kleene 1967, p. 250). （wikipedia上英文比较清楚，但是要需要解释的太多，就不翻译了）
For any formal effectively generated theory T including basic arithmetical truths and also certain truths about formal provability, if T includes a statement of its own consistency then T is inconsistent. （wikipedia上英文比较清楚，但是要需要解释的太多，就不翻译了）
这里，必须解释一下几个概念：
形式化：不论公理和定理，它们都是用断言或者命题表述的。这些断言和命题，我们都要把它们写成公式，这是命题的形式化；而推导的规则，我们也要将它们形式化，变成公式，这是规则的形式化。
形式体系：是从一组公理出发，通过形式化的推导办法（就是把“依靠逻辑推理的数学证明过程”变成“算算术”），生成了若干定理，由这些公理和定理合起来构成的整个体系叫形式体系。特别需要强调的，是我们先会假定这些公理或者定律，是“真”的。而如果我们使用形式化的推导办法，主要是推出“真”的定理。换言之，我们说这些形式化的推导是“保真”的。
相容性：相容性是从公理出发，指依靠形式化的推导办法（就是把“依靠逻辑推理的数学证明过程”变成“算算术”），我们不能推出有一个定理既是“真的”，而与此定理相反的断言也是“真的”。比如在某个形式化的断言表明“陈安歌唱得好”是真的，那么另一个形式的断言表明“陈安不是歌唱得好”，则这个关于陈安的形式体系就是"不相容"的,也可以说这个形式体系是没有“一致性”的。
完备性：如果不用集合论，这个解释比较复杂。简单地说，就是如果在一个形式体系中存在一个关于某个断言的"真""假"判断，也就应该存在一个形式上含义相反的断言的"真""假"判断。比如，在一个形式体系中如果存在“蒋科学是吃素的”的“真”“假”判断，就应该存在“蒋科学不是吃素的”的“真”“假”判断，否则这个形式体系就是不完备的。
皮亚诺算数公理：是一组关于自然数的生成规则的公理，很容易查到，就不讲了。
关于哥德尔定理的证明，非常纷繁复杂，来回绕圈，据说当他证明完了，只有几十个人能看懂。我也没找到原稿，也不准备去“看懂”。这里只是简单说说他的证明办法。某个使用了皮亚诺算数公理的形式体系，其生成过程所用到的规则也会被形式化（否则我们就没办法让机器自动化了），而那些形式化了的规则，变成了"算术",我们称为“元数学”。既然这个“元数学”是“算术”，当然就变成了包含皮亚诺算术公理的形式体系。哥德尔巧妙地利用了要处理的形式体系和“元数学”上的形式体系，构造了一个悖论。最后利用这个悖论，给出了他的证明。
有兴趣的朋友可以参考我给出的书。
行文至此，就可以明白，我为什么说：
（1）形式化的公理体系含有内在的矛盾性（哥德尔对悖论的利用）。
（2）哥德尔的理论是关于形式化的公理体系的，是数学上的一个分支，与“数学的真理性”没什么关系；扯“数学的真理性”不要来扯数理逻辑。
（3）有很多学计算机的，从事信息行业的朋友，估计就没几个人关心这么个钻牛角尖的定理。所以这定理远远谈不上是个当家花旦。
（4）可以清楚地看出，定理的成立是靠“皮亚诺算术公理”的，所以程代展老师把事说大了。而且，百度一下就知道，欧式几何公理系统在一阶逻辑下就是相容且完备的。
（敬请期待下一篇。）
----------------------------讨论-----------------------------------
对研讨有意义的回复（1） [17]SN20111212此文和其它先发表的有关博文所讨论问题的出典如下：
B. A. W. Russell, "The Principles of Mathematics," Cambridge University Press, 1903.
A. N. Whitehead and B. A. W. Russell, "Principia Mathematica," 3 volumes， Cambridge University Press, 1910-1913. (通称PM)
B. A. W. Russell, "The Philosophical Importance of Mathematical Logic," The Monist，Volume 23, Issue 4, Pages 481-493, October 1913.
关于介绍哥德尔不完全性定理的现代专业书籍，到amazon上去大概很容易找到，恕不一一列举了。
关于所讨论问题的最早，最好的中文文献，本人认为是：
王浩，“数理逻辑通俗讲话”，科学出版社，1981.
王宪钧，“数理逻辑引论”中的第三篇，北京大学出版社，1982.
你至少先认真读读上面两篇中文文献，就自然能够了解到哥德尔不完全性定理的来龙去脉，认识到其内涵远比通常那些不求甚解的胡乱解释深刻的多。
----------------
【作者说明】关于罗素的文献，网上没有搜到，但是找到一篇介绍罗素思想的PDF，如下。其中特别谈到了罗素悖论和罗素对一阶逻辑的贡献。
https://blog.sciencenet.cn/blog-731678-664470.html
上一篇：正面回击：哥德尔定理和西蒙的哲学（2）
下一篇：围观：关于相对论的比赛终于开始了
扫一扫，分享此博文