这天，兔子正在家里勤勤恳恳地算着“我爱你”系统的定理。这时，手机突然震动了起来。
兔子拿起手机一看，竟然是乌龟在找他。
“你把你手头的工作先放一放，我在我家的地洞里发现了一块石板，石板上都是神秘的符号。你赶快过来我们一起研究研究。”乌龟的语气听着很急切。
兔子舍不得放下手上的工作便回绝了乌龟。但他继续先前的工作的时候，那些还不知道是什么的神秘符号在他脑子里乱转。他思前想后，决定去找乌龟。
他来到乌龟的住址，发现乌龟的家不见了，原来房子所在的位置出现了一个大洞。
乌龟从洞里面探出脑袋，摆摆头示意兔子进去。
“你这怎么回事，你的房子怎么塌了？”兔子有点幸灾乐祸，谁让乌龟老捉弄他。
“没事儿，最近电视上不是流行盗墓嘛。我不敢去别处挖，就把家里挖塌了。”乌龟尴尬地笑了笑。“先别说这个，来看我在地洞里发现的石板。”
石板上的外星人符号系统
兔子看向石板，石板上的都是| 、、这三个符号。
“据我的推测，这些神秘的符号代表了大自然的某种规律。我觉得它们和外星人有关！”乌龟说，“我们就把石板上的系统叫外星人符号系统吧。”
虽然觉得很无厘头，兔子还是继续看石板。在石板的最上方有一串符号：
“这可能是这些符号代表的形式系统的公理，这个形式系统的公理可不像“我爱你”系统中只有“我爱”一个，只要符合这个形式的，都是它的公理。我们可以把它叫做公理模式。”乌龟在旁解释道。
兔子继续往下看，下方还有一串符号：
兔子一拍脑袋：“既然上面是公理，那下面的一定是推导规则了！把定理的最前面和最后面都添个**| **还是一个定理。”
乌龟点点头表示肯定，说：“让我们先找一下定理的规律。我随便写一串符号，你来判断它是不是定理。”
外星人符号系统的定理
乌龟在地上划出如下的符号串：
**| | | | | | | | | | **
“这一看就不是定理！”兔子有点看不起乌龟，“这个形式系统里的定理符号串里都只有一个****和一个****。”
“你别着急，”乌龟慢条斯理地说，“我就是想拿它做个例子，像它这样的形式都不对的符号串肯定不是定理。定理的形式应该是先一组竖线，中间圆形分隔开，再一组竖线，再三角形分隔开，最后还有一组竖线，对吧？”
“对，我就是这个意思。”兔子说。
“一个符号串要是定理，它首先得符合这种形式。我们把符合这种形式的符号串都叫做构型良好的符号串吧。”乌龟说。
“简单点，就叫良构符号串。”兔子对乌龟的啰嗦有些厌烦，好好一个东西都被他说复杂了。
自顶向下和自底向上的定理判断过程
“那好，那我们来试试看判断一个良构符号串到底是不是定理好了。”说着，乌龟又写下了一串符号：
兔子想了一想，说：“我觉得有两种方法可以判断它是不是定理。第一种是逆推过去，假设这个符号串是定理，那它一定是由上一个符号串推导过来的，我可以一步步逆推回去，直到它无法再回退了，这时，它要不是一个公理，要不就啥也不是。”
他先划去符号串最初的一个**| ，划去符号串最后的一个| ；再划去最初的一个| 和最后的一个| **。
“看吧，逆推回去的符号串不是一个公理，所以你那个符号串也不是定理。”兔子得意地向乌龟瞥了一眼。
乌龟不以为意，问他：“那还有一种方法呢？”
“还有一种看起来更笨一点。”兔子把第二种方法写在了地上：
1a. 将最为简单的公理（ | | | | ）丢进桶里。
1b. 对于桶里的每个公理应用推理规则，将推得的结果丢进桶里。
2a. 将第二简单的公理丢进桶里。
2b. 对桶里的每个符号串应用规则，并将结果都丢进桶里。
3a. 将第三简单的公理丢入桶里。
3b. 对桶里的每个符号串应用规则，并将结果都丢进桶里。
等等等等
“这个系统的没有缩短符号串的规则，桶里装的定理会越来越长，直到比你这个符号串长。如果它是定理，肯定会出现在已经生成的符号串中。”兔子解释一下这些步骤，““我爱你”系统倒是又增又减的，比这复杂多了。”
乌龟笑了，他对兔子说道：“你使用的第一种方法，可以叫做自顶向下的判定过程；你使用的第二种方法，从公理往上进行，可以叫做自底向上的判定过程。”
“不过，你不觉得这样太机械了吗，我们应该找一找系统外的判定过程。”乌龟提出了更高的要求。
系统外的判定过程
兔子随手画着定理的推导规则，突然灵感像闪电一样击中了他：“我知道了，是加法！”
“在公理模式中，第一个I的数量要等于后两个I的数量相加；而推导规则从满足加法标准的公理出发，只能产生满足加法标准的定理。推导规则把加法标准变成了定理的一个遗传特性！”兔子说。
“其实还可以这么想，”兔子的灵感源源不断，“这些符号串就是加法的算式！“IIIIIIIIIIII”就是“6=2+4”。”
“你从外星人符号系统的定理和加法中看到了同构。”乌龟对兔子的发现表示肯定。
形式系统的同构
看到兔子对同构这个词表示不解，乌龟解释道：“两个复杂结构间的每个部分可以建立一一对应的关系，也就是映射，且这些部分在各自的结构中起到相似的作用。我拿现在这个系统的定理和加法举个例子吧。”
乌龟在地上写下：
⇔=
⇔+
I⇔1
II⇔2
III⇔3
等等
“这些就是两个结构间符号和符号一一对应的关系。这种元素间“较低层次”的对应关系有一个名称：解释。”乌龟继续说，“如果这是一种有意义的解释，我们会发现两个系统的真陈述与定理之间也存在着对应的关系。”
“比如，外星人符号系统的定理IIIIIIIIIIII对应着加法的真陈述：“6=2+4”。事实上，如果你要建立如下的映射关系，”乌龟又写了另一套映射关系：
⇔你
⇔我
I⇔他
“你会发现定理的解释看起来并不比随便乱写的符号串的更好一点。你可以选择这样解释，只不过这样的解释是无意义的。”乌龟说。
“当语言学家要破译密码或者解读古代文字时，他们会尝试各种各样的解释，直到有一种解释可以在更高的层次上和我们的语言产生对应，他们就找到了有意义的解释。”乌龟说。
“比如解释英文中的“is”，人们可以把它翻译成“有”，“能”等等字，直到把它翻译成“是”的时候，英语的句子才能和汉语的句子对上号。”乌龟说。
兔子觉得脑袋中隐约能感受到同构的意思，但仔细思考下又觉得这个概念很模糊。
他有些迷惑：“如果这个系统的定理和加法同构的话，IIIIIIIIII II就应该是一条定理。但它并不是一条定理，它不是良构符号串啊。”
形式系统的论域
“是的，我建立的这个形式系统还不够完备。”乌龟说。
“啊，这是你弄的啊，白费我这么多时间研究它了。”兔子向乌龟抱怨道。
乌龟第一次认真地看向兔子：“你愿意听听我为什么要建这么一个形式系统吗？”
“好的。”兔子点点头，他倒要看看乌龟的葫芦里到底卖的什么药。
“其实数学家甚至是所有人的工作，都是在尝试用某个形式系统中的所有定理反映某个领域，也就是系统的论域，中的所有真理。如果这个尝试成功了，我们就可以说这个形式系统和它的论域完全同构了。”
“能解释一下论域吗？”兔子问。
“打个比方吧，当我们讨论iPhone和小米的时候，我们的论域就是所有手机品牌。”乌龟说。
“我们用来表示加法的阿拉伯数字和＋号，其实只是形式系统中的符号而已；我们使用的语言，也可以说是人们用以与世界同构的形式系统。”乌龟说。
“我们会发现，在我们百分之一百了解形式系统的论域之前，无法确定我们构造的形式系统中的每一条定理的解释是否都是真理。”乌龟说。
看兔子听的云里雾里的，乌龟又举了一个例子：
“比如“量子”这个词，几百年前的人们是无法理解它的意思的，即使他们能分别看懂这两个字。但无论“量子”、“Quantum”这些词能否被人解读，它们表示的事物是一直存在于世界上的。”
形式系统的多重解释
“你们兔子一族里面表现团结的力量时不是经常会用“1+1>2”吗。从最初这个形式系统的论域来看，这种解释肯定是不太合适的。”乌龟说。
“但一个形式系统只能有一种解释吗？”乌龟反问道。
乌龟又问：“我这个外星人符号系统其实还有一种有意义的解释，你发现了吗？”
“是的，我也发现了另一种解释。”兔子说，“而且我发现，不仅一个形式系统可以有多种有意义的解释，一个领域也可以由多个形式系统解释。比如数学家和哲学家分别用独特的形式系统尝试着与世界同构。”
“你说的不错。看你也累了，让我们总结一下今天的收获吧。”乌龟说。
“我们从这个外星人符号系统说到了它和加法的同构，又通过两个层次区别了形式系统有意义的解释和无意义的解释，然后讨论了形式系统的论域，最后，我们聊到了形式系统的多重解释。”
“大概就是这样了，”兔子确实有些累了，“至于这个外星人符号系统的另一种有意义的解释，就留给那些在看我们故事的人当做一个谜题好了。”
