（考虑到原文跟帖已经够多，国内学校内打开慢，所以这里专门开一个帖子，方便大家对guage兄这篇文章的谈论。以下是我个人看法，不一定对。有些地方可能源自我对guage兄论述有误解）。

今天终于把guage兄的这个系列系统地看了一遍，写得不错。guage兄的作品有一个特点：在看似不经意之中，常常暗藏玄机。尽管如此，guage兄的有些看法我不太赞同。

也许其他有些没有系统了解过Godel不完备定理的人，很容易如guage兄所说凭字面意思误解它，但就我而言，我看完这个帖子之后，感觉我本人对Godel不完备定理的认识与理解，与本文所介绍的并无不同，只是对guage兄的一些个人感想有些不赞同。

例如，guage兄一再强调，这里涉及到的“证明”这个术语，跟我们通常所说的“证明”含义不同。但是在我看来，这没有不同。逻辑学中的“证明”，是把通常的证明过程抽象化、形式化，提炼出本质，其实跟数学中证明某一道具体的数学题，含义没有分别。我们可以通过同构映射的方式，把一道数学题的证明过程形式化（或“翻译”）为一道逻辑推理过程（即利用公理、符号、变形规则等进行的符号串演算），这个过程就是逻辑学上的所谓证明。

至于什么样的“证明”才能算作是一个“证明”，那又是另外一回事。一种观点是，证明某个东西存在，而不必管这个东西到底是什么，这也可以看作是一个证明；另一种看法与之不同，认为光证明其存在，这个证明过程还没有完结，必须还得把这个东西到底是什么给找出来，证明才算结束。后者即是guage兄详细介绍过的构造主义观点。

我有点迷惑的是，Hilbert应该知道这样一个事实：可以证明素数有无穷多个，但是到底素数集合是什么，不存在一种算法来给出它。换句话说，给出一个数，不存在一个算法来判断它是不是素数。既然如此，那他为什么还试图给出所谓“Hilbert计划”：要寻求一些算法，这些算法可以构造出（所有）真的算术命题？

guage兄提到，“Godel定理中的用语，特别是“真”、“证明”这两个词的意义与我们通常看到的并不相同，这也是造成混乱的一个重大原因”。这点我不赞同。我觉得一般人能够知道“真”、“证明”这两个词的意义，关于“证明”我在上面已经谈到，这里不提。“真”命题，是可以赋予逻辑真值“1”的命题，这一点应该没有错。对于一个公理系统内可以判定的真命题b，可以在这个系统内推导出来：((A→b)∧A)→b，其中A表示系统的公理集合。由于事先假定任何一个命题，其真值不是0就是1，如果是0，则其否定命题的真值就是1，因此对于不可判定命题，由于它和它的否定命题都是不可判定的，所以它和它的否定命题中，必然有一个是真值为1的不可判定命题。这一点，guage兄用另一种方式也谈到过。

关于Penrose的论述，首先需要注意的是，人工智能有很多不同的学派，其中到目前为止最为成功的还是数理逻辑派。严格依靠逻辑演算的人工智能，是无法判定不可判定的真命题，但是人却可以依靠猜想和直觉、经验、类比、联想等等方式直接找到真理，而不必通过一个严格执行的程序（最后通过实验或其他来验证），从这点来说，这种机器人不能具有象人那样的思考能力，这是对的。比如一元五次以上的方程不存在求根公式，因此不存在一种算法来求解这类方程（机器人无法求解）。但是其中某些比较特殊的方程，人可以直接凭直觉给出试探解，再代入方程验算一下对不对，以此方式来找到解。当然现在的人工智能理论，同样试图建立能够实现直觉、经验、类比、联想等等功能的人工智能理论，总之最大限度地模仿人类的一切，此时Penrose的论述应该是错的。毕竟，人类不过是大自然制造的机器。除非人真的存在灵魂，否则我看不出什么理由认为造不出象人一样的机器。神经网络配合纳米技术，使得这种可能性大为增加。

关于Hawking的看法，直接否定可能也缺乏依据，虽然他本人提出这种看法，也许多少是靠一知半解蒙出来的。首先，终极理论的目标是什么？是不是想得到这样一个理论系统，从这个理论中可以推导出宇宙中的一切真理？其次物理理论体系也好，整个数学理论体系也好，是否可以变成一个形式系统？或者满足Godel定理条件的形式系统，可否镶嵌在前者所变成的形式系统之中？如果是，那么Hawking的看法不是瞎说。

关于类比Heisenberg不确定原理。如果物理理论可以翻译成一个形式系统，其中Heisenberg不确定原理翻译成：当粒子的位置为X可以判定时，粒子的动量是否为P，是一个不可判定的命题，那么这种理解也不是胡说八道的。

我最不能同意的，是guage兄列举的“荒谬的推论3”。事实上，任何一个公理系统中，它的所有公理都是属于在该系统内不可证明的真命题（不可判定的真命题）。所以在欧氏几何中，平行公理是永远无法证明的。同理，假如连续统假设是一个不可判定的真命题，那么它只能直接作为一个公理来使用，而不能成为一个可以证明的定理。如果引入新的等价公理来替代它，那么在新的理论系统中连续统假设变成一个可以“证明”的定理，但这不过是采用了拆东墙补西墙的办法。无法证明的真命题，只能通过物理实验证明与之相关的所有推导结论，来验证它的正确性。

（现在开学了，我有些急事不得不忙，所以所有回帖待我忙过这阵子再来回复。其他所有对该话题感兴趣的，不妨都来拷问guage兄。毕竟guage兄的这篇文章是目前为止有关这个话题最专业、最好的一篇文章）

对-哥德尔定理之拙见-一文及回复的评论

首先赞一下gauge兄的洋洋洒洒好文章，值90分。刚过完年看这种文章特别醒酒，煞是过瘾。

称赞gauge兄对哥德尔定理适用的限制条件之强调。
声援gauge兄对强AI学派的精神支持，也就是对Penrose的批判，但Penrose对人脑思维含有＂非计算＂的成分的强调是有功劳的。还有，他关于量子力学效应对人脑意识的决定性作用的见解，将被证明是正确的，虽然他现在因此而饱受围攻。
大体同意gauge兄对Hawking观点的批判。Hawking和Penrose这两个大地主，最近挨了不少批斗，反映伟大人类思维深处的普遍的革命本色。

既然讨论，好话近于废话，对能评判哥德尔定理的君子而言，奉承更是包藏祸心的。所以，还是来些难听的吧。大家批Penrose,Hawking过瘾，其实批星空批gauge何尝不是这样。

我的几点看法：
（1）星空兄反对gauge兄认为哥德尔意义下的＂证明＂，＂真＂与我们通常的理解不一致。 我认为你们大体各对一半：哥德尔意义下的＂真＂与我们通常的理解是一致的，但哥德尔意义下的＂证明＂比我们通常的理解要窄（狭义）一些。gauge兄讲得很清楚，哥德尔意义下的＂证明＂是指形式系统中一阶谓词演算下的一个＂可计算＂流程（算法），而确实有不能约化为＂计算＂的证明。但另一方面，哥德尔意义下的＂证明＂比我们通常的理解又要＂高层次＂一些，因为它是关于系统自身的，而不是关于系统内部的。哥德尔定理是所谓的＂元定理＂或＂形而上＂的定理,meta-theorem。
（2）本来Hawking认为TOE物理理论建立不起来的观点就很难说一定对（我认为，有不少领域，已经有了TOE，例如机械工程，甚至化学），而他借用哥德尔定理来作论证的话，就正如gauge兄评价的，属于＂惨不忍睹＂。建立TOE就是要把物理理论建成一个形式系统，只是按哥德尔定理，即算这种形式系统建立起来了，我们永远无法通过演算证明该体系是否自洽或有真理遗漏。不知道是否Hawking的上述见解属于误传，但愿如此。
（3）gauge批评了＂有人认为，Godel定理告诉我们有一些真的数学定理是永远无法证明的＂。星空兄表示强烈反对，我认为明确了上述（1）中＂证明＂的差异，就不会有争议了。改成＂有人认为，Godel定理告诉我们有一些真的数学定理是永远无法给出一阶谓词演算证明的。＂就严密了。其次，＂有一些真的数学定理是永远无法证明的＂中的数学定理是指＂公理系统外的真命题＂的话，用哥德尔定理其实是多余的，如果不是错误的话。
（4）星空兄“关于类比Heisenberg不确定原理。如果物理理论可以翻译成一个形式系统，其中Heisenberg不确定原理翻译成：当粒子的位置为X可以判定时，粒子的动量是否为P，是一个不可判定的命题，那么这种理解也不是胡说八道的。＂很有创意，但哥本哈根学派会说，这不是一个不可判定的命题，而是一个无意义的命题。至于如何跟哥德尔定理扯上关系，还值得探讨，因为量子力学公理系统与哥德尔定理赖以成立的形式系统之间有很大差异。
（5）gauge兄不太赞同的＂哥德尔定理是对人类认知的极限提供了逻辑依据＂，其实有一定道理，因为人类处理非常复杂的体系时，计算是不能逃避的，但可计算性受哥德尔定理的约束，使得某些问题的解永远无法得到。

致谢：我读gauge兄文章激发出的一个想法是“存在内在矛盾的公理体系可能具有更强大的生命力。＂

问个枝节的问题

星空：
我有点迷惑的是，Hilbert应该知道这样一个事实：可以证明素数有无穷多个，但是到底素数集合是什么，不存在一种算法来给出它。换句话说，给出一个数，不存在一个算法来判断它是不是素数。既然如此，那他为什么还试图给出所谓“Hilbert计划”：要寻求一些算法，这些算法可以构造出（所有）真的算术命题？
-------------------------------------
我想问对素数的试除算不算是一个算法
任何一个数都可以用有限步试除来判断他是否是素数
只是复杂度好像很高

我被搞糊涂了，搜到两个证明方法，有一个看似是直接证明怀特海猜想的将逻辑运算对应成小数的证明，还有一个是构造出那个不可证明的命题的证明，都说是哥德尔的证明。到底哪个是他对这个定理 的证明啊。

>我被搞糊涂了，搜到两个证明方法，有一个看似是直接证明怀特海猜想的将逻辑运算对应成小数的证明，>还有一个是构造出那个不可证明的命题的证明，都说是哥德尔的证明。到底哪个是他对这个定理 的证明
>啊。


建议阅读：

朱水林着 <<哥德尔不完全性定理>>，很详细，且不难。 记得网上有免费的PDF版。

OR

更友好的介绍可参考Ernest Nagel 和 J. Newman的<<Goedel＇s Proof>>，属于普及性但不失严密性的证明介绍。

刚把gage兄的整篇文章看完了，觉得其基本观点好像有误。

::Hilbert提出一个计划，希望由有限、组合的方式，先证明最简单的算术是一个内部一致的理论，然后以此为基础证明数学分析的一致性，尔后进一步证明整个数学的一致性。Hilbert计划中的证明就是纯粹构造式的。

这里说的证明是元数学（或证明论）中的证明，属于形式系统外部的证明。它是一种构造性的方法，用来证明形式系统的一致性

::Hilbert的形式体系与Brouwer的直觉主义相比而言，对于证明有更加严格、狭窄的含义。不仅仅其中没有排中律，而且规定了定理只能通过变形规则得到。新的定理只能通过已经被证明的定理变形得到。这是一种很强的构造性。

而这里说的证明是形式系统内部的证明。
实际上绝大部分的形式系统（包括这里说的Hilbert形式体系）都包含了排中律。（排中律虽然不是公理，但可以由公理和推理规则得到）


就是说把形式系统内部的证明和元数学的证明混淆了

::而且规定了定理只能通过变形规则得到。新的定理只能通过已经被证明的定理变形得到。

这是形式化方法的特征，与直觉主义无关


::显然的确给出了XXX是一个定理的证明。
::但是这个证明在形式主义看来是不合法的，或者说是没有意义的。因为形式体系中的证明只能由已经证明的定理通过变形规则得到。

1、这个证明是可以翻译为一个形式证明的
2、直觉主义不能接受这个证明，因为它使用了排中律，而形式主义会接受这个证明。
形式主义要求的可构造性只局限于元数学，而不涉及形式系统内部的证明。
3、形式化与形式主义不是一回事

::Godel第一不完备定理的第四个叙述方式：在包含基本算术且一致的形式体系中，存在真的但不可构造的命题。

把形式系统内部的证明和元数学证明混淆了，才会有这样的观点

谢谢大家参与讨论。以前作为中国逻辑学会会员时有不少通信地址，如今弄丢了，不然可以介绍他们进来参加讨论。今天临时进来回复几句，其它的以后再回复：

1）我提到素数这个例子，也是带有请教大家的意思。我不止一次看到“给出一个数，不存在一个算法来判断它是不是素数”这样的说法，我想让这个数除以所有比它小的自然数，看有没有能够整除的，不就行了？所以我自己理解的是：无法给出素数的一般表达式（即由一个表达式出发给出所有素数)，这才是“没有确定一个数是不是素数的算法”的含义。

2）我记得有文献说过，整个欧氏几何体系，可以变成一个纯逻辑的形式（符号）系统——此时几何中的证明，变成符号逻辑演算形式。我好像还记得，说整个数学理论大厦都可以翻译形式数论系统，从而最终变成一个形式系统。在我眼里，形式系统跟具体理论系统同等给我实在的感觉。

3）需要说明的是，人工智能曾经被人视为伪科学。不过再怎么说，计算机下棋是实实在在地实现了的。我硕士研究生阶段学习的人工智能课程比较肤浅，因为老师很肤浅。

4）我提到“一元五次以上的方程不存在求根公式，因此不存在一种算法来求解这类方程（机器人无法求解）”。需要说明的是，实际上计算机技术可以求解很多方程，因为可以采用数值近似方法，而不必依赖于解析方法。

5）我提到“关于类比Heisenberg不确定原理。如果物理理论可以翻译成一个形式系统，其中Heisenberg不确定原理翻译成：当粒子的位置为X可以判定时，粒子的动量是否为P，是一个不可判定的命题（即无论是P还是不是P，都无法判断），那么这种理解也不是胡说八道的”。这里有一个例外：没有考虑量子逻辑。在量子力学的基础理论中，量子逻辑学派的权威和影响力是很大的。

其它的以后再说。

::但是这个证明在形式主义看来是不合法的，或者说是没有意义的。因为形式体系中的证明只能由已经证明的定理通过变形规则得到。

这句话其实是正确的，我在前面理解错了它的意思
不过把“这个证明在形式主义看来是不合法的”改为“这不是形式证明”更好

在我将来有机会重新系统复习一遍逻辑之前，我暂时不再讨论这个话题，因为感觉心是虚的。此外，有些观点如果不展开说彻底、说明白，仅仅直接点到，只会造成字面上的误解。

建议阅读：

朱水林着 <<哥德尔不完全性定理>>，很详细，且不难。 记得网上有免费的PDF版。

OR

更友好的介绍可参考Ernest Nagel 和 J. Newman的<<Goedel＇s Proof>>，属于普及性但不失严密性的证明介绍
=========
一本都没找到，上面的找不到能看的有效地址。只在维基上找到些证明要点看。谁有完整证明的有效链接啊，有就给提供一个。

::Godel第一不完备定理的第四个叙述方式：在包含基本算术且一致的形式体系中，存在真的但不可构造的命题。

把形式系统内部的证明和元数学证明混淆了，才会有这样的观点
==========

我觉着这个叙述对啊，这个叙述自身是关于整个形式体系的结论，并不是在体系内由公理、变形规则推导出来的内部结论。他这个构造是指在形式体系内由公理变形规则构造符号串去对命题进行证明，不是指按形成规则去构造命题公式。

朱水林书：哥德尔不完全性定理 PDF

已发至客栈公共邮箱。

4）我提到“一元五次以上的方程不存在求根公式，因此不存在一种算法来求解这类方程（机器人无法求解）”。需要说明的是，实际上计算机技术可以求解很多方程，因为可以采用数值近似方法，而不必依赖于解析方法。
=============================================
精确说，应该说“一元五次以上的一般方程”不可根式解。因为某些特殊方程可以解

::他这个构造是指在形式体系内由公理变形规则构造符号串去对命题进行证明，不是指按形成规则去构造命题公式。

如果这样理解构造这个词，那么对Godel定理的第四种叙述方式是正确的。
但原文中的构造并不仅仅是这个意思，它还和形式主义（或直觉主义）所要求的构造性证明这个构造同义。而后面这个构造的含义是不同的。

－－－－－－－－－－－－－－－－

“Hilbert的形式体系与Brouwer的直觉主义相比而言，对于证明有更加严格、狭窄的含义。不仅仅其中没有排中律，而且规定了定理只能通过变形规则得到。新的定理只能通过已经被证明的定理变形得到。这是一种很强的构造性。”

这里把形式证明和构造性证明混为一谈了。
形式系统中的证明叫做形式证明，获得形式证明的命题叫形式定理。形式证明必须严格遵守推理规则，也就是新的定理只能通过公理或已被证明的定理变形得到。形式证明也可分为构造性和非构造性的，构造性的形式系统不同于非构造性的形式系统。在非构造性的形式系统中，排中律（即P v ～P）不是一个形式定理。
元数学是用来证明形式系统的相容性的，它必须使用构造性的方法。注意，这里说的证明是系统外的证明，形式主义对形式证明没有限制。
而按直觉主义，证明必须是构造性的，无论它是否形式化。

－－－－－－－－－－－－－－－－

另外，关于Gooodstein定理。去那个网页上看了一下，它只说了Gooodstein定理不能在Peano算术系统中证明，没有说它不能在任何形式系统中获得证明。

::在非构造性的形式系统中，排中律（即P v ～P）不是一个形式定理

笔误，应该把“非”字去掉

::它只说了Gooodstein定理不能在Peano算术系统中证明，没有说它不能在任何形式系统中获得证明。

说明一下。我是想说，Gooodstein定理不能在Peano算术系统中证明，不等于不能把原来的证明翻译成一个形式证明，当然这时必须对Peano算术系统进行扩充。我不清楚，通常的数学中，所用到的前提是否比Peano算术系统更强（似乎应该更强一些）

:::通常的数学中，所用到的前提是否比Peano算术系统更强（似乎应该更强一些）

Not necessarily. In real and complex analysis, or in geometries, for instances, the axiomatic system does not contain an axiom or an equivalent one from which integers can be constructed. Basically, (integer) numbers there are used without definition. In number theory, however, the numbers have to be defined (constructed) beforehand.

朱水林的书《哥德尔不完全性定理》还是不错的，唯一的不足是，对哥德尔不完全性定理的证明本身叙述得不够，甚至省略了第二定理的证明。既然作为专门的专业书籍，最关键的证明部分，应该不惜笔墨，证明过程应该足够深入和全面。不过作为搞哲学的，写到这种份上还算不错的。