之前开始学数理逻辑的时候听说了《哥德尔，艾舍尔，巴赫》这本书，不过实在是太忙，这书又很厚，结果最后并没有去看。前两天看到Twitter上有人提到这本书再版了，正好现在放假无事，于是便到书店把这本书买了回来。要说这本书里讲到的哥德尔不完备性定理，可以说是上个世纪人类最为伟大的发现了，不过似乎听说过的人并不多，这的确很可惜。译者在前言里称这本书是一本奇书，我觉得不虚此言，总之看的我是非常的兴奋。所以作为看书后的回顾，这里就记录一些阅读后的感想，供自己作为回顾以及没时间看书又想稍作了解的人。
在谈论哥德尔伟大的定理之前我们需要了解一些基本的概念，首先就是形式系统。不过在解释什么是形式系统之前请让我们回想一下初中学过的几何。如果你用过人教2000年版的初中数学书的话你一定还记得那本和代数一样厚（或者反过来说也一样）的几何，里面充斥着诸如“公理”“定理”一类的表述。如果你和我一样对这些表述并不以为然并且认为它们基本上是一回事的话，那么恭喜你，你和我一样犯下了一个严重的错误。不过这个错误并不会影响到你的中考或者高考成绩，所以大概从考试的角度来说这并不严重。但是如果我们要讨论形式系统的话我们还是先搞清楚这两个词是怎么回事。
首先是公理：
公理是无法被证明或决定对错，但被设为不证自明的一个命题。
也就是说，公理是一切证明的起点，它被视为是理所应当的。所以，公理应该是一些简单的，而且符合直觉的陈述。那么回过头来看看我们当时几何，也就是欧几里德几何中的那些公理：
- 任意两个点可以通过一条直线连接。
- 任意线段能无限延伸成一条直线。
- 给定任意线段，可以以其一个端点作为圆心，该线段作为半径作一个圆。
- 所有直角都全等。
- 若两条直线都与第三条直线相交，并且在同一边的内角之和小于两个直角，则这两条直线在这一边必定相交。
是不是很浅显易懂并且你会认为是理所应当的？当然了，你可能看着第5条公理不是那么的浅显易懂，是的，欧几里德也这么想，很多人都这么想，以至于由这条公理生出了其他的几何学说！这个我们之后再说。最后一个公理的一个等价表述其实是“通过一个不在直线上的点，有且仅有一条不与该直线相交的直线。”这个是不是稍微浅显一些？
那么定理呢？
定理是经过受逻辑限制的证明为真的陈述。
也就是说定理与公理都是真的,但是两者最大区别是定理需要证明。那么所谓的经过受逻辑限制的证明又是什么东西？与其找个解释，我想我们不如直接来看看欧几里德是怎么证明其几何中的定理的：
定理1：通过一个已知有限长的直线可以作一个等边三角形
设AB是已知有限直线
- 以A为圆心，以AB为距离画圆B\Gamma\Delta 。 (公理3)
- 以B为圆心，以BA为距离画圆A\Gamma E 。 (公理3)
- 由两圆的交点\Gamma向A，B连线。\Gamma A，\Gamma B (公理1)
- 因为点A是圆B\Gamma\Delta的圆心，所以AB=A\Gamma。
- 因为点B是圆A\Gamma E的圆心，所以BA=B\Gamma。
- 因为已经证明了A\Gamma=AB，所以B\Gamma，A\Gamma都等于AB。
- 所以三条线段B\Gamma，A\Gamma,AB彼此相等。
- 所以三角形AB\Gamma是等边的，即在个已知有限长的直线AB上作出了一个等边三角形。
好了，证明结束，我想如此简单的证明不会有人看不懂吧，那么现在我们回过头来看看这个证明是怎么做到的。前3步是之前提到的公理，是最基本的东西，我们可以直接这么做而不必多加考虑，因为理智告诉我们这样一定没错。而4-6步呢？他们都是“因为…所以…”的句式，这个句式告诉我们，由于“因为”给出的前提条件，可以得到“所以”当中的结论。并且，如果“因为”所说的是正确的，那么，“所以”当中的结论也一定正确。在这里，这个正确性是显然的（好吧，我知道有些数学证明的一个偷懒技巧就是在不会证的时候写“显然可得”但是我相信这里的结果对于任何一个心智正常的人而言都是显然的）。这其实就是一种逻辑：当你接受前提“因为”时，你就要接受结果“所以”。而到了第7步，则是由第6步的结论而自然得到的结果。最后，在第8步，由于有了上一步的结论，我们得到了我们想要有的那个三角形。
这就是一个典型的证明过程，由逻辑将一些正确的事物连接到一块，并且，得到另一个正确的结论，再而且，这个过程被我们的理智所认可。到这里就比较好玩了，我们有了公理，有了逻辑规则，而且这些东西看上去又相当有规律，那么是不是我们可以弄出一套东西来，这套东西里有公理，有规则，然后只要通过公理和规则进行推理，那么就能得到有用的结论呢？特别的，这套东西最好能让机器来做，我们把公理和规则输入进去，机器来给我们给出源源不断的正确结论，要是这个系统要是能够包含一切的现实规律，那就更好了。这样我们就可以放手让机器去给我们创造一切，我们自己就可以活在没有饥饿没有寒冷的新闻联播的世界里了。我X，想想就给力啊！
是够给力，而这个的实现便是数学中的形式系统。欧几里德几何本身已经有那么些形式系统的意思了，比如说作为基础的公理，比如说严密的逻辑推理。不过并不够，欧氏几何的推理是由自然语言做的，虽然已经足够简单，但是还是不够简单，并且，自然语言的复杂性，二义性也不是可以轻松就发觉的。另外，还记得那个看上去不怎么顺眼的第五公理么？历史上有不少人想要证明这个公理可以不用，大量的尝试竟然衍生出了其他的系统，比如说椭圆几何，仅仅将第五公理所说的“过直线外一点有且仅有一条直线与之平行”否定为没有直线与之平行，再加上其他的4公理，就能推出一套自己的系统。这样初看会觉得造成了系统的矛盾，但是让我们想一想，我们会觉得矛盾的原因是什么？关键就是在欧氏几何中提到的“点”，“线”这些东西，我们要怎么解释？这个问题可能有点奇怪，“点”就是点呗。但是如果我们跳出“点”这个词给我们固有印象，假装把它当作一个没有意义的符号（或者干脆换个不认识的字，免得我们潜意识里的联想，比如用“齾”），然后重新进行解释，我们就会发现，如果把“点”解释为球上直径的一对端点，把“线”解释为以球直径做为直径的球面上的圆，一切就迎刃而解了，此时公理1“任意两个‘点’可以通过一条‘直线’连接”是不是也能解释的通？两条‘线’不可能无交点是不是也能解释的通？也就是说普通的点的概念并不是这里“点”的唯一解释！那么是不是说我们可以抛弃这些具体的概念，而是使用一些抽象的，和具体现实无关的词汇，而在使用时根据需要给这些抽象词汇予以解释呢？是的，而这正是形式系统所要做的。
那么按照上面的想法，让我来叙述一下什么是形式系统。
首先我们需要一个抽象的符号集合，从某种意义上讲，符号和现实生活的联系越少越好，免得使我们产生不必要的联想。但是实际上，形式系统在怎么样也是要实用的，所以其中符号还是难免要和现实紧密联系起来，免得在我们的理解上造成太大的麻烦（你能想象一个充斥着“棏彎嗄齾”之类完全看不懂的字的一个系统么？）
其次，一套文法。我们要知道如何将这些符号按照一定的规则组织到一起。胡乱堆放到一起的字符是没有意义的，他们的顺序需要有规则来确定。
然后是上面已经提到多次的公理–推理的基础。还有推理规则，这些规则一般是非常简明的，足以让机器也能实现的“死”规则
最后，有了上面的东西，我们可以得到一些定理，这些定理的集合就是这个形式系统的理论。
需要再次强调的是，形式系统里的字符是高度抽象的，所以，任何想当然的结论都是危险的，例如，如果形式系统公理中有a+b，这并不意味着b+a也是公理，而是需要证明的，因为+并不是加法，而仅仅是一个符号。对于符号的解释是之后按照我们的需求，或者对这个系统本身含义的观察得出的。并且，解释也不是唯一的。
这样我们就对形式系统有了一个初步的了解，之后我会举例说明一个书上的讲到的简单的形式系统，以及容易产生的误解。当然还有形式系统的两个重要性质。听说文章太长了没人看，所以这些就推后吧。