我知道你不知道我知道你知道

技术宅结城浩写了几本Java，C，Perl的书后估计是觉得程序猿的钱不好赚，于是打起了宅们的主意，一本数学少女就这么红起来了。第一次听说这本书还是大一，听介绍还挺有趣的，可惜当时没有中文版，真正看到还是几年后的事了。前些日子听说这书居然还出系列了，并且还漫画化了，我该说11区已经没有救了么。看了漫画第一话的内容，居然是经典的泥孩子问题，上次说到的模态逻辑和可能世界理论正巧能够用的上，那么既然上次只是很简单的说了一下大概，这次借这个机会我就再多说两句好了。

泥孩子问题是这样的：

想象一下有n个孩子在一起玩，他们的母亲告诉他们如果他们弄脏了自己，后果会很严重。所以，理所应当的，这些孩子不愿意自己变脏，但是却非常乐意别人变脏（这腹黑的……）。现在，我们假设在这n个孩子中有k个在玩的时候弄脏了他们自己的额头，每个人都能看到其他人的的额头但是不能看到他们自己的额头。所以，没人会坦白他看到了什么。当然为了不至于回家后面对不知道是什么的“很严重的后果”，他们一起来到了父亲那里。这个父亲显然也不是省油的灯，他并没有直接告诉这些小孩他们头上有没有泥巴，只是说了“你们之间至少有一个人头顶有泥巴”。之后这个父亲就一遍又一遍的问“你们知道自己头上有泥巴么？” 我们假设所有小孩都足够聪明，诚实，并且他们总是同时回答，那么将会发生什么？

我们先假设只有3个孩子，那么如果我们用一个三元组(q_1, q_2, q_3)来表示这三个孩子的状态，以0或1分别表示某人头上没有或有泥巴，则我们知道所有的可能世界有8种：（0，0，0），（1，0，0），（0，1，0），（0，0，1），（0，1，1），（1，0，1），（1，1，0），（1，1，1）。如果我们把“0个孩子头上有泥巴”，“1个孩子头上有泥巴”，“2个孩子头上有泥巴”，“3个孩子头上有泥巴” 分成4组的话，我们可以画出下面的这副图M_0：
Photobucket

其中每个点代表一个可能世界，这个可能世界的状态则被标注在旁边，那么边是按照什么规矩连接起来的呢？从数值上讲，是连接有且仅有一位与起始点不同的点，所以（1，0，0）可以连接（1，0，1），（1，1，0），（0，0，0）而不能连接（0，1，1）因为他们有3位不同而不是一位。从含义上来讲，由于某个点代表着一个可能世界，则和它连接的点就是这个可能世界的所有可能世界，但是这里稍微有点复杂，因为这些可能世界是从不同人眼里出发得到的可能世界。回到具体的含义上来，（1，0，0）代表了孩子A头上有泥巴而孩子B，C上没有，那么这个世界中，由孩子A看来，他知道B和C头上没有泥巴，但是不知道自己头上有没有泥巴，所以A的所有可能世界是（1，0，0）和（0，0，0）。同理，B的所有可能世界则是（1，0，0）和（1，1，0），C的就是（1，0，0）和（1，0，1）。

那么为了明确区分到底是谁眼里的可能世界，我们在每条边上对此做出标示，则这个图就可以变为M_1：
Photobucket Pictures, Images and Photos

所以在他们的父亲说任何话之前，所有可能世界和他们的关系就如上如图所示。但是，当父亲说：“你们之间至少有一个人头上有泥巴”的时候这些可能世界就发生了变化，（0，0，0）变成不可能的了，所以就成了这样，图M_2：
Photobucket Pictures, Images and Photos

此时，如果只有一个孩子头上有泥巴，那么头上有泥巴的那个孩子则必然知道自己头上有泥巴，而另外两个孩子则仍没有足够的信息来确定是否自己头上有泥巴。为什么呢？我们假设此时的世界是（0，0，1）那么以这个世界为基准，对于A而言虽然他不知道自己所在的世界，但是通过观察其他的两个孩子，他可以知道自己必定在（0，0，1）和（1，0，1）这两个世界其中之一，但是这两个世界里A头上有没有泥巴是不一样的，所以A无法判定自己头上有没有泥巴，B同理。唯独C在这里除了（0，0，1）外不存在其余的可能世界，所以对于C而言，他可以确定自己头上一定有泥巴。到这里，我们可以说，如果孩子们可以判断在所有可能世界里，自己头上有没有泥巴这件事情况都是一样时，他就可以确定自己头上有没有泥巴了。

那么数学上我们如何表示？在这里我们最终要推出的是A，B，C知道自己头上有（或没有）泥巴，于是如果我们用p表示自己头上有泥巴，q表示自己头上没泥巴，那么p，q就是我们常说的命题（一个能区分真假的语句），K_A，K_B，K_C分别表示A，B，C知道，我们把它们叫做模态算子。则K_A p的含义就是A知道自己头上有泥巴，如果我们再加入\lnot来代表否定，那么K_A \lnot K_B p就表示A知道B不知道自己头上有泥巴。当然这么下去也可以造出像标题一样绕口的句子，不过把人绕晕乎是没有任何好处的，就在此打住。所以上面提到的（0，0，1）世界的情况，我们就可以写为：

  • $$(M_2, (0, 0, 1))\models \lnot K_A p$$
  • $$(M_2, (0, 0, 1))\models \lnot K_B p$$
  • $$(M_2, (0, 0, 1))\models K_C p$$

这些式子的含义是，在图M_2所示的情况下，当世界为（0，0，1）时，A，B，C三者的知识情况，言下之意就是当世界为（0，0，1）时，A，B一定不知道自己头上有没有泥巴，而C一定知道自己头上有泥巴。

回到最初的问题，如果世界不是（0，0，1）而是（1，0，1）呢？(M_2, (1, 0, 1))又能得到什么？此时我们可以看到，无论是A，B，还是C，在（1，0，1）这个世界下，对于他们自己的总有另一个可能世界，在那个可能世界中自己头上有没有泥巴是不一样的，所以要是这样，他们都不会知道到底自己头上有没有泥巴，于是三人都会回答：不知道。这时情况又起了变化，当所有人回答不知道时，这就意味着必定存在着两个或两个以上的人，他们头上有泥巴，于是这个世界又变成了M_3:
Photobucket Pictures, Images and Photos

此时，除了对于B而言还存在两个可能世界以外，A，C均只有一个可能世界，所以在图M_3的情况下我们有：

  • $$(M_3, (1, 0, 1))\models K_A p$$
  • $$(M_3, (1, 0, 1))\models \lnot K_B p$$
  • $$(M_3, (1, 0, 1))\models K_C p$$

那么，当世界是（1，1，0）时也可以“同理可得”，就不用多说了吧。如果你对这些感兴趣，可以另外参考MIT出版的Reasoning About Knowledge，上面说的很详细，当然数学上也要严谨的多。

TNND，回头看这文的时候突然反应过来，这泥马的拿手摸一下不就知道有没有泥巴了，还弄得这么麻烦，搞数学的还真是没事干啊。

新受姬调教记

一切都得从父上非常折翼地买了个国行MOTO ME501说起。然后——各种用的不顺手。于是吾就和父上商量着换手机用。考研完了之后，觉得考的尚可，于是就换了。为什么说折翼呢？父上花了2600，也就是一台milestone的钱买了这个，这还不算，在吾刚入手的时候，就发现里面充斥这诸如ku6视频同花顺炒股之类的蛋疼软件，然后——卸载不能。然后，感谢党妈妈，感谢傻屄的moto，一台android系统的手机居然没有gtalk菜市场（android market）googlemap等等等等google应用，总之看着这惨不忍睹的受姬吾不由再次感叹一句，果然买国行的上辈子都是折翼的天使（附带一提堂哥买了个国行的E63，也就是吾之前用的，现在父上用的手机，那台已经被吾调教的各种乖巧，这下父上可以比较轻松的翻墙了……）。 当然了，不得不提这破手机居然还是1.5系统，茫茫多软件装不了，然后moto到现在还不给升级，看着人家HTC换固件就像女人换卫生巾一样，moto众（又不是吾要买moto的掀桌）内牛满面黯然神伤。

遇到问题，有三种应对措施：解决它，忍受它，绕开它。很明显作为每天都要朝夕相处的东西，后两个选项不在考虑之内。于是选项就只有解决它了。首先是google应用，上网查了一下，有个叫做GMS包，也就是google全服务的东西，可以用recovery模式（类似于电脑的BIOS?）刷上。于是就按着教程刷，刷完之后一进系统，要求输入google帐号，挺好，要的就是google服务，于是输入，然后——这泥马，google服务器连接不能，然后——不认证这个帐号就不给进系统。这难道就是传说中的变砖？嗯吾表示非常淡定，上网查了一下，发现有大大已经放出了1.5的官方ROM包（可以理解为1.5的安装包），于是轻车熟路的用recovery刷了回去。

首次尝试受挫，于是吾放低要求，总之先把那些让人蛋疼的原装软件删除再说。于是就需要root权限——android是基于linux的系统，最高权限就是root。还好有详细教程，于是依样画葫芦之后，ROOT权限到手。蛋疼软件看不到了，好开心。然后去搞了个山寨菜市场，乱七八糟下了些软件，结果一个比一个折翼，尤其是浏览器都没下一个能用的（自带的流量用着肉痛），于是春晚就懒得看了——都不能上推吐槽的说。

从大伯家（过年的聚集地）回来，上网查了一下，发现2.1的ROM已经趋近完美了（唯一的问题后面说），于是就准备动手刷机。由于已经有了root，于是按理说应该不难的。但是——他喵的居然这个时候又变砖了！初步判断是该死的山寨菜市场搞的鬼，因为重启之后依然会弹出来“您有⑨个软件需要更新”，然后一片华丽丽的黑屏。好吧变砖什么的习惯就好，刷回1.5系统，重刷root（刷过1.5root就没了FML）。然后刷recovery，就是把recovery的那个系统换掉，利用root权限在system文件夹下换掉一个recovery.img的文件就好了，非常容易，然后那个土的掉渣的recovery界面变得很漂亮，功能也强了很多。之后就是刷上hiapk上找到的最近的ROM，然后——神清气爽，google应用全都能用了，google服务器也轻松的登陆上去了，然后就是开机画面被换成了ubuntu囧，另外里面内置了很多不错的软件，root权限也是有的，媒体库也改进了茫茫多。唯一的问题就是——打电话有爆音。手机最初是用来通话的，但现在通话仿佛成了它最不重要的功能了，这还真是讽刺。嘛说唯一还不准确，在1.5系统下无法播放的flv格式文件到了2.1依然无法播放，于是吾只好继续内牛满面去了。 然而android究竟是个牛X的系统，比如刷root用到的connectbot可以连ssh，虽然貌似不能直接用来翻墙但是明显有这个理论上的可能性。弄得吾现在都想学一下linux系统了。总之刷机成功,メデタシメデタシ。

———————-分割线———————–

说起手机上网自然就是OPM（OPERA MINI）了。众所周知OPERA公司曾做过一个艰难的决定，就是推出了中国版。擅自用国际版会自动强制下载中国版。于是各路达人为了自己不可告人的秘密捯饬出了自定义服务器什么的，一个不到1K的index.php文件就可以break the sky，让人叹服道高一尺魔高一丈。然而与塞班系统有各种自定义服务器版不同，OPM for Android只能自己动手修改。到网上找了教程折腾了一天（当然不是一直在搞这个，中间也吃了饭睡了觉搅了基看了会明朝那些事），最后发现一个令人发指的事实：现在已经没有国际版和中国版之分了，所有的OPM发现手机是中国IP都会自动使用中国的中转服务器而不是强迫汝下载中国版。也就是说连米国人用的OPM都内置了中国的中转服务器，这是何等的尼玛。这导致的结果是，按着原来的教程无法修改新版的OPM，无论是从官网下载的还是从菜市场下载的。（据果子狸同学说还是有办法的，不过他提供的解决方案吾表示理解不能）。还好从另一个地方提供了比较旧比较纯洁的OPM5.1，总算是修改成功了。

嗯ME501到此就算是调教完毕了。除了不能放flv啊（喂）打电话会爆音啊（喂喂）在没啥缺点了。大概……

P.S：明朝那些事看了一会就有点腻了……记得当时临考前一天晚上开始准备复习（整学期没看过，所以应该是预习+学习？）然后去图书馆借专业书结果看到一本明朝那些事然后看到图书馆闭馆然后专业书也没接出来（电脑关了）然后第二天早上就考试了然后只好自己依靠天书一般的课件自己推测BB84协议是咋回事（第二天还就考了这个）。等等以上不是重点，重点是，吾果然对不务正业非常有爱，那天晚上看的各种有兴趣啊，果然那种明明已经火烧眉毛了还要浪费时间的快感吾完全无法拒绝么wwww

GEB读书笔记之二——形式系统的相容性

上次说到了形式系统大概是个什么样子，不过光用语言描述总是很抽象的，不好理解。那么就来举一个书上给出的例子来看看：

pq系统

  • 字符集：p   q    –
  • 公理：设 x 是包含且仅包含一个或多个字符’-‘的字符串，则 x-qxp- 是这个系统中的串。
  • 推理规则：设 x，y，z 的含义如上 x 所述，如果 xqypz 是这个系统中的一个串，则 x-qypz- 也是这个系统中的串。

这个系统就是这样了，字符集和公理应该很好理解，至于最后的推理规则，虽然不难，但是对有些人可能看上去有点陌生。这种形式的定义我们一般称之为递归定义，至于递归的含义，有一个关于它的经典笑话：

     递归 [名词]：见递归。

这个笑话很形象的描述了递归的一个特点：自己定义自己。这听上去有点坑爹，自己定义自己不是说永远没完么？是的，所以递归的定义和这个有区别，自己定义自己没错，但是重要的一点是：定义用的是简单一些的版本，并且，起点是给定的。那么在这里，起点就是已经是系统中的，形如 xqypz 的串。那么这种串又是哪来的呢？向上看，这种串是由公理给出的。如果要再举一个例子的话那就是数学里著名的斐波那契数列，我们将这个数列的第 i 个数表示为 Fib(i) 则我们有：

  1. Fib(0) = 0
  2. Fib(1) = 1
  3. Fib(n) = Fib(n – 1) + Fib(n – 2)     (n > 1)

是不是很类似呢？好了，理解了这个我们就可以先来试试看看 pq 系统里都有哪些字符串。最简单的当然是当 x 只是一个 – 的时候，那么按照公理,字符串 – -q-p- 就可以算一个。之后由于有了这个串，我们就可以按照推理规则进行扩充，在这里，x 是 – -，y 是 – ，z 是 – ，所以扩充后就会变为 – – -q-p- – 。数一数，不要眼花了哦。按照这种想法，我们就可以生成不计其数的这个系统里的字符串。那么也许你很快就注意到了，所有的字符串，无论它们有多么长，长相都会是形如 “一堆横杠后面跟着一个q，q后面再来一堆横杠，之后连着一个p，p之后再有若干个横杠，结束”  凡是不是这个形式的串，肯定不会是这个系统中的串。于是我们把这种形式的串叫做良构的（Well-Formed）。这也是之前所说的特定的排列顺序，这是由规则决定的。

那么我们知道了只有这个形式的串才有可能是系统中的串，但是这并不意味着凡是这种形式的串都是这个系统中的串。那么有没有什么办法来判定任意这种形式的串是不是这个系统中的串呢？这个并不难，如果你愿意考虑一下的话可一先停在这里。如果你写了足够多的串，那么应该可以发觉这些串都有一个相似的性质，这个性质就是在字母 q 前的横杠个数等于在q，p之间的横杠个数与 p 之后的横杠个数的和。换句话来说，这个系统和加法有着异曲同工之妙。如果我们把q解释为等于，p解释为加法，- 解释为数字1，- – 解释为数字2，等等，我们就可以把这个系统中的每一个串翻译为一句形如“3等于2加1”之类的正整数加法等式，我们把这个叫做形式系统的解释，而正整数加法和这个形式系统的关系我们称之为同构，就如同“苍井空.rmvb”和显示器上的图像的关系 就如同“爱情买卖.mp3”和从你音响里发出的噪音音乐一样。那么，解释是唯一的吗？答案是否定的，如果稍加考虑我们就可以给出另一个解释：对于横杠的解释不变，但是将 q 解释为减法，p 解释为等于。虽然我们改变了解释，但是这个系统仍旧可以解释的通。

刚才说到了“可以解释的通”，这实际上就涉及到了形式系统的一个重要性质：相容性。或者叫无矛盾性，一致性。显然的，有矛盾的东西对于我们而言价值不大，我们想要的系统理所应当应该是无矛盾的。书上将这一性质分成了两层，外部一致性和内部一致性，外部一致性比较好理解，它指的是系统中的每一个定理（在pq系统中就是那些公理和由推理规则生成的串）经过解释后都成为一个真的陈述。即所有系统中的陈述都与外部世界相符，这里的外部世界自然就是我们的世界了。而内部一致性则是指系统中不存在两个或更多的定理，他们之间是彼此不相容的。一个最简单的例子就是如果一个系统中同时有“小明今天早上造的桌子A是方形的”和“小明今天早上造的桌子A是圆形的”，那么这个系统就是内部不一致的。因为虽然我们也许不知道小明今天早晨造的桌子A是什么样的（甚至小明到底会不会造桌子我们也不知道），但是我们可以肯定这个桌子不可能既是方的又是圆的。这其实就是我们判断一个系统是否是内部一致的过程：我们先想象一个世界，这个世界要尽量符合这个系统内的所有定理。像上面，我们想像一个存在小明的世界，并且这个小明能够造桌子，但是我们再怎么想也想不出一个桌子要怎样才能即是方形的也是圆形的，所以我们说这个系统不是内部一致的。换句话说，如果这两个命题是“小明今天上午睡觉了”和“小明今天下午跑步了”，我们就可以想象出一个世界，在这个世界里小明上午睡觉了并且小明下午跑步了，所以我们说这个系统是内部一致的。需要注意的是现实世界里小明到底做了什么无所谓，在内部一致里，只要在我们的一个想象的可能世界里所有的陈述之间没有冲突就可以了。

不过想象的可能的世界这种说法有点坑爹，我偏要想一个桌子即是圆的又是方的的世界你能把我咋地？（好吧，其实我承认我想不出来）作者给出的结论是说想象的世界要和真实世界的数学和逻辑相一致才行。不知道多少人愿意就这么算了，凭啥只是数学和逻辑，物理呢？生物呢？化学呢？语文呢？政治正确性都不顾了你想死么？所以这里就让我多解释一下。不过这里要牵扯到模态逻辑和可能世界理论，当然只是初步的。首先在一般的逻辑里，一个命题（能够判断真假的语句）的表述方式无非有两种：直接表示和添加否定的表示。但是在模态逻辑里，增加了“可能”和“必定”两种“形容词”，也就是说，一个命题，比如“Sony是业界的良心” 在一般的逻辑里顶多可以再表述为“并非Sony是业界的良心”。而在模态逻辑里，还可以表示为“有可能Sony是业界的良心”和“一定有Sony是业界的良心”。虽然这些命题的真假在你看来可能取决于考虑问题的人是任青，索匪，还是果粉（？）。但是在可能世界理论之下，我们如何定义这些命题的真假呢？下面以一定为例，解释真值是如何定义的。

     命题 A 在某一可能世界里是必然的,当且仅当 A 在那个世界的所有可能世界里都是真的

由此可见，首先在判定一个以一定开头的命题的真假时，我们会限定说它在某一基本的可能世界里。之后，我们说如果在那个可能世界的所有可能世界里这个命题都是真的，那么原命题为真。这里稍微有点绕，那么来举个例子好了：我们首先限定我们当前的世界是讨论问题的基本的可能世界，那么这样的话“任天堂是游戏业霸主”的世界，“索尼是游戏业霸主”的世界，和“苹果是游戏业霸主”的世界，就是我们当前世界的可能世界，但是“雅达利是游戏业霸主”的世界就不是我们当前世界的可能世界了，因为它已经死了。（现在的雅达利和以前的没什么关系，就像现在的AT&T和以前的AT&T不是一回事一样）

所以说，在这里，提到可能世界，我们总有一个基准，“所有可能世界”不是指绝对意义上的所有可能世界，而是与基准世界相关联的所有可能世界。如果某一个可能世界里的规则与基准世界里的规则相矛盾，那么这个可能世界就不是我们想要的可能世界，他对于我们没有意义。所以回到主题，在内部一致性里，我倾向于把我们现实世界当作基准，那么如果存在一个在这基准之上的可能世界，在那个世界里系统中的所有定理的解释之间都不存在矛盾，则我们说这个系统是内部一致的。所以此时一个“桌子同时是方的和圆的”的可能世界就不是一个可以被接受的可能世界了，因为在基准世界（我们的世界）里，这是不可能的。

好了，那么关于形式系统的相容性大概就是这么多了，下次应该就是关于形式系统的另外一个重要性质了。下一次应该可以和哥德尔扯上关系了……吧—_卅……

GEB读书笔记之一——形式系统初步

之前开始学数理逻辑的时候听说了《哥德尔，艾舍尔，巴赫》这本书，不过实在是太忙，这书又很厚，结果最后并没有去看。前两天看到Twitter上有人提到这本书再版了，正好现在放假无事，于是便到书店把这本书买了回来。要说这本书里讲到的哥德尔不完备性定理，可以说是上个世纪人类最为伟大的发现了，不过似乎听说过的人并不多，这的确很可惜。译者在前言里称这本书是一本奇书，我觉得不虚此言，总之看的我是非常的兴奋。所以作为看书后的回顾，这里就记录一些阅读后的感想，供自己作为回顾以及没时间看书又想稍作了解的人。

在谈论哥德尔伟大的定理之前我们需要了解一些基本的概念，首先就是形式系统。不过在解释什么是形式系统之前请让我们回想一下初中学过的几何。如果你用过人教2000年版的初中数学书的话你一定还记得那本和代数一样厚（或者反过来说也一样）的几何，里面充斥着诸如“公理”“定理”一类的表述。如果你和我一样对这些表述并不以为然并且认为它们基本上是一回事的话，那么恭喜你，你和我一样犯下了一个严重的错误。不过这个错误并不会影响到你的中考或者高考成绩，所以大概从考试的角度来说这并不严重。但是如果我们要讨论形式系统的话我们还是先搞清楚这两个词是怎么回事。

首先是公理：

公理是无法被证明或决定对错，但被设为不证自明的一个命题。

也就是说，公理是一切证明的起点，它被视为是理所应当的。所以，公理应该是一些简单的，而且符合直觉的陈述。那么回过头来看看我们当时几何，也就是欧几里德几何中的那些公理：

  1. 任意两个点可以通过一条直线连接。
  2. 任意线段能无限延伸成一条直线。
  3. 给定任意线段，可以以其一个端点作为圆心，该线段作为半径作一个圆。
  4. 所有直角都全等。
  5. 若两条直线都与第三条直线相交，并且在同一边的内角之和小于两个直角，则这两条直线在这一边必定相交。

是不是很浅显易懂并且你会认为是理所应当的？当然了，你可能看着第5条公理不是那么的浅显易懂，是的，欧几里德也这么想，很多人都这么想，以至于由这条公理生出了其他的几何学说！这个我们之后再说。最后一个公理的一个等价表述其实是“通过一个不在直线上的点，有且仅有一条不与该直线相交的直线。”这个是不是稍微浅显一些？

那么定理呢？

定理是经过受逻辑限制的证明为真的陈述。

也就是说定理与公理都是真的,但是两者最大区别是定理需要证明。那么所谓的经过受逻辑限制的证明又是什么东西？与其找个解释，我想我们不如直接来看看欧几里德是怎么证明其几何中的定理的：

定理1：通过一个已知有限长的直线可以作一个等边三角形

Photobucket

设AB是已知有限直线

  1. 以A为圆心，以AB为距离画圆B\Gamma\Delta 。 (公理3)
  2. 以B为圆心，以BA为距离画圆A\Gamma E 。 (公理3)
  3. 由两圆的交点\Gamma向A，B连线。\Gamma A，\Gamma B (公理1)
  4. 因为点A是圆B\Gamma\Delta的圆心，所以AB=A\Gamma。
  5. 因为点B是圆A\Gamma E的圆心，所以BA=B\Gamma。
  6. 因为已经证明了A\Gamma=AB，所以B\Gamma，A\Gamma都等于AB。
  7. 所以三条线段B\Gamma，A\Gamma,AB彼此相等。
  8. 所以三角形AB\Gamma是等边的，即在个已知有限长的直线AB上作出了一个等边三角形。

好了，证明结束，我想如此简单的证明不会有人看不懂吧，那么现在我们回过头来看看这个证明是怎么做到的。前3步是之前提到的公理，是最基本的东西，我们可以直接这么做而不必多加考虑，因为理智告诉我们这样一定没错。而4-6步呢？他们都是“因为…所以…”的句式，这个句式告诉我们，由于“因为”给出的前提条件，可以得到“所以”当中的结论。并且，如果“因为”所说的是正确的，那么，“所以”当中的结论也一定正确。在这里，这个正确性是显然的（好吧，我知道有些数学证明的一个偷懒技巧就是在不会证的时候写“显然可得”但是我相信这里的结果对于任何一个心智正常的人而言都是显然的）。这其实就是一种逻辑：当你接受前提“因为”时，你就要接受结果“所以”。而到了第7步，则是由第6步的结论而自然得到的结果。最后，在第8步，由于有了上一步的结论，我们得到了我们想要有的那个三角形。

这就是一个典型的证明过程，由逻辑将一些正确的事物连接到一块，并且，得到另一个正确的结论，再而且，这个过程被我们的理智所认可。到这里就比较好玩了，我们有了公理，有了逻辑规则，而且这些东西看上去又相当有规律，那么是不是我们可以弄出一套东西来，这套东西里有公理，有规则，然后只要通过公理和规则进行推理，那么就能得到有用的结论呢？特别的，这套东西最好能让机器来做，我们把公理和规则输入进去，机器来给我们给出源源不断的正确结论，要是这个系统要是能够包含一切的现实规律，那就更好了。这样我们就可以放手让机器去给我们创造一切，我们自己就可以活在没有饥饿没有寒冷的新闻联播的世界里了。我X，想想就给力啊！

是够给力，而这个的实现便是数学中的形式系统。欧几里德几何本身已经有那么些形式系统的意思了，比如说作为基础的公理，比如说严密的逻辑推理。不过并不够，欧氏几何的推理是由自然语言做的，虽然已经足够简单，但是还是不够简单，并且，自然语言的复杂性，二义性也不是可以轻松就发觉的。另外，还记得那个看上去不怎么顺眼的第五公理么？历史上有不少人想要证明这个公理可以不用，大量的尝试竟然衍生出了其他的系统，比如说椭圆几何，仅仅将第五公理所说的“过直线外一点有且仅有一条直线与之平行”否定为没有直线与之平行，再加上其他的4公理，就能推出一套自己的系统。这样初看会觉得造成了系统的矛盾，但是让我们想一想，我们会觉得矛盾的原因是什么？关键就是在欧氏几何中提到的“点”，“线”这些东西，我们要怎么解释？这个问题可能有点奇怪，“点”就是点呗。但是如果我们跳出“点”这个词给我们固有印象，假装把它当作一个没有意义的符号（或者干脆换个不认识的字，免得我们潜意识里的联想，比如用“齾”），然后重新进行解释，我们就会发现，如果把“点”解释为球上直径的一对端点，把“线”解释为以球直径做为直径的球面上的圆，一切就迎刃而解了，此时公理1“任意两个‘点’可以通过一条‘直线’连接”是不是也能解释的通？两条‘线’不可能无交点是不是也能解释的通？也就是说普通的点的概念并不是这里“点”的唯一解释！那么是不是说我们可以抛弃这些具体的概念，而是使用一些抽象的，和具体现实无关的词汇，而在使用时根据需要给这些抽象词汇予以解释呢？是的，而这正是形式系统所要做的。

那么按照上面的想法，让我来叙述一下什么是形式系统。

首先我们需要一个抽象的符号集合，从某种意义上讲，符号和现实生活的联系越少越好，免得使我们产生不必要的联想。但是实际上，形式系统在怎么样也是要实用的，所以其中符号还是难免要和现实紧密联系起来，免得在我们的理解上造成太大的麻烦（你能想象一个充斥着“棏彎嗄齾”之类完全看不懂的字的一个系统么？）

其次，一套文法。我们要知道如何将这些符号按照一定的规则组织到一起。胡乱堆放到一起的字符是没有意义的，他们的顺序需要有规则来确定。

然后是上面已经提到多次的公理–推理的基础。还有推理规则，这些规则一般是非常简明的，足以让机器也能实现的“死”规则

最后，有了上面的东西，我们可以得到一些定理，这些定理的集合就是这个形式系统的理论。

需要再次强调的是，形式系统里的字符是高度抽象的，所以，任何想当然的结论都是危险的，例如，如果形式系统公理中有a+b，这并不意味着b+a也是公理，而是需要证明的，因为+并不是加法，而仅仅是一个符号。对于符号的解释是之后按照我们的需求，或者对这个系统本身含义的观察得出的。并且，解释也不是唯一的。

这样我们就对形式系统有了一个初步的了解，之后我会举例说明一个书上的讲到的简单的形式系统，以及容易产生的误解。当然还有形式系统的两个重要性质。听说文章太长了没人看，所以这些就推后吧。