转载请注明作者：phylips@bmy
哥德尔完备性定理
希尔伯特在20世纪20年代介绍了他的元数学纲领：一致性有待证明的公理将被包含在一个形式逻辑系统之内，而证明仅仅是有限数目的符号的一种排列而已。当希尔伯特开始思考希尔伯特纲领时，希尔伯特的学生阿克曼和冯诺依曼似乎正在朝着用有限性方法证明PA的一致性的方向大步迈进。他们二人都已经为PA的一个有限的子系统找到了这样的证明，成功似乎指日可待。
这样哥德尔开始试图将算术一致性还原为PA的一致性，然而就是在这样的努力中失败了。哥德尔开始思考这些问题时，他重新思考了从外部而不是从内部考察一个系统的意思。从外部看，这些系统包含着符号串之间的关系。从内部看，这些系统能够表达关于不同数学对象的命题。哥德尔通过给符号串用自然数编码，将外部带到了内部。
哥德尔发现存在这样的命题，它们从系统外部看是真命题，但无法在系统内部得到证明。于是他得出了一个非凡结论：一种有意义的数学真理的观念不仅是存在的，而且其范围还超出了任何给定的形式系统的证明能力。在1931年，他发表的论文<<论 <数学原理>及有关系统的形式不可判定命题>>中，他选择对形式系统PM给出了他的结果，从而说明即使强逻辑系统也不可能把全部数学真理包含在内。
在哥德尔的证明中，关键的一步在于他证明了：一个自然数作为PM中可证命题的一个代码，这一性质本身可以在PM中表示出来。根据这一事实，哥德尔可以在PM中构造出一些命题，这些命题可以被看做表达了这样一个断言，即某些命题在PM中是不可证的。也就是说他可以构造出一个命题A，该命题经译码后可以断言某一命题B在PM中是不可证的。现在，在没有获知密码的人看来，命题A不过是一串符号而已，但是通过代码，神秘性就消失了：A表示这样一个命题，即某个符号串B表示在PM中一个不可证的命题。A和B通常是不同的命题，哥德尔问，它们是否有可能是相同的呢？事实上它们可以是相同的，哥德尔可以利用对角线方法证明这个结论。
运用这些技巧，我们可以使被断言为不可证的命题和做出这一断言的命题是同一个命题。换句话说哥德尔发现了如果获得这样一个非凡的命题，我们将它称之外U，具有如下性质：
U说某个特殊命题在PM中不可证。
那个特殊的命题就是U本身。
因此，U说"U在PM中不可证"
如果我们承认PM中证明的任何命题都是真的，那么我们发现U是真的，但它在PM中不可证。
U是真的。假定它是假的，那么它表述的内容就是假的，因此它就是不是不可证的，而一定是可证的，从而是真的，这与开始假定U是假的矛盾，所以它一定是真的。因为它是真的，所以它表述的内容为真，所以它在PM中不可证。
我们把U称为不可判定命题，当然这种不可判断性只与系统内部的可证性，从我们外部的观点来看U是真的。
另一方面，在PM内部，我们可以证明：如果PM是一致的，那么U。因此正是PM是一致的这一个假定，才使U在PM内部得不到证明。既然我们知道U在PM内部是不可证的，我们就必须得出结论说，PM的一致性在PM中不可证。而希尔伯特的主要目的就在于：用于被认为构成PM的一个非常有限的子集的有限性方法来证明像PM这样的系统的一致性。然而哥德尔证明了，即使就PM的全部能力而言，它也不足以证明自身的一致性。于是希尔伯特纲领走到了尽头。
下面具体来看，如果构造出那样的一个命题U。
图灵和图灵机
在哥德尓1930年的博士论文中证明了弗雷格的规则是完备的，这样就回答了希尔伯特1928年提出的第一个问题。而第二个问题即判定问题，在哥德尔的工作发表之后，人们很难想象存在这样的判定算法，于是阿兰图灵开始思考如果证明这样的算法是不存在的。
图灵采取了这样的一条道路，他首先分析了人的计算过程。通过丢掉非本质的细节，将这些计算活动局限在少数几种极为简单的基本操作上。然后图灵说明人可以被一个能够执行这些基本操作的机器所替代。然后只要证明仅仅执行那些基本操作的机器不可能判定一个给定的结论是否可以用弗雷格的规则从给定的前提中导出，这样他就能够下结论说，判定问题的算法是不存在的。
作为副产品，他对计算过程的分析，产生了通用计算机的一个数学模型。
他观察到：在计算的每一个阶段，只有少数符号受到了注意。每一个阶段所采取的行动仅仅取决于受到注意的那些符号以及当前的心灵状态。
然后他做出了如下抽象：计算通过在一条被划分成方格的纸带上写下符号来进行。执行计算的人在每一步都只注意其中一个方格的符号。她的下一步将仅仅取决于这个符号和她的心灵状态。她的下一步是这样的：她在当前注意的方格里写下一个符号，然后将注意力转向它左边或者右边的相邻符号。
现在可以很容易看出，做这项工作的人可以用一个机器替代，纸带在机器上来回移动。关键之处在于图灵对于计算概念的分析，通过某种算法程序可计算的任何东西都可以通过一台图灵机来计算。因此如果我们可以证明某些任务无法用图灵机完成，那么我们就可以说没有任何算法可以完成这项任务。这就是图灵证明判定问题不存在算法的方法。
实际上一台图灵机可以用这样的一个五元组来表示：当机器处于状态R，注视纸带上的符号a时，它将用b来代替a，向右移动一个方格，然后转到状态S。而一个具体的算法便可以由这些五元组表示的状态转换的集合组成的图灵机来表示出来。R a:b -> S 或者R a:b <- S
图灵将对角线方法应用于这种情况，得到了图灵机不能解决的问题，由此推出了判定问题的不可解性。与哥德尓类似，图灵采用了对角线方法也对图灵机通过自然数进行了编码。
图灵机本身可以是自然数编码表示，这样它也作为自身的输入。实际上有些输入会使图灵机停止下来，另一些则不会。这样一台图灵机就具有一些停机集合。如果我们考虑把一台图灵机的停机集合组成了一个包裹，并且认为那台机器的码数就是这个包裹的标签。对角线方法允许我们构造出一个与图灵机的任何停机集合都不同的自然数集合，我们称之为D。方法是这样的，我们考虑把图灵机的编码作为自身的输入，如果它的编码数不属于自身的停机集合，那么我们就把它加入D。而集合D则不是任何图灵机的停机集合。
然后考虑这样一个问题：
找到一种算法，判定一个给定的自然数是否属于集合D。
这就是一个不可解问题的例子。首先如果存在这样的一个算法，我们就能找到这样的一个图灵机，但是我可以改造一下这个图灵机，把以下两个五元组加入到这个图灵机：F 0:口-> F 和 F 口:口-> F。对于这个新的改进的图灵机来说，如果输入的数属于D那么那么机器就会像以前一样运转，并输出1而告终，如果输入的数不属于D，那这台机器将永远向右移动。这样我们就找到了一台图灵机它的停机集合刚好就是D。于是与我们的对角线方法矛盾。所以并不存在这样的一个算法。由此可知判断问题在算法上是不可解的。
为了验证自己工作的有效性，图灵又提出了通用机模型，通用机包含了图灵机代码以及待处理的数据。而这刚好对应着我们今天的机器，程序与数据的概念。也为存储程序计算机提供了一个模型。正是图灵在证明判定问题的不可解性是，对计算概念的分析以及对通用机的发现促使了计算机的产生。
1945年图灵又发表了他那篇著名的ACE(自动计算机)报告。这是对计算机的一次完整的描述，一直到逻辑电路图。也就是在这时冯诺依曼提出了他著名的"关于EDVAC的报告草案"，它实际上主张将要建造的EDVAC作为图灵通用机的一个物理模型实现出来。在这个报告里，提出了存储程序的概念，也就是沿用至今的冯诺依曼结构，实际上它的革命性不在于存储程序而是通用性，存储程序只是达到这一目的的一种手段。
1950年，图灵又发表了他的经典论文，计算机与智能，提出了著名的图灵测试来测试计算机是否具有智能。1954年6月7日，图灵咬了一个浸过氰化物的苹果，结束了自己的生命。而他的通用机思想却延续到今天。
总结
实际这些文章是在我看过了，<<逻辑的引擎>>之后，对里面设计的数学问题的一个总结，剔除了关于科学家们生平逸事的内容。而是专注于那些纯粹的思想是怎样的，以及怎样产生发展和被解决的。而这样的一些思想，逐步的称为计算机科学背后的基础。从这里，或许可以稍微理解这些伟大的人物和思想，是如何于计算机的起源产生关系的。
参考文献：
<<逻辑的引擎>> Engines of Logic 马丁 戴维斯