阿宅们，好好读书啊！

如果你有看过凉宫春日系列的话，应该还记得在《凉宫春日的烦闷》里的 “竹叶狂想曲一章”（话说提到这个我每次的第一反应就是某人在某年七夕很淡定的去校北门拔了一个竹子然后大摇大摆的放回宿舍做许愿竹的事），阿虚受1096的委托和她一起回到了过去，又在老1096的色诱下帮春日在校园里画了一操场的火星文，可惜画完后小1096才发现时光机器不见了以至于回不去了，最后他俩只能去大萌神的家里同床共枕到3年后了（3年间就睡了一次觉，一次睡了3年…不对，可恶啊，阿虚你怎么不去死一万遍啊！）。回来之后的阿虚对时空跳跃的过程感到莫名其妙，就在他在SOS团活动室里胡思乱想这次时空跳跃似乎哪里有问题的时候，大萌神说到：

     相容的系统无法证明自己的无矛盾性

这其实就是哥德尔第二部完备性定理的一种表述，萌神用这句话成功的让阿虚闭了嘴，不过阿虚也不像是真懂了的样子，更像是反正无法理解那就干脆不要理解了的样子。其实这也不能怪阿虚学艺不精，毕竟这玩意也的确不好理解，书上对于证明也是一带而过，只是说和第一不完备性定理思路差不多，并不难证明（好吧，看见“不难证明”这四个字你懂了么？）。我当年上数理逻辑课的时候老师在花了2次课6个课时的时间证明了哥德尔第一不完备性定理后也说由于第二不完备性定理的证明过于复杂所以略去了证明只讲了结论。所以这个定理的证明在这里也只能微讲一下思路了。

哥德尔的证明是在系统的内部构造一个“此系统一致”的句子，之后证明了如果这个句子是系统中的定理，那么同时“此系统不一致”也会是这个系统的定理。然而一旦这两个句子都是系统中的定理，则显然的，系统不相容。这也说明了，除非系统不相容，否则我们没法证明系统是一致的，但是……不一致的系统证明了又有毛用啊，因为在不一致的系统中所有能在系统内表示的句子都是真的，这对我们没有任何用处。就如同虽然你能包含所有的真理，但是也包含了所有的假理，这种东西除了一小撮别有用心的人喜欢拿来骗广大的人民群众外正常人是不会对这种东西感兴趣的。

第二不完备性定理在某些方面看上去有些令人不安，特别是如果你认为一切东西都需要证明才能保证正确性的话。由于哥德尔第二不完备性定理的存在，一个系统的正确性证明只能依赖于另外一个系统，因为自己没办法证明自己。但是这就如同一个一环套一环的锁链，当然可以一步一步的证明下去，不过当证明到这条锁链的一个顶端时我们该如何呢？它的正确性该如何证明？如果不能，我们之前证明的那些又能够算得上可靠么？所以，数学是可靠的么？更进一步，也有人相信这个锁链的最后一环应该是人的理智，所以说，人的理智是可靠的么？

这些论调听上去有些恐怖，毕竟数学无处不在，现代科学又建立在人的理智之上，如果这两样东西都不可信的话那还真的是2012了。不过我倒是觉得大可不必，最好的论据就是我们现在活的很好，几千年都过来了，总体而言没有出什么BUG。数学不可信？我不这么觉的，没有数学怕是我们连可信不可信这个概念都没有，还讨论个屁啊。理智不可信？那我倒想问问不信理智了你信什么？动物的本能？那我们怕是现在还和黑猩猩没有什么区别。所以说真的无法证明？大丈夫萌大奶！几千年的经验告诉我们这些东西还是可以相信的，而且至今为止也没有什么东西看上去比数学更可信，所以大可不必担心啦～你觉得呢？

那么下一篇文章，虽然还有不少东西，但是看上去都已经偏向哲学的范畴了，所以合起来讲吧，颇有些玄妙的东西我也不懂啦……

在继续折腾数学之前我们先来看看计算机中的一个类似的问题吧。作为程序猿，提到新的一门语言，大概都是是先学“Hello World”怎么说（相对的，正常人一般会先学“我爱你”怎么说）。一般来说提到Hello World程序那必定就是非常简单的程序了，不过我们想像这样一个程序：这个程序接收输入n，之后寻找方程 \(x^n+y^n=z^n\) 的整数解，如果找到，则打印Hello World，如果没找到，则继续搜索下去并不打印任何东西。那么如果我们有另外一个程序，这个程序可以判定之前那个程序是否能够显示Hello World，如果能显示就输出Yes，不能的话就输出No。这其实就相当于一个费马大定理的验证程序，相似的，我们还可以弄出证明XXXX猜想的程序，数学家们耗费几百年才解决或者至今都没有解决的问题就能被我们计算机工作者轻松加愉快的解决了耶～～～那么这种程序真的可能做出来么？ 答案一如既往的悲剧：否。

我们的想要做的程序可以由下面的图来说明，假设我们想要做的程序是H，它可以接收另外一个程序 P 和输入 I 作为输入，其用于断定带输入 I 的程序 P 是否显示Hello World，如果是，则程序H输出Yes，否则输出No。我们将证明这种程序H是不存在的。

运用归谬法，假设这样的程序H存在，我们将其做一些修改，修改后的程序我们称之为\(H_1\)，但是其与H没有本质的不同。这样的修改是：当H输出为No的时候，\(H_1\)输出Hello World。

第二步，我们让 P 的输入 I 就是 P 本身，这个可以由编码来实现，类似于上次讲的哥德尔配数，程序也是可以编码的。之后我们就只需要输入 P 而不是 P 和 I 了。此时构造程序\(H_2\)，其在\(H_1\)的基础上做如下修改：

• 读入整个输入P并保存
• 之后模拟\(H_1\)，只是当\(H_1\)读取输入时\(H_2\)就读取上一步保存的副本

最后的示意图可以如下所示：

那么现在就可以证明\(H_2\)是不存在的。因为如果我们把\(H_2\)当做输入 P 喂给它自己，这时就会出现悖论。首先，如果判定程序\(H_2\)输出Yes，则意味着\(H_2\)以自身作为输入显示Hello World，但是刚才我们假设\(H_2\)输出的是Yes而不是Hello World。同样的，如果假设\(H_2\)以自身作为输入输出的是Hello  World，则判定程序\(H_2\)输出一定是Yes。所以无论假设\(H_2\)有什么输出，都能推出其有另一个输出。这就造成了悖论，解决这个悖论的方法就是承认\(H_2\)不存在，所以\(H_1\)也不存在，所以H也不存在。

哥德尔的证明和上面的类似，哥德尔在我们所说的那个足够复杂的系统中构造了一个自指的命题，这个命题为真，并且这个命题在那个系统下不可证，于是两全的企图被打破了，想活在新闻连播中？那么只有自己努力喽。不过在说明哥德尔用了什么命题之前，先来看看自指是什么意思：

在这个视频里，Carl在说My voice is higher than your voice时会同时提高声音，可以说这句话自己提到了自己，这种感觉很奇妙，因为一般来说我们说的一个句子都是在讨论其他东西，而这个句子却在说自己，再举个例子：“这句话有七个字”，告诉了我们一个关于这句话自己的事实：它有七个字。这种句子听上去也许不是很舒服，但却是哥德尔证明中重要的东西。

之后就明说了吧，我们为了证明希尔伯特方案是不可能的，需要构造一个能够推翻它的定理，这个定理满足如下条件：

• 在那个足够复杂的系统内部可以表示。
• 这个定理是真的。
• 这个定理在那个复杂系统中不可证。

能够在复杂系统内部被表示是一个必要条件，否则谈何“在该系统下可证”这个性质（自己都表示不了的东西可不可证无所谓）。那么哥德尔想要构造的命题就是：“本命题不是系统的定理”。但是，直接这么说是不行的，因为这句话是没法表示成系统中的定理的。原因某种程度上是显然的，这句话形容的是系统的一个性质，但是，系统内部的定理是不会形容系统本身的性质的，就像几何学中的定理讲述的是点，线，面等的性质而不是几何的性质。只有有了几何这个整体的概念后我们才会说出几何本身的性质是什么什么。所以直接这么说是不行的，那么就只有来构造一个和这句话等价但是在系统内部可以表示的命题。这就要利用到之前说到的哥德尔配数了。

首先我们要表示不可证这个概念，因为我们已经把系统中各个定理表示成数的形式了，所以每个定理有一个数来表示，并且每个定理的证明过程也能由一串数来表示，就像上次说的4=1+3就可以表示为11110100111，而证明的过程就是把那三步的数连接起来，当然要用一个其他的数分割每个步骤，假设用2吧，则证明过程就可以数字化为11010012111010011211110100111。
于是
（11110100111，11010012111010011211110100111）
就是一个证明对。一对数是否是正确的证明数这个问题是可以在有限的步数内得到证明的，人工的方法无非是将数字翻译回来，在推导中一步一步看下去，看看哪些是公里，哪些不是，对于不是的则可以检查其是否可以从某个规则中推理出来。这样就能证明两个数组成的对是否是一个真的证明对了。这其实就是可证——两个数构成一个证明对，与不可证——两个数无法构成一个证明对的表示。而且由于其可在有限步骤里证明，所以其是可以在系统中表示的。

之后我们要想如何能让定理自己描述定理。书上自创了一个词“摁”，我估摸着作者用这两个字想要表达的意思就是用手把自己融汇并按入到自己里面，所以又是提手旁又是汇又是恩的，这听上去口味有点重啊……撇开口味不谈，摁的前提是有一个至少有一个自由变元的公式，这里的自由变元有点像方程中的未知数，你可以将不同的数代入到那个未知数中。所以在摁的意义下，我们首先计算公式的哥德尔数，之后将这个哥德尔数代入到原来公式的自由变元中，得到的新公式的哥德尔数被称作原哥德尔数的算数摁化。给定两个数，能否在有限步骤中确定一个数是不是一个数的算数摁化？答案是可以，人工做也不难，首先将一个数翻译回原本的公式，之后将其中的自由变元拿刚才的数代替，最后计算出新公式的哥德尔数，将其与另一个数比较，相同则这两个数中一个是另一个的算数摁化，否则则不是。可见这些工作都能在有限步骤中完成，所以算数摁也是可以在系统中表示的。

准备工作就此完成了，我们来构造最后的公式吧：

公式G’：不存在 a 和 a’ 使得: （1）a 和 a’ 是证明对; 并且（2）a’ 是 a” 的算数摁化。

这个公式显然存在一个哥德尔数，我们假设其为 u，随后我们将这公式里的自由变元 a” （注意 a 和 a’ 不是自由变元，它们在公式的开头被提到了）用 u 来代替，则得到

公式G：不存在 a 和 a’ 使得: （1）a 和 a’ 是证明对; 并且（2）a’ 是 u 的算数摁化。

这里，公式G的哥德尔数是什么？G本身是由 G’ 摁得到的，G’的哥德尔数是 u，所以由上面的定义，G的哥德尔数就是u的算数摁化。

所以，u的算数摁化是存在的，他就是G的哥德尔数，自然，公式G中的（2）是成立的。从字面意义上理解，公式G说得是现象（1）和现象（2）不能同时成立。但是现在现象（2）已经成立了，并且还告诉我们 a’ 具体是什么，那么不能成立的事就只可能是（1）了，所以我们可以把公式G重新措辞为：

没有一个数 a 能与 u 的算数摁化形成证明对。

换句话说就是：以 u 的算数摁化为哥德尔数的那个公式找不到一个可以证明其的序列。既然找不到这样一个序列，则以 u 的算数摁化为哥德尔数的那个公式不是系统中的定理。但是回过头来我们想想，“以 u 的算数摁化为哥德尔数的那个公式”是什么？那不就是公式G自己么！所以这句话相当于在说“G不是系统中的定理”，由于G就是它自己，所以这句话等价于：

我不是系统中的定理。

这样，我们就以一个能在系统中表示的公式G，描述了一个我们想要的那个等价的定理。之后的问题就简单了，G是系统中的定理么？如果是，则其是系统中的真理，可是实际上它在说啥？他说自己不是系统中的定理，这样就出现了矛盾。如果不是呢？这倒没有矛盾，但是G的非定理性是由其自己断定的，因而G讲述的是真理，但是G又不是系统的定理，于是我们就找到了一个真理，他能在系统中被表示，但它却不是系统中的定理，完备性的希望就此破灭了。

悲剧啊！

可见任意想到的可以让我们生活的更好的方法最后都被证明了是浮云，世界总是向着混乱不堪飞奔而去，渺小的人类在自然的力量面前是显的得多么的微不足道，就人活动的这点负熵顶屁用啊，QB快来拯救宇宙啊，这泥马越说越悲观了，不过事实也的确坑爹。虽然哥德尔不完备性定理完了，不过这文章应该还有后续，比如说哥德尔第二不完备性定理什么的，还有留给我们的残酷的现实是什么什么的，那么就下次再见吧。

上次提到了一个叫pq的形式系统，并且讨论了相容性是什么玩意，那么这次就来讲讲形式系统的另一个重要概念——完备性。

还记得我们给pq系统赋予的加法解释么？当时我说这个系统形式化了正整数的加法，那么笼统的说加法行不行？行，但是却不够准确，因为0=0+0这个简单的加法在pq系统里就没有办法表示，更别提非整数的加法了。像这样，如果在某个系统里不能表示我们想表示的所有结论，那么这个系统我们就称其为不完备的。就比如pq系统，其在加法的意义下是不完备的，但是在正整数加法的意义下却是完备的。可见完备与否取也决于我们想让一个形式系统有何等的能力。

那么回到最初的问题，数学家希尔伯特的想法是，弄出一个数学上的形式系统，这个形式系统足够强大，并且是相容的，是完备的，这样我们就可以机械的通过符号上的演算来得出各种定理与结论。由于它足够强大，所以我们可以从中获得非常多的定理。并且由于相容性的保证，我们得出的定理都是真的，又由于完备性的保证，所有我们想要得到的定理我们都可以得到。这大概就是所谓的让所有人的活在新闻联播的世界里的想法。不过希尔伯特提是提出来了，但是据坊间谣传说其本人相比于推导数学更喜欢帮人打官司，特别是遗产官司，这样可以在打完官司后大肆获利一笔。于是他本人并没在这上面花太多心思。不过这种想法听上去还是非常诱人，也吸引了不少人去研究，可惜此等美梦被哥德尔给打破了，哥德尔证明了：当有人活在新闻联播中的时候，必须有另外一群人活在今日说法之中，这就叫一国两制。一个足够强大的系统，不可能同时具有相容性和完备性。也就是说，一个系统如果足够强大，那么要么它能推出所有你想得到的结论，但是随之而来的其必定能推出另外一些你不想得到的——也就是错误的结论。（完备的但是是不相容的）要么其所有的结论都是正确的，但是其却必定不能推出你所有想要得到的所有结论。（相容的但却不是完备的）鱼和熊掌不能兼得。这就像电影社交网络的某个海报上写的那样——You Don’t Get To 500 Million Friends Without Making a Few Enemies.

在说哥德尔的证明之前先来问问大家一个问题吧：证明和计算是一回事么？对于我来说，之前一直认为这两件东西不是一回事，就像水和米饭虽然都是吃的但是不是一回事一样。不过哥德尔似乎不这么想，他认为计算和证明差不多，于是就有了哥德尔配数。那么举个例子来说明哥德尔配数是什么东西吧。首先我们来证明 4=1+3是pq系统中的定理：

1. – – q – p –               公理
2. – – – q – p – –           推理规则
3. – – – – q – p – – –   推理规则

这就是4=1+3在pq系统中的证明过程，如果这时我们用0代表q，00代表p，每个横杠用一个1来代表，那么整个证明过程可以写为：

1. 1101001                     公里
2. 111010011                 推理规则
3. 11110100111             推理规则

这个过程可以称之为数字化，而每个字母对应的数字就被称为哥德尔配数。要说明的是，配数的方法是不定的，只要保证一一对应就可以了，也就是说需要每一个数都能够被恢复成原始的字符串。此时我们就可以说证明是由一步步的算数运算得出的了（虽然这个运算的步骤和方法可能看上去莫名其妙）。这样我们就把证明转换为了数字上的计算。

那么在最后进入哥德尔不完备性定理之前，先揪出来一个之前说了无数遍却从没明确过的概念吧：一个足够复杂的系统。这是一个什么样的系统？这里的足够复杂是什么意思？详细的解释会比较麻烦，所以简单点来说就是：当这个系统可以形式化自然数时，这个系统就是一个足够复杂的系统。自然数是一个从小学起我们就开始接触的概念了，想必大家都认为这个很简单。但是即使是这样的系统，也不能做到两全，这听上去还真是可惜。除此之外，我们还要求这个系统里的所有能推出的结论都是一定能在有限步数中能推出的，这个应该好理解，毕竟我们需要这个系统给我们提供结论，如果他提供结论的过程有可能花费无限的时间（无论这个可能性有多低），那么其对我们而言就是没有意义的。另外虽然你可能觉得如果需要1亿年才能提供结论的话，虽说这是有限的，但是也没有意义。话虽如此，我们在这里并不限制推理所用的时间，100亿年也无妨，只要不是无限即可。

那么哥德尔最后就是证明了，下列四点不能同时成立：

1. 系统足够复杂
2. 系统相容
3. 系统完备
4. 系统的公设集递归

最后一点其实就是说的其推出结论只需要有限步骤，我们在这里用递归来表示有限步骤得结论这个性质。

下一篇就会切入哥德尔定理的证明，通过构造一个自指的命题，来证明希尔伯特的想法是不现实的，那么下次再说吧～

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

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不是一回事一样）

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

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