科学网 › 标签 › 哥德尔定理

标签: 哥德尔定理

相关帖子	版块	作者	回复/查看	最后发表

没有相关内容

相关日志

简化版哥德尔定理——逻辑学笔记33: mayaoji 2020-9-16 15:49; 个人分类: 逻辑学|3288 次阅读|0 个评论

贝里悖论和哥德尔定理——逻辑学笔记29: mayaoji 2019-5-1 12:46; 1、贝里悖论 “不可描述的感觉”，这个词本身描述了一种感觉，但它又说这种感觉是不可描述的，这里存在矛盾。贝里悖论是由英国的图书管理员贝里发现的，它和上面的例子类似。“不能用少于20个字确定的最小自然数”，这句话确定了一个自然数，但它本身又少于20个字，说明这个自然数能被少于20个字确定。 2、哥德尔定理数学命题不是真的就是假的，或者说不是正确的就是错误的。以往认为，对于真的命题我们总能证明它，即使我们暂时还证明不了，但理论上这样的证明总是存在的。哥德尔定理表明，存在着真的但又无法证明的命题。哥德尔在1931年实际上证明了，存在正确的算术命题，而这命题无法在算术中得到证明。麻省理工学院的逻辑学教授George Boolos于1989年给出哥德尔定理的一种新证明，这种新的证明参考了贝里悖论。 3、新证明的思路 “不能用少于20个字确定的最小自然数”，这句话不是数学命题。但Boolos将这句话翻译成算术命题，并且得到，这个命题是真的但无法在算术上证明它。和贝里悖论不同，这命题在数学上并不会导致矛盾。证明的思路如下。 Boolos 首先给出“ 确定 ”这个概念的数学定义：公式 G(x) 确定自然数 m ，当且仅当， ∀x( G(x) ↔x=m ) 是定理，即它可以在算术系统中证明。按照这个定义， 2x=4 确定 2 ，因为能够证明 ∀x(2x=4 ↔x=2 ) 。 Boolos然后构造出公式F(x)： ∃ y(y=10k∧A(x,y)) 它的意思是：x是不能用长度小于 10k 的公式确定的最小自然数（这个公式的细节在后面解释）。而公式 F(x) 本身的长度又小于 10k 。所以 F(x) 本质上和贝里的那个句子相同。令 n 是长度小于 10k 的公式无法确定的最小自然数，则 ∀x( F(x) ↔x=n ) 是真的。由于 F(x) 的长度小于 10k ，所以 n 无法由 F(x) 确定。按照确定的定义， ∀x( F(x) ↔x=n ) 不是定理。所以， ∀x( F(x) ↔x=n ) 是正确的算术命题，但无法在算术系统中证明。 4 、证明的细节 (1) 公式及其长度公式由联结词、量词、运算符、谓词、个体常元、个体变元和括号按合适的方式组合而成。公式的长度就是公式包含的符号数。联结词：﹁， → , ∧ ， ∨ ， ↔ 量词： ∀ ， ∃ 运算符：+，x 谓词：= 个体常元：0，S0，S00，…… 个体变元： x ， x’ ， x’’ ，…… 括号： ( ， ) 一共有 16 个符号。说明，上面的 0 就是通常的 0 ，而通常的 1 用S0表示，2用S00表示……。为了方便，后面仍用通常的表示方法，但要清楚它实际上是上面的符号。同样，为了方便我们用y和z表示变量 x’ 和 x’’ 。举个例子， ∀x ( x+1=y ) 是公式。这个公式的长度不是 9 ，而是 11 。因为 1 是 S0 ， y 是 x’ 。由于只有16个符号，对任一个自然数i，只有有限个长度为i的公式，也只有有限个长度小于i的公式。 (2) “确定”的性质如前面所述，“ 确定 ”的定义是这样的：公式 G(x) 确定自然数 m ，当且仅当， ∀x( F(x) ↔x=m ) 是定理，即它可以在算术系统中证明。容易证明，一个公式最多确定一个自然数。又由于只有有限个长度小于i的公式，所以存在不能被长度小于i的公式确定的自然数，而这些自然数中又有一个是最小的。即不能被长度小于i的公式确定的最小自然数是存在的。 (3)F(x) 的展开为什么 ∃ y(y=10k∧A(x,y)) 表示 “x是不能用长度小于 10k 的公式确定的最小自然数”呢？这里需要把 A(x,y) 展开。先引入 C(x,z) ， C(x,z) 表示“ x 可被某个长度为 z 的公式确定”。令 B(x,y) 为 ∃ z(zy∧C(x,z)) ，它表示“ x 可被某个长度小于 y 的公式确定”。令 A(x,y) 为﹁ B(x,y) ∧ ∀a(a x → B(a,y) ) ，它表示“ x 是不能被长度小于 y 的公式确定的最小自然数”。 F(x) 是 ∃ y(y=10k∧A(x,y)) ，即“ x 是不能被长度小于 10k 的公式确定的最小自然数”，其中 k 是 A(x,y) 的长度。 F(x) 的长度是多少呢？ 10 的长度是 11 ， k 的长度是 k+1 ， A(x,y) 的长度为 k ，其他为 9 ，所以 F(x) 的长度是 2k+21 。因为 k 大于 3 ，所以 2k+2110k 。所以 F(x) 的长度小于 10k 。证明还没有完成， C(x,z) 还需要进一步展开，或者需要证明 C(x,z) 能用算术公式表达。Boolos认为，利用哥德尔编码技术， C(x,z) 能够用算术公式表达。不过他省略了具体的证明，这里的证明应该是和哥德尔的原始证明类似的。; 个人分类: 逻辑学|3920 次阅读|0 个评论

认知逻辑和哥德尔定理——逻辑学笔记22: mayaoji 2017-7-1 20:18; 哥德尔第二不完全定理如果一个数学系统是协调的，那么它的协调性在那个系统里不可证。（协调就是无法推出矛盾的意思。）换句话说：如果它的协调性是可证的，那么将出现矛盾。下面这个推理题和哥德尔定理的证明有些类似。推理题逻辑之岛上有两种人：好人和坏人。好人只说真话，坏人只说假话。一天，一个游客来到逻辑之岛。岛上的某居民对他说：你永远不会相信我是好人。假设这个游客具有内省能力。什么样的内省能力？如果相信 p ，则相信自己相信 p 。举个例子。他相信地球是圆的，那他会相信自己相信地球是圆的。此外还具有完美的逻辑推理能力。游客会推出什么？下面我们来证明，假设游客相信自己不会相信矛盾，则他会相信矛盾。游客推理：如果我相信他是好人。那么我相信他说的是真话，那么我相信，我永远都不相信他是好人。而我相信他是好人，则我会相信我相信他是好人。所以如果假设我相信他是好人，将得到我相信，我相信他是好人和我不相信他是好人。这样我的信念就矛盾了。而我是不会相信矛盾的，所以假设错误，所以我不相信这居民是好人。游客接着推理：我不相信他是好人，而他也说我不相信他是好人，这说明他说的是真话，所以他是好人。推理到这里，由于游客具有反省能力，所以游客相信自己相信他是好人。游客继续推理：我相信他是好人，而他又说我永远不会相信他是好人，他的话是假话，所以他是坏人。这时，游客既相信他是好人，又相信他是坏人。信念矛盾了。所以，如果游客相信自己不会相信矛盾，那么他将相信矛盾。认知逻辑上面实际上证明了： B ﹁ B ⊥∧ B(p ↔ ﹁ Bp) ⇒ B ⊥ 它和下式等价：﹁ B ⊥∧ B(p ↔ ﹁ Bp) ⇒ ﹁ B ﹁ B ⊥ 上面的式子里 B 表示相信， p 表示那居民是好人，⊥表示矛盾。 p ↔ ﹁ Bp 表示：他是好人，当且仅当，游客不相信他是好人。推理时，除了经典命题逻辑的规则外，还加了 3 条规则： (1) 如果 A 是逻辑定理，那么 BA (2) 如果 B(p → q) ∧ Bp ，那么 Bq (3) 如果 Bp ，则 BBp 其中 (1) 和 (2) 表达的是完美的推理能力， (3) 是自省能力。上面的推理可以用符号严格地重写一遍。和哥德尔定理的联系将上面的 B 理解为“证明”。﹁ B ⊥∧ B(p ↔ ﹁ Bp) ⇒ ﹁ B ﹁ B ⊥表示的就是哥德尔第二不完全定理。在认知逻辑中直接引入 B 这个算子，但在哥德尔证明所用的数学系统中并没有这样的算子。他利用高超的技巧构造了“证明”这个谓词，同时证明了存在一个命题 p ，使得 p ↔ ﹁ Bp 是系统中的定理。他构造的命题 p 意思是这样的：本语句在本系统中无法证明。在做完这些构造性的工作后，后面的证明就简单了，其过程和上面的证明一样。参考资料： Raymond Smullyan ， Forever Undecided ： A puzzle guide to godel ， 1987; 个人分类: 逻辑学|4132 次阅读|0 个评论

哥德尔定理的证明——5殊途同归: 热度 13 xying 2013-6-3 06:56; 哥德尔定理说：不存在着一个自洽的形式公理系统，能够有效地证明这里面所有的算术真理。这个系统的无矛盾性，也不可能在系统里被证明。哥德尔定理被很多地方传述引用，表面看来是不同的说法。从上一篇的证明中，可以看出之间的联系。我们先谈内部的论断再谈外面的同类。首先，这是针对所有包含算术的形式公理系统。形式公理系统，指用形式化的一阶谓词逻辑来描述公式、命题和证明。这些逻辑演绎通常都用在自然语言表达的数学证明中，只是用符号形式化后更加明确严密，涉及到无限时十分谨慎和限制。这系统的提法，有的说包含“皮亚诺算术（ PA ）的公理”或说“一阶算术”，其实指的都是同一个东西。 PA 是最早研究的算术公理，是能够用一阶谓词表达的公理。包含了加法和乘法的形式公理系统，必须含有算术的公理。哥德尔虽然只在 PM 上证明了他的定理，很容易看到，他的结论也适用于所有包含了算术更大的系统。 “相容的”（ consistent ，或译为“一致的”或者“自洽的”）是数学系统最基本的要求，说明这个系统推出的结论不会自相矛盾。在科学发展的初期，研究都是基于直觉和经验，逻辑偶尔点缀其间只为理解内容，人们并不担心这个问题。随着微积分踏进了无穷的领域，悖论频现，数学家们看着这迅速增长的系统忧心忡忡，唯恐有朝一日发现，这只是场终归会自相矛盾的游戏，推理出来的怕只是一面之词。为此，相容性的证明便提到日程来。完备性（ completeness ，或译为“完全的”）则是要说明这个系统功能足够强大，对系统中的问题都能给个答案。这是第二位的期望。希尔伯特领导的形式公理化运动，希望如同形式逻辑系统一样，用形式化的方式，为数学建造一个严谨、清晰、相容且完备的系统。凡是用反证法证明的，都要在相容的系统假设下才能得到结论。不相容的系统，任何命题都能得证，这是平凡的完备。在相容的系统中，不完备性与存在着不可判定的命题等价。所以哥德尔的第一个定理，称“不完备性定理”或“不可判定定理”。有时哥德尔定理的表述中的条件是“ω - 相容的”而不是“相容的”。“ω - 相容的”在逻辑上是比“相容的”更强的要求。从前者可以推出后者。这是“每一个自然数都没有这性质”和“不存在着一个数有这性质”两者语义的差异，大多数人的理解，它们是相同。但是在形式系统中，因为没有一个能处理无限的规则，形式推理跨不过这个间隙。所以哥德尔的证明是用“ω - 相容的”来表述。定理中“相容的”表述，是 J Barkley Rosser 在 1936 年证明的更好的结果。为什么希尔伯特计划不包含着能够处理无限的规则？这要从“有限主义”的影响讲起。上个世纪初，一系列涉及到无穷的悖论将数学家弄得焦头烂额，有限的都是坚实可靠的，对无穷看法的分歧引起对数学基础的争论。因为无穷超越了想象，罗素提出将数学归结为逻辑，称为逻辑主义。与之对立的是直觉主义。最早的是克罗内克，他反对康托尔的实无穷，只接受整数，认为自然数是上帝创造的，直觉上清楚的。其他都是人造的，例如无理数没有一个构造方法或判定准则，不能用有限的步骤来确定，是可疑的。彭加勒嘲笑逻辑主义，认为这是将数学建立在无限的同语反复上，反对不能用有限个个体来定义的概念，用选择公理逐一从无限集合中选择是不可理解的。布劳威尔认为数学的基础只能建立在构造性的程序上，正确性和可靠性的决定是靠直觉而不是经验和逻辑。反对将有限经验总结的排中律推向无限的领域。布劳威尔和外尔只接受像数学归纳法那样，叙述进行中状态的潜无穷，反对像无穷集合和无理数那样，作为实体的实无穷。这个争论造成数学研究的分裂和混乱，直觉主义的主张将导致一批经典数学和数学分析的大部分成果失效，希尔伯特出自保卫无穷领域革命的成果，用行政手段压制了直觉主义。但是有限主义的疑虑，毕竟还是产生了影响，在希尔伯特计划里有两个原则，一是“形式化”，定义和推理抛弃了符号和规则之外的东西，形式地进行，这让数学清晰且严谨。这个形式公理化的思想被历史认同了。第二个是“有限化”，迷惘于由无穷产生的悖论，以及疑虑只凭逻辑思考不能验证之事的真实性，他希望有效的证明只用有限的步骤，每一步只涉及到有限个数学的对象。全称命题表达的规律对每一个对象都必须能够验证，存在的判断必须能给出一个特定的对象。有限制地在元数学上使用数学归纳法等等。【 2 】这些规则相当于原始递归的方法，被用在绝大多数能够被人认可的数学证明中。哥德尔看到“有限化”的局限性，他的定理说明，如此局限的系统必定是不完备的，甚至连自身的无矛盾性都不能证明。虽然他的证明不否定在 PM 之外的可能性，但对于不能映射到 PM 系统的“有限化”证明，还没有人知道是什么概念。【 3 】哥德尔定理之后，人们关心的是，我们能够证明系统的相容性吗？有完备的系统吗？这答案都是肯定的。逻辑系统的相容性很平凡，因为公理都是重言式，定理也是重言式了。其否定命题一定不是定理。对于包含算术的公理系统，哥德尔定理只说，在系统里不能证明其相容性，并不排斥在系统外的证明。 PM 的相容性，在 1936 年由甘岑（ Gerhard Gentzen ）用“超限归纳法”证明了。大多数数论逻辑家并不怀疑这个证明的正确性，但这个证明用的不是“有限的”方法，不能映射到 PM 中，超出了希尔伯特“绝对证明”的规定。人们最关心的是实数理论（数学分析）的无矛盾性，五十年代，日本学者将甘岑的工作推广到高阶谓词演算来探索， 1967 年，日本高桥元男用非构造的方法证明了数学分析子系统的相容性，由于这证明不是构造性的，数学分析的相容性至今还没有得到有效的证明。【 3 】很多系统不是完备的，这并不奇怪。例如，欧几里德几何在缺乏平行公设时，显然不是完备的。关键是经过扩充后，有没有可能让它完备化。一阶形式逻辑推理系统，比如说群论等一阶系统，可以是既相容又完备的系统。哥德尔在他的 1929 年博士论文，证明了一阶谓词逻辑的完备性定理。【 2 】但他的算术形式系统不完备性定理，杜绝了以扩充来完备它的希望。在一阶集合论的 ZF 系统中，由于可以定义自然数，所以也是不完备的。存在着不可判定的命题与不完备性是等价的。不从哥德尔定理出发，哥德尔 1940 年和 Cohen1960 年代的工作合起来，证明了连续统假设在 ZFC 集合公理系统中是不可判定的，选择公理在 ZF 集合公理系统中也是不可判定的。 1982 年美国帕里斯、哈林顿、弗里德曼相继在有限组合理论中找到既不能肯定也不能否定的关于自然数的命题。【 1 】【 2 】时至今日，人们用不同的方法，构造性了在现有系统中不可判定的一些命题，哥德尔定理得到了很好的验证。哥德尔的贡献在科学史上是罕见的，他以一人之力在短短的几年内，对一阶逻辑系统的完备性，数论和分析形式系统的完备性，选择公理的相容性等中心问题作出明确的解答。科学在长期演化中，某种思想到了一定时期必定成熟。 1931 年哥德尔发表了不完备性定理。几乎在同一个时间，波兰逻辑学家塔斯基（ Tarski ）在 1931 年送交了《形式化语言中的真理概念》论文。【 4 】塔斯基从理论语义学或逻辑语义学角度研究形式语言，回答了类似哥德尔的问题。塔斯基认为真理的定义，所要求满足的条件是“形式上正确、实质上充分”，这后者表达为，对于理论中所有句子的一个 T 范式（ Schema T ）： φ ↔ Tφ 。就 PM 系统而言，这范式说：数学命题可证，当且仅当这命题在数学上是正确的。他同样构造一个自我纠缠的例子，证明了塔斯基定理：任何包含一阶算术的理论，如果有 T 范式，它是不相容的。 1936 年英国数学家图灵研究抽象的计算模型，发表了图灵机的理论。图灵机是等价于任何有限逻辑数学过程的终极强大的逻辑机器。现代的电子计算机也可以看作是通用的图灵机。图灵机的停机问题是：能否有个程序判断任意一个程序，它是否在有限的时间内结束运行。他同样也是构造出一个自我纠缠的例子，证明这是不可能的。【 6 】塔斯基定理和图灵停机不可判定，都与哥德尔不完备性定理等价，相互间可以推证。哥德尔的不完备性定理，塔斯基的形式语言真理论，图灵机和停机判定问题，被称为现代逻辑科学在哲学方面的三大成果。这分别在数学形式系统，语义学和计算领域，研究数学证明能力，语言表达能力和机器计算能力，他们都应用和发展了递归理论，研究在有限或向无限进行中的逻辑推理，所（不）能到达的极限。无穷超越了人类理解的极限。在芝诺的悖论里，阿基里斯一直无法在逻辑上超越乌龟。【 7 】几千年来人类智力的进步解答了一部分的困惑，但它在不断被征服后，又屹立在那里，就像他们间的距离只是缩小而不是消除。每个人可能会有个梦中情人，现实中人们只可能在有限的时间里，接触到有限的人中搜寻，也许是终生无缘相遇。人们在潜无穷和实无穷的逻辑鸿沟两边相望，没有一座桥梁跨越。有限化的证明、计算和语言表达站在潜无穷这一边，自我纠缠无休止的自诘，意味着实无穷。难道这告诉我们：逻辑永远无法跨越潜无穷到达实无穷？（完）【参考资料】【1】 Wikipedia ， Gdel'sincompleteness theorems http://en.wikipedia.org/wiki/G%C3%B6del's_incompleteness_theorems 【2】哥德尔不完全性定理 ( 朱水林 ) http://ishare.iask.sina.com.cn/f/23413902.html 【3】数理逻辑的发展 http://www.kepu.net.cn/gb/basic/szsx/4/44/4_44_1014.htm 【4】张祥龙，塔斯基对于“真理”的定义及其意义 http://www.cnphenomenology.com/modules/article/view.article.php/24/c2 【5】 SEP Self-reference http://plato.stanford.edu/entries/self-reference/ 【6】维基百科，停机问题 http://zh.wikipedia.org/wiki/%E5%81%9C%E6%9C%BA%E9%97%AE%E9%A2%98 【7】应行仁科学网博文，阿基里斯与乌龟的悖论解决了吗？ http://blog.sciencenet.cn/blog-826653-642105.html; 个人分类: 科普|14822 次阅读|69 个评论

哥德尔定理的证明——4核心证明: 热度 6 xying 2013-5-30 07:34; 这篇介绍哥德尔证明的核心逻辑。你需要的不再是补充知识，而是澄明心思，清晰头脑，来跟上证明的思路。哥德尔有一套计算可形式化的“原始递归函数”理论，将元数学里的命题：“哥德尔数为 x 的公式序列，是哥德尔数为 z 公式的形式证明”，对应着算术计算，映射成 PM 里的公式。这个带有自然数变量 x 和 z 的公式简记为 Dem(x, z) 。 PM 里的公式原来只是无意义的字符串，无关真假，能够用演绎规则，从公理和其他定理产生出来的公式，称为定理，这个过程称为形式证明。将一些符号解释成逻辑关系，赋予公理真值，一些公式便有了逻辑的含义，称为命题，定理便是逻辑上为真的命题。将一些符号解释为算术符号，哥德尔的“对应引理”通过 PA 公理，建立起数论真理和算术命题的对应关系，因此赋予了这些公式的数学含义。元数学是在 PM 上层谈论公式性质和关系的语言。这里将不时地在元数学和 PM 两边说道、对应，你必须留意这一点，才不会被绕晕了。以后除非强调，元数学命题里谈到“证明”都是指在 PM 里的形式证明，有时也略去哥德尔数对应的说明，简略地说成：“ x 是 z 的证明”。这两个范畴间命题间的映射是形式与语义间的关系，对两边相同的逻辑运算保持着形式和语义的对应关系。哥德尔用 Dem(x, z) ，构造一个 PM 的公式 G ，它表达元数学的命题“公式 G 在 PM 内是不能被形式证明的。” 在构造新公式前，还需要介绍一个关于哥德尔数的函数表达式。假如在哥德尔数为 k 的公式中，有个自然数变量 y （哥德尔数是 17 ），将自然数 k 的 PM 表达（ SSS … SSS0 ）代入这公式中所有 y 变量出现的地方，这个新公式的哥德尔数记为 sub(k, 17, k) 。哥德尔努力显示这个置换操作是可计算的， sub(k,17, k) 是原始递归函数，它对应的 PM 字符串的表达式，记为 Sub(k, 17, k) 。比如说 k 对应的公式是“ ∃ x(x=Sy) ”，代入后的新公式 Sub(k, 17, k) 是“ ∃ x(x=SSSS … SSS0) ”（这里 SSSS … SSS0 有 k+1 个 S ），它的哥德尔数是 sub(k, 17, k) 。在 Dem(x, z) 前加一个存在的量词 ( ∃ x)Dem(x, z) ，对应着元数学里“存在着一个 x ，它是 z 的证明”，简言之，“ z 是可证的”。其否定式 ~( ∃ x)Dem(x, z) 对应着“ z 是不可证的”。将哥德尔数函数 sub(y, 17, y) 代入 ~( ∃ x)Dem(x, z) 中的 z ，有公式 1 ~( ∃ x)Dem(x, Sub(y, 17, y)) 这 PM 公式直接的含义是数学命题：“不存在着一个哥德尔数 x ，它满足 dem(x, sub(y, 17,y)) 的算术关系。”它对应着元数学里的命题：“哥德尔数为 sub(y, 17,y) 的公式是不可证的。” 设公式 1 所对应的哥德尔数是 n ，这是一个确定的自然数，将它代入公式 1 的变量 y ，便有公式 G ~( ∃ x)Dem(x, Sub(n,17, n)) 记哥德尔数 g = sub(n, 17,n) ，这也是一个确定的自然数。公式 G 对应着元数学里的命题：“哥德尔数为 g 的公式是不可证明。” 这 g 对应着哪个公式？ sub(n,17,n) 是置换操作后新公式的哥德尔数。这新公式是将哥德尔数为 n 的公式（即公式 1 ）里的变量 y 用 n 代入，这正是公式 G ！公式 G 的哥德尔数是 g 。因此，公式 G 对应着元数学里的命题：“公式 G 是不可证明的。” 公式～ G 即 ( ∃ x)Dem(x, Sub(n,17, n)) 则对应着元数学里的命题：“公式 G 是可证明的。” 我们已经把自我纠缠镶进了公式 G ！嘘一口气，慢慢消化这个公式和对应的含义。然后往下看这证明的辩驳。如果细心推敲，你可能会有些疑惑，这很正常，需要慢慢消化。哥德尔的证明手法很不寻常。当大数学家冯·诺依曼得知哥德尔证明时大为赞赏，细究之后，两次宣布找出了证明中的错误，后来他又两次修正了自己的错误。他惭愧地看到自己由这个插曲，轻易地改变了关于数学绝对真理的看法，而且相继改变了三次。哥德尔用反证法证明在 PM 里，公式 G 是不可判定的。假如公式 G 可证，这件事的元数学陈述是：“公式 G 是可证明的”， ~G 对应的正是这句话，说明它是可证的。反过来，假如 ~G 是定理，这公式对应的元数学命题“公式 G 是可证明的”为真，这元数学的判断是： PM 里可以证明公式 G ，即公式 G 是定理。因此，公式 G 是定理，当且仅当公式 ~G 是定理。【注】 PM 是相容时，这种情况是不允许的，所以上述导致矛盾的假设都不成立。 G 和 ~G 在 PM 里都不可证，也就是不可判定的。 G是不可证明的事实，说明元数学描写G的命题是真理，它对应着这公式 G 的含义为真。 PM 里一个表达真理的公式 G ，不能在 PM 里被证明，说明 PM 是不完备的。这（在元数学里）就证明了：定理1：PM如果是相容的（consistent）则是不完备的（incomplete）。在相容的 PM 里不可能判定 G 的真假，所以哥德尔这个定理有时叫做“不可判定定理”。是不是在 PM 里加上这个不可判定的命题作为公设，系统扩张后就可以让它完备起来？哥德尔说，这是不可能的！加上新的公理，按照相同的逻辑，还可以证明有新的不可判定的命题。这让公理化的原始设想完全落空。这定理简单的推论是：数论里有无穷多个真理不能用初等方法（数论里的公理和定理）来证明，不断引进数论外的定理后，总是还有不能用形式逻辑证明的数论真理。所以古老数论难题的解决，常常意味着带来新方法的突破。下面证明：相容性是不可能在 PM 里证明的。回顾一下“相容性”的含义，它说：系统里一个命题和它的否定不能同时是定理。这是数学系统无矛盾性的要求。如果不是这样，在系统里就可以证明任何的命题成立。所以“相容性”等价于“系统存在着一个命题，它是不可证明的。” 我们构造一个新的公式公式 A ( ∃ z)~( ∃ x)Dem(x, z) 这个公式对应着元数学的直接解读是：“存在着一个公式 z ，不存在着公式序列 x 是它的证明”；即“有一个公式，它是不可证明的”，即“ PM 是相容的”。公式 G 是否也有类似的解读呢？它的直接元数学的解读是：“公式 G 是不可证明的。”，我们已经从元数学证明：命题 G 是真的。它是真的又不能在 PM 里证明，这正是“ PM 是不完备的”的意思。所以，公式 G 的另一个解读是：“ PM 是不完备的。” 元数学里的定理 1 说：如果 PM 是相容的，则 PM 是不完备的。对应着 PM 里的公式： ( ∃ z)~( ∃ x)Dem(x, z) → ~( ∃ x)Dem(x, Sub(n, 17, n)) 也就是说，如果我们能够在 PM 里证明它是相容的， ( ∃ z)~( ∃ x)Dem(x, z) 公式为真，按照上式和 PM 里三段论推理的分离规则，推出 ~( ∃ x)Dem(x, Sub(n,17, n)) 为真，即在 PM 里证明了公式 G ，这与公式 G 在 PM 里是不可证的事实相矛盾，所以公式 A 不能在 PM 里被证明。这就有了定理2：PM不能证明自身的相容性（consistency）。（待续）【注】这里沿用了【 1 】里 PM 公式与元数学对应关系的简化证明思路。这里的定理 1 是 J Barkley Rosser 1936 年证明在相容条件下的较强结果。实际上这不是哥德尔 1931 年的证明。哥德尔证明的是：如果 PM 是ω - 相容的（ω -consistent ），则是不完备的。 “ω - 相容的”的定义是：对于算术谓词 P ，“ ( ∃ x)P(x) ”和每一个自然数 k 的“ ~P(k) ”不能同时为真。而“相容的”则是：对于任何命题 p 和 ~p 不能同时为真。“ω - 相容的”是个较强的要求，它能够推出“相容的”条件。“ω - 相容的”的定义里“ ~( ∃ x)P(x) ”（不存在着一个数有这性质）和每一个自然数 k “~P(k)” （每一个自然数都没有这性质）在语义理解上是同一回事，但在形式系统里，因为没有一个能处理无限的规则（希尔伯特计划中有限主义的限制），所以不能把它们看成是一样的。哥德尔的实际证明逻辑如下。假设 G 可证，这说明有个 PM 公式序列是 G 的证明，设这个公式序列的哥德尔数为 k ，这元数学命题对应着数论命题 dem(k, g) ，已知 g = sub(n, 17, n) ，所以有 dem(k, sub(n, 17, n)) ，它陈述了一个算术的事实，表示为 PM 的公式 Dem(k, sub(n, 17, n)) ，这说明它是 PM 里的定理。有一个具体的数 k 满足这关系，逻辑上说明存在着一个数 x 满足这关系，也就是 ( ∃ x)Dem(x, sub(n,17, n)) 能够被证明，这公式是 ~G 。这说明从 G 可证，可以推出它否定形式 ~G 也可证。从而，如果 PM 是相容的， G 在 PM 里不可证。假设 ~G 在 PM 里可证。如果 G 不可证，也就是对于所有的 k ， dem(k, g) 都不是事实的，即 ~dem(k,sub(n, 17, n)) 都是真的，所以 ~Dem(k, Sub(n, 17, n)) 对每一个的自然数 k 都是个定理， ~G 可证意味着 ( ∃ x)Dem(x, Sub(n, 17, n)) 是 PM 里的定理，如果 PM 是ω - 相容的，这是不可能的。从而，如果 PM 是ω - 相容的， ~G 在 PM 里不可证。因此，如果 PM 是ω - 相容的， G 是不可判定的。不可判定的命题，根据排中律， G 和 ~G 必有一真，但在 PM 里都不能证明它们，所以 PM 是不完备的。【参考资料】【1】内格尔和纽曼《哥德尔证明》 http://bbs.sciencenet.cn/home.php?mod=attachmentid=32962 【2】哥德尔不完全性定理 ( 朱水林 ) http://ishare.iask.sina.com.cn/f/23413902.html 【3】 Gdel's proof summary http://www.jamieyorkpress.com/wp-content/uploads/2012/04/G%C3%B6dels-proof-summary.pdf; 个人分类: 科普|15879 次阅读|16 个评论

哥德尔定理的证明——3哥德尔编码: 热度 11 xying 2013-5-27 07:05; 公理系统的不可判定命题、相容性和完备性问题是相联的。系统里的命题，如果既不可能证明它成立，也不可能证明与之相反的成立，这便是个不可判定的命题。相容的系统，不可能证明相反的一对命题同时成立。完备的系统，必须能够证明任何一对相反命题，必有一个成立。所以具有不可判定命题的系统，如果是相容的必定是不完备的。如果在 PM 里，能构造出这样一个自相矛盾的命题：若证明它成立，等同于证明相反的命题也成立。它就是个不可判定的命题。就证明了“哥德尔不可判定定理”，或者根据上面简单的推论就有“哥德尔不完备性定理”。 “这个命题是不可证明的”这句话，如果能放在 PM 里，它便在证明时自相矛盾。但这句话是元数学的命题。我们必须用一个映射，将这命题变换成 PM 里自涉的（ self-referent ）算术命题。歌德尔先用编码将 PM 里的公式一一映射成自然数（哥德尔数），这个数就好比是身份证的号码，唯一代表着那个公式，从公式角度来看这个数就是它自己。这个公式里如果包含了这个数和它的含义，就能够谈论自己。这一篇介绍这个哥德尔编码。前面说过，形式公理系统里的公式是由一组原始字符，按照形成规则构成的字符串，编码就是将字符串一一映射成一个自然数，称为哥德尔数。我们来看哥德尔是怎么编码的（这基本按哥德尔 1931 年论文的版本）。包含着皮亚诺算术公理的形式公理系统 PM ，有 12 个固定符号，分别对应着哥德尔数如下：符号～ V → ∃ = 0 S （）， + · 编码 1 2 3 4 5 6 7 8 9 10 11 12 含义非或得出存在等于零后继标点标点标点加乘公式在表中符号的含义解释下，具有逻辑和数学命题的含义，哥德尔“对应引理”证明了 PM 中原本只具有形式的定理，对应着其数学含义下的数论真理。不难看出，如果不再定义数字符号， n 个 S 的字符串 SSS…SSS0 的含义是自然数 n ，这字符串称为数 n 在 PM 的表达。继续说编码的规则。自然数变量 x ， y ， z ， … 的哥德尔数分别是 13 ， 17 ， 19 ， … 依序对应着大于 12 的质数。命题变量 p ， q ， r ， … 的哥德尔数是 13 2 ， 17 2 ， 19 2 ， … 依序对应着大于 12 的质数的平方。谓词变量 P ， Q ， R ，…的哥德尔数是 13 3 ， 17 3 ， 19 3 ，…依序对应着大于 12 的质数的立方。公式的编码是一组质数幂的乘积，这组质数的个数与公式中的字符数相等，从 2 开始依序列出前几个的质数，它的指数对应着相应位置上公式符号的哥德尔数。举例来说：公式“ ∃x(x=Sy) ”这里 8 个字符对应的哥德尔数依序是 4 ， 13 ， 8 ， 13 ， 5 ， 7 ， 17 ， 9 ，这公式的哥德尔数按照编码规则便是 2 4 3 13 5 8 7 13 11 5 13 7 17 17 19 9 ，它是一个很大的自然数。形式证明是由几个公式组成的序列，序列中每一个公式如果不是公理或已知的定理，都必须是由序列里前面的公式按变换规则生成的，证明的结果是序列中最后一个公式。形式证明的编码也与公式的编码规则类似，只不过其指数是对应着次序上公式的哥德尔数，举例来说：从“每个数有个后继数”用替换规则证明“零有一个后继数”，可以表示为两个公式的序列：“ ∃x(x=Sy) ； ∃x(x=S0) ”第一个公式的哥德尔数为 m ，第二个为 n 时，这个形式证明的哥德尔数是： 2 m 3 n ，也是一个自然数。更细致的解释见内格尔和纽曼《哥德尔证明》【 1 】。按照这样的编码，每一个公式或证明对应着一个哥德尔数。根据算术基本定理，每一个自然数可以分解成唯一的质数幂的乘积，依照质数指定的位置和其指数对应的字符或公式，哥德尔数可以解码出对应的公式或证明。这个编码规则建立起公式或证明，与（一部分）自然数的一一映射。每个哥德尔数通过这个一一映射，拥有它所对应字符串的信息。既然公式和证明的所有信息都在对应的哥德尔数上，那么讨论公式和证明，这些谈论字符串性质的元数学问题，便是一个数论的命题，就可能把它用公式表达出来【 2 】。比如一个元数学的命题说：“ ~(0=S0) ”是个否定式的命题。也就是判断它的第一个符号是“ ~ ”。这是个用自然语言表达的元数学命题，首先把它转化成数论的命题，然后用 PM 里的公式来表达。这个公式的哥德尔数是 2 1 3 8 5 6 7 5 11 7 13 6 17 9 ，符号“ ~ ”的哥德尔数是 1 ，公式的第一个符号是“ ~ ”，对应着公式的哥德尔数是 2 的 1 次方的因子。记这个数为 a ，那么这个元数学命题对应的数论命题是：“ a 整除于 2 ，且 a 不能整除于 4 。”前面说到，自然数 a 在 PM 里表达是有 a 个 S 的字符串“ SSS…SSS0 ”，“ a 整除于 2 ”等价于“存在着一个数 x ，有 a=2 · x ”，可以表示为： ∃ x(SSS…SSS0=x · SS0) ，这个数论命题不难用 PM 里的公式表示为： ~(~ ∃ x(SSS…SSS0=x · SS0)V( ∃ x)(SSS…SSS0=× · SSSS0)) ；这个直观的例子显示元数学上的命题，是怎样映射成 PM 里的公式。现在考虑证明中要用到的一个重要元数学命题：“公式序列 X 证明了公式 Z ”。我们知道在形式证明的公式序列里的公式有个的顺序规则，与公理、已知的定理、变换规则及被证明公式的对应有关。所谓的“证明”就是有限次地从前面的公式递推出后面的公式，这叫做递归。将公式对应成数后，“证明”就是这些数间的递归函数。假定公式序列 X 的哥德尔数是 x ，公式 Z 的哥德尔数是 z 。从这些关系不难想象出自然数 x 和 z 之间的算术关系，将这个算术关系记为“ dem(x, z) ”。哥德尔在论文中用了极大的努力证明了这个 dem(x,z) 是数 x 和 z 之间的“原始递归关系”，所以它可以形式地表示成一个 PM 的公式【 2 】，记为“ Dem(x, z) ”。我们已经将元数学的命题“ X 证明了 Z ”，映射成 PM 的公式 Dem(x, z) 。这完成了这一篇文章的目标。学习计算机的读者可能疑惑，为什么要这么麻烦地编码？这质疑有道理。哥德尔证明这个定理时在 1931 年，那时候还没有计算机，哥德尔在编码、递归函数、可表达性等问题上都做了开创性的贡献。这里介绍哥德尔编码，是沿着哥德尔原来证明的轨迹，了解这个经常会被人们提及的内容。现代的计算机实践经验，已经在人们头脑里形成了新的直观，对计算机理论有更多了解的，更能落实到这些直观背后充分的理论根据。有了这些直观，理解这些就很容易了。 PM 里的公式和证明，可以用任何一种编码（比如说 Unicode ）变成 0 和 1 的字符串，也就是一个自然数了。这个自然数也可以通过解码得出原来的公式和证明。这就建立起一一映射。这时候同样可以通过递归函数理论，将上述的“证明”语句表达为 PM 里的公式 Dem(x, z) 。也可以想象写一个程序，解码自然数 x 得出一个公式序列来，然后验证这序列是可以递推出自然数 z 解码所得的公式，把这个程序用 PM 里形式语言写出来，便是个 PM 里的公式。总之，我们可以把“ X 证明了 Z ”，映射成 PM 的公式 Dem(x, z) 。注意，表示式“ Dem(x,z) ”实际上不是 PM 里的式子，它只是一个方便的记号，联系了两个哥德尔数的变量x和z在一个公式里，我们用来代表 PM 里那个非常长的公式。怎么在这个 Dem(x, z) 代表的公式里做到自我纠缠，这个技巧将在下一篇的核心证明里介绍。（待续）【参考资料】【 1 】内格尔和纽曼《哥德尔证明》（中文版下载，谢谢徐晓） http://bbs.sciencenet.cn/home.php?mod=attachmentid=32962 【 2 】数论中有不可数多的命题，而 PM 只能有可数个式子，所以并非所有的数论命题都能表达成 PM 里的公式。哥德尔证明了原始递归函数可以表达成 PM 里的公式。; 个人分类: 科普|16538 次阅读|24 个评论

哥德尔定理的证明——2魔鬼的设计: 热度 10 xying 2013-5-23 08:01; 哥德尔要在形式公理系统里，放进一个“自我纠缠”的魔鬼，用系统里的公式表达“这个公式是不可证明的”含义，构造一个不可判定的命题。如果他做到了，这系统若是相容的就是不完备的（这不难推出，读者可以想一想）。他的想法来自于法国数学家理查德（ Jules Richard ） 1905 年的语义悖论。理查德悖论【 1 】【 2 】的一个变种是这样的：用语言描述一类自然数的算术性质。模仿公理化的方法，从基本概念开始，依定义过的内容来描述新的定义。这些定义的内容总是用有限个字符来表达。比如说，定义了整数，乘除法后，定义“（平方数）是某个整数的自乘”，“（质数）是只能被1和自己整除的数”等等。把这些定义按描述句子的长短和字典顺序排列成一个表，这里每一个定义，在表中的序号是一个自然数。例如“（质数）是只能被1和自己整除的数”的序号是19，“（平方数）是某个整数的自乘”的序号是50。对照定义和它的序号，不外乎有两种情况：一类是这序号恰好符合定义的描述，例如序号19（它是质数，有定义的性质）；另一类是这序号不具有定义性质的情况，例如50（不是平方数，没这性质），将这些不具有定义性质序号的数定义为“理查德数”。这样50是理查德数，19则不是。理查德数是在这系统中有明确数学性质定义的一类自然数，它的定义也可以在这表中，假设它的定义对应着序号n。问：n是不是理查德数？论证一下，若n不符合它所对应的定义，按照理查德数定义的描述，n应该是理查德数，这是说n是符合理查德数定义了，即n符合它所标号的定义，这就和初始的假设矛盾了。这个悖论说明：即使对自然数的算术性质，用任何语言（包括形式语言）来定义，也可能发生矛盾。这悖论有些疵瑕，但即使这个表长有限，矛盾仍在。重点是它与 1901 年的罗素悖论有着相同的逻辑结构—— self-reference ，而罗素悖论与谎言悖论都是因为自我纠缠惹得祸。罗素和一些人认为：如果把对象语言和讨论对象语言的“元语言”区分开来，就可以避免这个纠缠。谎言悖论“这句话是错的。”在区分后就有了两层的意思，一个是用对象语言表达的语句，另一个是从元语言角度来讨论用对象语言表达的语义，在各自层次里都是一个简单的陈述。从元语言层次，这句话的含义，是评判句中“这句话”，指的是对象语言层次的句子错了，对象语言层次的句子不能评价元语言层次的句子，这就避免了纠缠引起的矛盾。对于理查德悖论，分清层次后，按照算术的性质描述自然数，只能采用算术公理和算术运算的性质，理查德数的定义采用了有关算术性质的讨论，系统序号数和对应定义间的关系，这属于讨论数学性质的“元数学”（ Metamathematics ）【 3 】，不是数学层次的语言，所以它不应该出现在这表中。规定它们不能混在一起，就杜绝了这个悖论。在 PM 里，用公理、定义和逻辑符号构成字符串的式子描写了数学，对于这些数学性质的讨论，即对于这些字符串的讨论，诸如“这个命题是否定式的”，“字符串 x 是字符串 z 的证明”，“ z 是不可证明的”，“ PM 是相容的”等等，则属于元数学的范畴。希尔伯特用精确的形式语言构建的形式公理系统，已经严格区分数学和元数学，建立起隔离墙，堵塞了这个漏洞。哥德尔要把“这个公式是不可证明的”的句子放在系统里，就必须绕过这堵墙，将这元数学的句子转换成数学和逻辑的式子。我们来看这该怎么设计。首先要了解什么是 PM 中合法的式子。它是按一种形式语言写的字符串。写过计算机程序的人应该不难理解，因为 Basic ， C ， Java 等等，所有计算机语言都是形式语言。希尔伯特的形式公理系统里的式子，是按照《数学原理》的思想，用很基本一阶谓词逻辑的形式言语来写的字符串。系统根据演绎规则来操作这个形式语言的字符串。命题逻辑内容大家中学时都学过。谓词逻辑是命题逻辑的推广，在命题中可以带有变量，用谓词表述变量代表个体的性质和关系，可以用量词来约束变量，比如说，“存在一个数 x ， x 的自乘等于 4 ”，这里 x 是变量，“存在一个数”是量词，“的自乘等于 4 ”叫谓词，表达成式子是“ ∃x(x · x=SSSS0) ”，（ SSSS0 是数 4 在系统里的表达），只包含个体谓词和个体量词的谓词逻辑称为一阶谓词逻辑，简称一阶逻辑。包含 PA 的一阶逻辑系统称为一阶算术系统。这个大致的解释，让不熟悉数理逻辑的读者能够想象这些术语。下面假设读者已经有了数理逻辑的基本知识，这里通俗地介绍后面要用到一些术语和例子。这些式子只是作为例子，不必记忆。有数理逻辑知识的读者应该熟悉这些内容。不熟悉的，简单接受用字符串可以表达算术命题的事实，了解式子的含义和这些术语，可以略过其他的细节。读懂这系列科普只需要看懂这些式子表达的意思就行，不需要有深入的知识。（关于数理逻辑的简介见【 4 】，详细可看任何教科书有关“ 一阶谓词逻辑”部分。）在这个系统中首先给出一些原始符号， PM 包含 12 个固定符号：～ V → ∃ = 0 S （）， + · 和数字变量 x ， y ， … ，命题变量 p ， q ， … ，谓词变量 P ， Q ， … 等等，以及式子形成规则（ syntax ），说明怎么组成合格的字符串。这些符合语法规则的字符串，称之为“ 公式 ”，如：“ ~(0=S0) ”。系统中有一组初始的公式，称之为“ 公理 ”，两条变换规则：将公式代入变量的替换规则和三段论推理的分离规则，称之为“ 变换规则 ”。好比计算机解读程序产生输出的规则。由几个公式应用变换规则产生的字符串，也是个公式。若是从公理（和已知的定理）开始，由有限次演绎产生的公式，则称为“ 定理 ”，这个过程称为“ 形式证明 ”，简称为 “ 证明 ” 。这里的定理可能很平凡，只要能被形式证明的都是。 PM 里有 4 个逻辑公理 pVp → p ； p → pVq ； pVq → qVp ； (p → q) → (rVp → rVq) ；将这里的的“ V ”解释成逻辑上的“与”，“→”为“推出”，容易理解这些都是逻辑的规则。它们和变换规则一起，形成逻辑推理能力。皮亚诺算术（ PA ）的公理可以表达为下面 6 个数字公理和一个数学归纳法公理（见【 5 】）。 ~(0=Sx) ； Sx=Sy → x=y ； x+0=x ； x+Sy=S(x+y) ； x · 0=0 ； x · Sy=x · y+x ；将这里的“～”解释为“否定”，“ ∃ ”为“存在一个”，“ Sx ”为变量 x 所表示的数的直接后继数，（想象 x+1 ），其他的按算术中符号的约定，很容易理解这 6 个公理的含义。但这些含义只是便于理解的手段。形式公理系统不需要理解这些含义来演算，在这个系统中，只需要把这些公式看成没有意义的字符串，按照变换规则来得出新的字符串，进行形式性的运算。这些字符串并不代表着客观世界的事物，没有真假可言，这就是“形式”的意思。形式公理系统可以操作没有含义的字符串，但是公理集合可以赋予这些字符串要描述对象的一种含义，这含义不被用在字符串的运算操作上，而建立起称为定理的字符串和描述对象真理间的一一对应关系。公式具有逻辑命题含义时称为命题，便有了真假之分，当公理被认为是真的，定理便是逻辑为真的命题。一个命题在系统内被证明，即被认为是真的，也就成为了定理。哥德尔 1931 年论文的命题 V 中，证明了存在着一个 PM 定理组成的无穷集合，其中每一条定理如果按照上面对于这些符号的解释，都表达了一条算术的真理；反之，有个算术真理的无穷集合（属于“原始递归的”，想象所有可以通过有限次算术运算的结果，它包括加法，乘法计算结果，判断质数等命题），如果这些真理按照上面符号含义的解释表达成公式，这些公式都是 PM 的定理。这种无穷多个对应关系，让你相信这字符串的确实具有那种被原始符号和逻辑定义解释的含义。这个哥德尔关键性的结论称为“ 对应引理 ”，它建立起 PM 定理和数论真理的对应关系。形式公理系统不需要依赖含义可以独立存在和演算，但含义的对应让它易于理解和应用。以后我们在不会混淆时，有时用含义来形容它所对应的那个公式。我们现在已经了解了什么是 PM 的公式和它的算术含义。要把讨论 PM 的元数学命题，变成 PM 里的命题，就需要建立起一个映射关系，把这个元数学的问题变成算术问题，然后应用“对应引理”表达为 PM 的公式。这就可以把纠缠的魔鬼引进防卫严密的 PM 殿堂。哥德尔用逻辑推理和算术运算间的一个对应，设计了这个映射。这便是“哥德尔编码”。（待续）【参考资料】【1】维基百科，理查德悖论 http://zh.wikipedia.org/wiki/%E7%90%86%E6%9F%A5%E5%BE%B7%E6%82%96%E8%AE%BA 【2】 Wikipedia ， Richard’sparadox http://en.wikipedia.org/wiki/Richard's_paradox 【3】 Wikipedia ， Metamathematics http://en.wikipedia.org/wiki/Metamathematics 【4】白冰博文，数理逻辑、谓词逻辑、一阶逻辑和公理系统 http://blog.sciencenet.cn/blog-58025-573028.html 【5】 Wikipedia ， Peano axioms http://en.wikipedia.org/wiki/Peano_axioms; 个人分类: 科普|11409 次阅读|18 个评论

哥德尔定理的证明——1背景和内容: 热度 23 xying 2013-5-21 07:20; 在大学时，我听到一个匪夷所思的定理：哥德尔用数学证明了，数学里有不能被证明的定理。这充满矛盾离奇的说法超越了我的想象，但让我记住了这个名字，一直到几十年后，有了足够的基础，我才了解他是怎么说的，如何证明这个革命性的定理。现在互联网可以很方便地得到信息，从网上很快能了解到哥德尔定理（ Gdel's Theorem ）的严谨陈述【 1 】，但是进一步的解读往往似是而非，一些推论或反驳多是从字面上的联想和发挥。这个理论是如此地刺激人，逻辑又很纠缠，游走在形式和含义的相接之处，最常被误用和责难。对于数学定理的理解最好是了解它的观念及核心逻辑，这样才能知道定理陈述的准确含义，才能合乎逻辑地推论。这系列关于哥德尔定理证明的几篇博文，基本按经典的普及本 Ernest Nagel James Newman 《 Gdel's Proof 》【 2 】的思路，揉合后续研究的补充。直指基本概念、思路和核心逻辑，引导读者思考，逐篇细化深入，而不过分拘泥细节的严谨性，因为它的正确性已由原来的研究来保证的。希望用四五篇的短文，让有理工科基础的读者能领会精神，数学、计算机和哲学专业了解数理逻辑的读者，能够消化这个证明。自从牛顿用物理的直觉，闯进无穷领域里大胆计算，铸造出犀利无比的分析工具后，许多人凭借着直观想象和聪明，也涌进去推导出许多互相冲突的结论，数学家花了两百多年的时间，才厘清了分析领域里的混乱，将整个数学建立在严格逻辑，而不是直观想象的基础上。欧几里德几何一直是科学理论的范本，四条自明性的公理加上一条平行公设，通过逻辑演绎，推导出平面几何无穷数量的定理。一直到了近代还只有几何，被认为是具有坚实基础的数学分支。在这光辉的榜样下，人们尝试用这公理化的方法来规范整个数学。人们后来发现欧几里德也不够严谨，逻辑上的漏洞得以修补，但追到极致，要依赖于“数”的理论。自然数的算术运算是数学的最基本的内容，自然数的性质曾经被中国先哲看成天道的机密，古希腊人作为宇宙的根本，在笛卡尔的哲学沉思里，认为我们无法判断自己是清醒还是幻觉，但在这两者中， 2+3=5 都是永远不变的真理。 1889 年意大利的数学家 Peano 用几条公理（皮亚诺算术公理 Peano arithmetic axiom ，简记为 PA ）【 3 】抽象地定义了“自然数”，“相等”，“直接后继”和数学归纳法的概念，从而能够用一阶逻辑演绎出整个自然数的算术系统，对应着包括通常的加法、乘法、质数等数论的定理。这样的客观世界真理，竟可以从一组有限的假设出发，描写成符号的式子，抽去了客观世界上的含义，不再依赖它们所代表对象的真实性来验证，只是用一组固定的操作规则，将字符串按照规则变换得出新的字符串，便产生出能够对应于客观世界真理的表达式。这个机械化的信念吸引了很多数学家。在这个运动的高潮时，罗素和怀特海在 1910-1913 年出版了三卷的《数学原理》，他们自信已将全部的数学建立在纯逻辑的基础上，为今后的所有数学打下了坚实的基础。 1920 年，当时数学界领军人物希尔伯特，提出一个计划，根据《数学原理》的思想，将所有的数学形式化，称为形式公理系统（ formal axiomatic system ），在这里用精确的形式符号语言来叙述数学命题，根据形式逻辑的规则来操作这些字符串的变换和生成，称之为“形式证明”。这个系统如果有完备性（ completeness ），相容性（ consistency ），保守性（ conservation ）和确定性（ decidability ），数学研究从此不再需要创造性的工作了，一切定理的发现和证明，归结为在这个形式公理系统下的机械运算。【 4 】这个形式公理系统计划，关键的一个环节是相容性的绝对证明。相容性（ consistency ）指系统不能产生自相矛盾的结论。过去所有科学理论的相容性，实际上并没有得到过逻辑的证明，结论依赖于客观的经验来验证。客观的事实是确定的，不矛盾的，这保证了结论的相容性。欧几里德几何虽然以公理化的方式，用逻辑推出所有的定理，它依赖这些公理是自明的，即符合直觉，也就是符合实际的空间经验，所以认为是真理。但这在逻辑上是不完全的。直觉只是经验的印象，怎么保证没有想象之外的事实？希尔伯特用笛卡尔坐标的解析几何，将欧几里德几何的相容性，用代数系统的相容性来保证，但代数系统的相容性该怎么得到保证？这仍然没有得到最后的解决。希尔伯特认为必须构建“绝对”的证明，即这个系统的相容性不再借助其他系统来保证，在抽去具体含义的形式化系统中，相信这个只包含逻辑结构和功能的系统，容易在一览无遗中寻找各个命题字符串之间的逻辑规律，而不需要依赖于不可靠的直觉和经验，从而来证明相容性，这个证明希望只用到有限次推理，每次只用到有限个数学的对象。 1931 年，就在大家为这数学毕其功于一役做努力时， 25 岁的数学家哥德尔发表了一篇论文“论《数学原理》及相关系统的不可判定命题”。让这雄心勃勃的希尔伯特计划成为泡影。哥德尔根据《数学原理》构造出一个简单的包含着皮亚诺算术公理的形式演算系统，称之为 PM 。哥德尔定理有两个结论，这结论对任何包含有自然数加法和乘法的形式公理系统也成立： 1. PM 如果是相容的（consistent）则是不完备的（incomplete）。 2. PM 不能证明自身的相容性（consistency）。解释一下这几个关键词。相容的（ consistent ），或者译为“一致的”或者“自洽的”，意思是说在这个系统里不能推出互相矛盾的结论。因为，若有一对相反的命题（比如说 a=b 和 a ≠ b ）同时为真，那么由它们可以合乎逻辑地推出任何命题（为真）。所以数学系统只有是相容的才有价值。相容的系统里至少有一个命题不能被证明（为真）。完备性（ completeness ），指所有的真理（语义上为真的命题），都能在这个系统里被形式证明（从系统里的定理或公理，按照形式逻辑的方法通过有限步骤推导出来）。 Incomplete 有时中文翻译成“不完备“或者“不完全的”，就是说有些真理不能在这个系统里被证明。这是数学里最具有革命性，也最让人沮丧的定理，它告诉我们公理化固有的局限性。哥德尔虽然只证明了在那个包含有PA的简单 PM 系统，但是它适用于任何包含自然数加法和乘法的数学系统。又有哪个足够大的数学系统不包括这算术运算？哥德尔是数学家和逻辑学者，在琢磨这个提供了严谨的形式逻辑基础，将数学命题形式化的《数学原理》时，他发现了一个秘密，这形式逻辑的操作与算术运算极其相似，如果将形式符号的式子对应于一个自然数，那么形式逻辑的运算就对应于算术的运算，这系统用形式逻辑来描述算术，但算术也可以来描述形式逻辑的过程，它可以合法地自己来谈论自己！这让人想起“这句话是错的”这个古老的谎言悖论。那么我们可以用《数学原理》的规则将“这个公式是不可证明的”，这个谈论数学公式的命题，形式化变成系统里的数学公式，造成一个恶性循环来摧毁这座精巧构建的纯洁的大厦。（待续）【参考资料】【1】 Wikipedia ， Gdel'sincompletenesstheorems http://en.wikipedia.org/wiki/G%C3%B6del's_incompleteness_theorems 【2】《 Gdel's Proof 》 by Ernest Nagel andJames Newman, NYU Press, 2001, 2nd edition http://www.amazon.com/G%C3%B6dels-Proof-Ernest-Nagel/dp/0814758371 【3】 Wikipedia ， Peano axioms http://en.wikipedia.org/wiki/Peano_axioms 【4】 Wikipedia ， Hilberts program http://en.wikipedia.org/wiki/Hilbert's_program; 个人分类: 科普|16412 次阅读|58 个评论

正面回击：哥德尔定理和西蒙的哲学（2）: 热度 2 physicsxuxiao 2013-2-23 13:44; （2）断言的形式化人类的智能是件让人迷惑的事情，我们总是希望用一种手段来描述人的智能并模仿之。比如我们能查觉到以下两个推理的某种一致性：推理A：中科院研究管理的人歌唱得差，而陈安是中科院研究管理的，所以陈安歌唱得差。推理B：清华的人个子高，而文克玲老师是清华的，所以文老师的个子比较高。我们都熟悉，这是三段论，这个推理过程可以用公式表达：推理A的公式化或者形式化：对象1（中科院研究管理的人）属性（歌唱得差），而且，对象2（陈安）属于对象1（中科院研究管理的人），导出，对象2（陈安）属性（歌唱得差）。推理B的公式化或者形式化：对象1（清华的人）属性（个子高），而且，对象2（文克玲老师）属于对象1（清华的人），导出，对象2（文克玲老师）属性（个子高）。总结以上两个公式，我们可以有个一般化的公式来表明三段论的推导过程：公式A：对象1（甲）属性（子），而且，对象2（乙）属于对象1（甲），导出，对象2（乙）属性（子）。这里，“甲”、“乙”、“子”都是变量名。将“甲”这个变量分别代入（中科院研究管理的人）和（清华的人），将“乙”这个变量代入（陈安）和（文克玲老师），“子”这个变量代入（歌唱得差）和（个子高），就分别得到了推理A和推理B的形式化的结果。进一步看，我们推理还牵涉“真”，“假”的问题。比如推理A和推理B的大前提是假的，则这次推理的结果就不一定正确。也就是说，推理A和推理B的结果的“真”或“假”是无法判定的。关于断言的“真”“假”的判断，我们也可以用公式来推导。有一门学问，称为“数理逻辑”，对应于数学里的“元数学”的一部分，就是专门玩这个花头的。当然，在历史上，这是令人激动的学问：我们模仿了人类的推理，并将之公式化或者形式化，那我们不就可以让机器做公式运算，代替人进行推理了吗？进而言之，机器不就有智能了吗？不要高兴得太早，特别要对那些搞数学的朋友说：“没那回事。” 第一件事就很麻烦，这就是自然语言的形式化。仅举一例，来说明这个困难：推理C：不是吃素的人就会吃肉，蒋科学可不是吃素的，所以蒋科学是吃肉的。很明显，这里“不是吃素的”有歧义，对人而言，这个理解很容易，可以对机器而言，尤其是对只会算公式的机器而言，这实在是让机器迷惑。所以，参与争论的朋友，要搞清楚，将自然语言描述的诸如“数学的真理性”等等命题，纳入数理逻辑的范畴，实在是不明智的。（敬请期待下一篇）; 个人分类: 乱七八糟|2812 次阅读|7 个评论

正面回击：哥德尔定理与西蒙的哲学（1）: 热度 2 physicsxuxiao 2013-2-23 10:43; (1)引言一说到与人工智能有关的话题，有两拨人一定不请自来：一拨是搞数学的（包括搞抽象计算机的），另一拨是搞认知心理学的，可以在你的基金本子上胡乱评论，毫无逻辑-我就吃过这个亏-会把一个简单的工程问题搞得玄而又玄，离题万里。最近网上又开始热炒“数学的真理性”，从郑波尽博主到程代展老先生，都频频发文。我觉得有必要借此机会，谈一下这些玄而又玄的问题。当然，这网上肯定有人知道我的师承，所以希望回应的时候，跟我讨论就行，别扯我的师承。; 个人分类: 乱七八糟|2905 次阅读|10 个评论

更多...

帐号		自动登录	找回密码
密码			注册

关闭 安全验证

标签: 哥德尔定理

相关帖子

相关日志

关闭安全验证