上次说到了形式系统大概是个什么样子，不过光用语言描述总是很抽象的，不好理解。那么就来举一个书上给出的例子来看看：
pq系统
- 字符集：p q -
- 公理：设 x 是包含且仅包含一个或多个字符'-'的字符串，则 x-qxp- 是这个系统中的串。
- 推理规则：设 x，y，z 的含义如上 x 所述，如果 xqypz 是这个系统中的一个串，则 x-qypz- 也是这个系统中的串。
这个系统就是这样了，字符集和公理应该很好理解，至于最后的推理规则，虽然不难，但是对有些人可能看上去有点陌生。这种形式的定义我们一般称之为递归定义，至于递归的含义，有一个关于它的经典笑话：
递归 [名词]：见递归。
这个笑话很形象的描述了递归的一个特点：自己定义自己。这听上去有点坑爹，自己定义自己不是说永远没完么？是的，所以递归的定义和这个有区别，自己定义自己没错，但是重要的一点是：定义用的是简单一些的版本，并且，起点是给定的。那么在这里，起点就是已经是系统中的，形如 xqypz 的串。那么这种串又是哪来的呢？向上看，这种串是由公理给出的。如果要再举一个例子的话那就是数学里著名的斐波那契数列，我们将这个数列的第 i 个数表示为 Fib(i) 则我们有：
- Fib(0) = 0
- Fib(1) = 1
- 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不是一回事一样）
所以说，在这里，提到可能世界，我们总有一个基准，“所有可能世界”不是指绝对意义上的所有可能世界，而是与基准世界相关联的所有可能世界。如果某一个可能世界里的规则与基准世界里的规则相矛盾，那么这个可能世界就不是我们想要的可能世界，他对于我们没有意义。所以回到主题，在内部一致性里，我倾向于把我们现实世界当作基准，那么如果存在一个在这基准之上的可能世界，在那个世界里系统中的所有定理的解释之间都不存在矛盾，则我们说这个系统是内部一致的。所以此时一个“桌子同时是方的和圆的”的可能世界就不是一个可以被接受的可能世界了，因为在基准世界（我们的世界）里，这是不可能的。
好了，那么关于形式系统的相容性大概就是这么多了，下次应该就是关于形式系统的另外一个重要性质了。下一次应该可以和哥德尔扯上关系了......吧—_卅......