在看计算理论相关的书的时候，偶然看到这个blog，http://skibinsky.com/godel-turing-and-cantor-the-math/，写的很好。我觉得用自动机的方式讲计算理论的话，从DFA，正则，到图灵机，都是很直观而且容易理解的，但是从Halt, Reducibility开始，再用图灵机的语言来描述就是一件可怕而且容易令人迷惑的方式了。这个时候通常不得不退回去，尝试从Lambda Calculus的角度去理解计算理论。不过 Recursion 的符号确实也很讨厌。如果起初就看到这篇文章，我想任何人在理解计算理论的时候都会更容易些吧。不过文章很长，看看我有没有耐心抽空翻译完它吧。
一个形式系统仅是一系列公理和规则，比如用简单的英文来记录公理，“Number 0 exists”。
但我们能否把自然数关联到公理和规则呢？我们知道，在计算机上一切都是数字。比如，字母 “N” 是78，字母 "u" 是 117，诸如此类。“Number”这个单词对于我们来讲，就像 7811710998101114 对于计算机一样，只是个长长的数字。为什么“N”是78， 不是87或者是8787？没什么特别，只是任意指定的而已，这种指定我们称之为编码规则。如 ASCII这样的具体的标准，规定了，计算机系统如果要兼容ASCII，则必须把“N”指定为78，反之也一样。
这里有意思的地方，即哥德尔证明的关键：在定义数字存在和简单算术的系统中，如果公理“Number 0 exists”，是其中的第一个公理。同时，用ASCII编码“Number 0 exists”，或者其他任何编码，得到关于这个公理的一个数字，表示关于这个关于数字的公理（或规则）。然后我们得到下面这些：
这串数字惊人地长，但终归还是数字。然后，对余下的所有初级公理和规则进行同样的编码，接着我们可以开始对这个形式系统的第一个推论进行编码，再对推论的推论进行编码，等等等等。最后，任何公理或者推论序列都变成一个数字。
有趣的事情开始出现，一方面你定义了一个描述自然数基本属性的形式系统；另一方面，这些公理和推论本身又是用自然数本身定义的！只要需要，我们就可以来回转换。可以把公理当作简单的英文来处理，又可以转换到纯粹的，即使会很长，的数字，把他们当作数字一样处理。系统是自指的：即描述数字的公理和规则同时又是数字自身。
现实生活中，用英语来描述形式系统，是非常冗长低效的方式。逻辑学家们发明了很多紧凑语法来描述这一类系统。另外，对于计算机，ASCII编码是不错的，但缺乏某些哥德尔证明所需要的关键属性。于是哥德尔建立了自己的完全唯一的编码，称为哥德尔编码。神奇的是，他是在计算机或者任何ASCII之类的东西出现的几十年前，就提出了这种编码。他的编码用素数进行，要感谢绝对基础的素数因式分解定理，赋予了对于下一步证明极其关键的属性。这类编码保证了，每个唯一的逻辑符号序列-公理，规则，推论等等-都有一个唯一的哥德尔编号。并且我们可以在哥德尔编号和产生哥德尔编号的原本的符号序列之间，来回转换。
现在我们可以用标准的符号逻辑来写逻辑语句，然后将其转换到哥德尔编号。关于自然数的形式系统（或者更复杂的形式系统），其公理和规则，我们都可以写，感谢哥德尔编码的魔法，这些语句同时也就是一些大自然数。从最短的公理到复杂的推论链条，任何事物最后都表现为数字。然后我们可以用一般的数学方法来处理这些数字：证明他们的定理，展示其属性，关系，就像我们在处理其他的数字一样。
以往在给定的逻辑系统里，我们要处理复杂的，证明所涉及到的无穷的可能性，现在，哥德尔宣称：
要知道，我们不一定非得处理这些疯狂的复杂性。我来告诉你一个特别的方法，怎样把任意证明变成一个极大的数字，并且怎样准确地把这些数字转回到原来的证明。只要你有任何证明，10页纸甚至1000页纸长的证明，都仅仅是一个唯一的完全表示你的证明的数字。并且这一点，对于所有可能的证明都成立。从现在开始，我们就只处理和证明关于数字的定理和关于数字的函数。这就简单得多了。
对于现代的软件开发者来讲，哥德尔下面的工作可能是很熟悉的-更别提在这些概念进入技术领域之前，他在几十年前就这么做了。他开始开发自己的函数库，实际上基本是特定领域的语言，用于解决他本来想要解决的问题。而他发明的现代递归概念，仅仅是他工作的副产品。用现代的词汇来讲，他勤奋地证明了他构造的所有函数都是可计算的-即这些函数在有限（即使很大）的离散的步骤之后，都能对某个问题给出相应的具体答案。这也暗示，未来的图灵机，其实已经在他对原始递归的定义中，隐约可见了。
他的第一个函数几乎就是微不足道：他定义了“x可以被y整除”。现代逻辑语言里，可以这样写：
$1. y | x \iff \exists z \leq x.x=y.z$
通常的语言描述就是，如果存在 z , z小于等于x, 并且 x 等于 z 乘以y, 则x可以被y整除。这就是整除的定义嘛。
之后的定义则开始使用前面定义好的函数，如同现代的软件函数库一样。这使得哥德尔可以飞快地开始建立他的复杂性推论。下一步他定义了什么是素数：
$2. isPrime(x) \iff \neg (\exists z \leq x.(z \ne 1 \wedge z \ne x \wedge z|x )) \wedge (x > 1)$
可以看出，如果遵循系统的创建更长语句的规则，则可以用逻辑语法来写更复杂的推论。这个语句声明：如果不存在一个数z，z小于x；z不等于1，而且z不等于x并且x能被z整除，则x是一个素数。这只是非常明确的对x只能被1和自身整除的表述。
如此这般，哥德尔继续对他的库建立逻辑上的展开。从皮亚诺公理开始，持续地进行推论，建立越来越多的精巧的函数。建立这样一个库的目的到底是什么呢？哥德尔的天才的目标在于：他就是想描述这样一个函数，能够检测可证明性的函数，即在任意逻辑系统中，什么才是正确的推论。
哥德尔编号能按照逻辑语句的语法进行编码。但是这些编码却不能告诉我们任何关于这些语句的含义。比如，我们可以说，“对于任意x，x+1都等于5”，这明显是错的，但我这样写并没有什么语法错误。我们可以写任何符合逻辑语法的语句，不完全的，无意义的，错的，都可以，如同我们能得到的，可以证明为真的推论语句一样。那么，到底怎样区分无意义的语句，和真正的证明呢？
写下上面那些错误的语句的时候，我们已经打破了一些逻辑系统里的规则。要写真正的证明语句，必须从公理开始，从公理建立下一步的结论，最后，正确地使用所有衍生出来的规则，然后抵达我们想要证明的任何东西。真的证明不能只是一个单独的语句。它总是严格的序列，可以追溯到系统最初的公理。这就揭示出，验证特定的语句是不是真正正确的证明，可以变成纯粹的数学函数的检查和验证！哥德尔用了不超过45个中间结果，得到了函数编号46：$provable(x)$
$provable(x)$ 和英语老师判卷一样。用英语写作的时候（如同用逻辑语法），任何荒唐的文章，包含任何拼写错误以及语法错误，你都可以写，但一个好老师却不会这样。写得好的文章可以得到及格以上的分数，错误的则被拒掉。$provable(x)$做的是一样的事情，只是它基于逻辑语法。如果“x”是正确的逻辑推论序列，遵循了所有的公理和规则，$provable(x)$则判定x是有效证明，否则拒绝x。很明显，$provable(x)$严重依赖哥德尔在第一到第四十五步之间定义的函数。其中包含了大量转换思维的复杂的工作。然而，所有的复杂性都被表示成和编码成纯粹的符号和数学逻辑。
任意逻辑系统中包含的自指的本质，这里再次出现。从纯粹数学的角度，$provable(x)$只是个函数，和别的函数没什么分别。当然它是个非常复杂的函数，但除了要完成很多复杂的步骤以得到结论，对于它所属于的形式系统而言，这里面没有什么是魔术。在他的系统中，这个公式描述什么可以和什么不可以被证明。这个函数为系统赋予了声音，系统开始向我们表达他自己，即在它内部，什么是可能的。从这里开始，事物变得越来越令人好奇。
爱因斯坦，哥德尔和美国宪法 如同来到硅谷的大多数人，哥德尔也是移民，也要面对公民权考试。当然，这个逻辑大师就开始学习美国宪法，当然，他很快就发现了其中的问题。按照哥德尔的说法，他发现了宪法中某个不一致的地方，以至于民主会恶化成为专制。哥德尔的朋友，知道没有什么社交惯例会阻止哥德尔批评他所发现的逻辑错误，于是决定找办法保证哥德尔通过公民权考试。其中一个办法则是阿尔伯特.爱因斯坦。尽管这些办法起到了好效果，分散了哥德尔的注意力，但最后哥德尔还是设法把他的发现传达给了主持仪式的法官。庆幸的是，这个法官也是几年前主持爱因斯坦宣誓的那个，哥德尔无惊无险通过了考试。如果决定告诉法官，你发现了美国最高法律文件的逻辑错误，有爱因斯坦做队友，还是不错的。
有个无法回避但相当简单的数学问题。起初，证明并不包括对角引理；哥德尔用他纯粹的脑力在全部证明中隐含地推导了它。引理表述的是，给定的哥德尔编号的系统，总是至少有一个数字$f$，对于任意逻辑公式$F$，$f=Godel-Number(F(f))$。
直觉上，证明可以如此理解，如果我们在纸上画函数，比如$y=Godel-Number(F(x))$,我们从$x=0,x=1,x=2$，开始，在得到相应的G-number的地方画点。一直增大$x$，并一直在坐标轴上向右移。引理证明，迟早这个图形会相交到一点，$y=x$。因此，我们至少有一个数字，传递给函数F之后，其自身也是最后的G-number。
现在，哥德尔得到了拼图的所有部分，并将带来数学史上最大的震惊。在哥德尔的论文中，“定理VI” 非常复杂。这里是证明的思路，传统上一直用来描述其关键的发现。
如前面讲的，$provable(x)$设计成很多复杂的步骤，作为检查$x$是否是可证明的语句的函数。我们可以定义另一个函数，$NP(x)=$NOT$provable(x)$。“NOT”是逻辑上很简单的操作，变换其输入。$provable(x)$只能是真或者假，$x$要么是可证明的要么不是。“NOT”用来转换其结果。因为，$NP(x)$也是一元函数，我们可以对它使用对角引理。然后一定存在一个$g$，而$g=Godel-Number(NP(g))$。目前为止，还是容易理解的。然后我们对$NP(x)$做函数图，找到它与对角线相交的点，标记这个点为$g$。
构造另一个逻辑语句$G=$NOT $provable(g)$-现在$G$不再是一个函数，因为我们放的是指定的数字$g$，现在它只是个很长的逻辑表达式，按照$provable(x)$的复杂的逻辑语法扩展开得到的，-这里我们的指定的数字$g$代替自由变量$x$。这个特定的逻辑语句是真吗？可以证明吗？
思考一下。$provable(x)$对于任意$x$，它都可以告诉我们“真”或“假”。那么$NOT$ $provable(x)$也只能是“真”或“假”。现在我们用特别的数字$g$，并且要找到$G=NOT$ $provable(g)$的值。只有两个答案，真或假，那么是哪个呢？
考虑如果$G$为假会发生什么。好吧，我们定义$G$为“$NOT provable(g)$”。如果$G$为假，那么$provable(g)$就是真。因为我们可以用对角引理来找到数字$g$的编号，我们得到，$g=Godel-Number(NP(g))=Godel-Number(g)$。这意味着$provable(g)=true$把编码成哥德尔编码的$g$当作正确的证明!从一个假的证明，我们却得到了真的结论。Ka-boom!整个系统的一致性在一个大核爆炸中化为乌有：我们得到关于$G$的证明事实上是个假的语句！系统不一致了，能够证明一个假的语句为真，那就意味你能证明任何东西和每样东西。太糟糕了。
好吧，让$G$为假不是个好事，它立刻导致系统不一致。然后考虑如果$G$为真。我们显然更喜欢让系统维持一致-否则他就毫无用处了-唯一的选择就是假定$G$为真。回到定义，$G=$NOT $provable(g)$。如果 $G$为真，那么$provable(x)$一定为假。我们严格的，存在于$provable(x)$内部的逻辑历史告诉我们，“$g$并不包含我愿意作为有效证明接受的逻辑序列。在所有可能的能够编码到你系统中的，$g$恰好不在其中”。于是，没有这样一个逻辑推论的序列；没有可以用来证明$G$的东西。
如果$G$为真。同时又没有关于$G$的证明。G对于我们的逻辑系统是不可证的。如果证明是一些以路为网络联起来的村庄,那么所有的指向我们最初的公理的道路都不会到达$G$。但是$G$存在而且又为真-然而地图上却没有一条逻辑上的路径从公理出发到达$G$。从系统得到所有的推论都不会包含$G$，因此，系统是不完备的。
这正是哥德尔要说的，“任何...能够表达基本数学的形式系统不可能是既一致又完备的”。
如果要保持一致性，则不得不接受存在这样的$G$语句，为真，但是又不可证明，系统永远是不完备的。或者你能够坚持让他们变得可证明，但那又立即使得系统不一致。对于任何能够表达最基本的算术公理的系统，都只能选择一样，不能同时拥有。
关于哥德尔证明，有些东西是很令人惊叹的。我们通常认为逻辑系统是纸上枯燥而无聊的，古怪的符号序列。然而突然间，符号们好像活了过来。好像系统自己有了智慧并且开始对我们讲他自己的公理，什么是一个定理的正确推导，什么是可证明的语句。最终，这令人费解$G$语句构造出来，显示有些真的语句是写不出来的...，然而又永远不可能证明他们存在于系统之中。真相就在那里，...，却完全触摸不到！
到底有多少这种隐藏的知识呢？很明显是无穷的。这里则是原因。哥德尔之后更加努力地去证明，因为他想展示一个有趣的结论。假如我们把G作为一个公理加入到系统中呢？毕竟我们知道它是真的，因为不这样，系统就不一致。这样会不会让我们的系统变得完备呢？结果是，如果添加新的公理到系统，系统就变了！记得所有定义$provable(x)$的步骤吗？既然现在我们加入了新的公理到原本的公理列表之中，我们就必须退回我们之前用于定义$provable(x)$的每一步，因为我们增加了新的公理。那么现在，我们面对一个新系统，这个系统有一个新的$provable\prime(x)$函数，继而又会有新的$G\prime$语句。并且$G\prime$与第一个我们添加到公理中的$G$语句不一样。那么，我们新的扩展呢的系统，出现了第二个不可证的语句。重复同样的过程，我们得到$G\prime\prime$，$G\prime\prime\prime$，以至对于这个一直在扩展的形式系统，我们得到无穷多个真却不可证的语句。
如果有人现在完全迷惑了，这并不奇怪。$G$语句是非常抽象的构造。那么所有的形式系统是不完备的，我们怎么能够实际上用到这个事实呢？对于所有这些数学上无以匹敌的辉煌的哥德尔的证明，给予我们很多开始时候并不具备的东西。
在得到我们自己的，关于真实世界中的应用的推论前，让我们真正建造更多的关于形式系统这个陌生世界的领悟。如同台球互相以某个角度碰撞，然后走向不同的方向，要理解哥德尔的结论之中完整蕴含的内容，我们复习一些与之密切相关的，其他的重要数学成果。第一个，是图灵的停机问题。
【待续】
原文地址：http://www.cnblogs.com/mlnlp/p/3773959.html
