“嗯！”
“哥德尔不完备定理。”米尔嘉回答道。
真
“嗯？嗯。打扫完卫生，他就一直在教室黑板上画着奇怪的图，一边画一边给我讲。他没有哥哥你讲得那么好，不过挺有意思的。”
“确实……总之，莱布尼茨当时想实现的是：即使不去思考含义也能把问题解决，即机械性地解题。”
“很好……下一道题。”
“那我们从头开始讲吧。”
“先别管这些。”米尔嘉说，“我们看逻辑公式。”
我看着黑板上的词语。公理、推理规则、证明、定理……？连支撑数学的最重要的概念 —— 证明 —— 都能被我们以微缩模型的形式建立起来吗？
从“示例是理解的试金石”这一理论出发，首先试着举几个公理的例子好了。因为要证明的逻辑公式是
就相当于写了以下逻辑公式。”
“啊！确实如此，很像很像。”泰朵拉点头。
是公理吗？
“我觉得成立……”我答道，“不对，这就考虑到真假了。光看形式的话 —— 我认为，不是公理。”
她说完就不吭声了。
“啊，真的……嗯，那 (3) 呢？”
“人家连一半都没听懂。他也说不知道这个定理的具体内容，我这才打算来问问哥哥你……”
“生成形式系统是‘用数学研究数学’的第一步。”
“按他说的，哥德尔不完备定理是一个很复杂的数学定理，这个定理证明了数学是不完备的。因此，数学这种由人类的头脑创造出的最严谨的学问，也是不完备的。好像是叫理性的界限。他说哥德尔不完备定理证明出了理性的界限……那家伙放了学都还在一个劲儿地说呢。”
“没错，泰朵拉。”
“……”泰朵拉无声地点了点头。
然后，米尔嘉似唱非唱地说道：
是逻辑公式吗？
活力少女进了教室。我把目光从米尔嘉身上移开。
德沃夏克 10 的《念故乡》从教室的扬声器里传了出来。
“形式上的数学？那是？”我忍不住插嘴道。
米尔嘉在黑板前来回踱步，继续“上课”。
“用数学……研究数学？”从刚刚开始，泰朵拉就一直在鹦鹉学舌般重复米尔嘉的话。不过……我自己也完全不知道她要讲什么了。
我们穿过校门，到了教学楼入口的换鞋处。入口是按年级划分的。
“那个，我之前跟那家伙吵了一架之后，慢慢熟悉了起来。刚才那个‘若……则……’就是他跟我讲的。他喜欢数学……可能是我们年级里书读得最多的人。”
“……”泰朵拉点了几下头。
Gödel's Incompleteness Theorems
泰朵拉忽然用两只手比了一个公主抱的手势。这授课内容还真是相当多呀。
假
(4)
“啊，米尔嘉学姐，你在想事情啊……对不起。”泰朵拉慌忙用双手遮住嘴。因为是高年级的教室，之前她都不好意思进来，不过最近也习惯了，都是大大方方地跑过来。
现在是二月，高三学生正处在高考季 4。整个学校都紧张兮兮的。他们都抱着这样的心态：熬过这个季节，迎来“春天”。这份紧张也传染给了我们这些高一、高二的学生。
“诀窍？”
“为什么？”
真
真
“就是说……或许之后，我们会把
“嗯，我懂了。”泰朵拉点头。
“那就是说，他要做一台会思考的机器？就像计算机。”
米尔嘉没说话，拿起书，给我看了看封面。
哦……所以米尔嘉才会每次都问“为什么”啊，原来是想要根据呀。泰朵拉沉思。不知为何，今天的泰朵拉很踏实，不再是平日里那个
“不过，形式是有限的。光靠公理模式不能生成新形式的逻辑公式。因此，我们定义一下推理规则吧。从形式上表示我们的逻辑性推理的，就是推理规则。”
假
“为什么？”
“对对，就是这个，就这个我不理解。”
“我们根据这两个规则来生成一个逻辑公式的序列。”米尔嘉继续说道，“这个逻辑公式的序列就是‘证明’。这样一来，位于‘证明’最末尾的逻辑公式
真
真
“那么……在这里，为了方便理解形式系统 H 中的逻辑公式，我们来定义一个符号‘
泰朵拉用指头戳了戳我，指了指米尔嘉扣在桌面上的书。书的封底上印着的标记跟学校图书室里的不一样。
“错了。”米尔嘉立即说道，“逻辑公式的定义中没有出现‘∧’这个符号。F3 里的是‘∨’而不是‘∧’。
“咱们高中好歹是重点高中，课程表里也包括如何备考这个课程。所以，我觉得只要好好上课，基本就没问题了。不过，光去上课并不一定就能学得好，这是肯定的。所以，还得掌握授课内容。”
“
“诶？真不明白么。比如求苹果价钱的题，‘设价钱为x日元’，列一个方程式。这就算向着‘式子的世界’启程了。接下来解方程式，求出x= 120，这就是求解。然后想着‘x表示价钱’，并回到‘含义的世界’。这样一来，就能得出答案是 120 日元。所以啊，所谓‘式子的世界’就像照出这个世界的镜子似的。照得好的话，就能用式子的变形来解决这世上的问题。”
“诶……没，没想过。”
唔……刚刚，米尔嘉说什么来着？
“这么晚了？学校的时间管理太严格了。”米尔嘉看向窗外。
“那个，虽然边走边说有点不好，不过我还是想请教一下学长如何‘备战高考’。我马上升高二了，有点担心高考……”
“那是 A 为假时，‘若 A，则 B’也为假的那些咯？那就是 (1) 啊。”
“为什么？”
“那个嘛……”
泰朵拉似乎对米尔嘉的话有了些许感触，只见她眼神中透露出十分的认真，咬着指甲。
“怎么了？这么严肃。”
“装作不知道的游戏？”米尔嘉反问道。
该从哪儿着手呢……
“……听懂是听懂了。”
“蔷薇的颜色、蔷薇的形状、蔷薇的香气 —— 拥有以上一切的花，才叫作蔷薇。那形式系统到底有没有数学的颜色、形状和香气呢？这个问题我们改天再想。”
“下面，我们来生成一个命题逻辑的形式系统玩儿。”
真
“嗯。‘严谨地思考’‘重视定义’‘重视语言’……”
“说理由就行了。因为 A 是变量，而我们在 F1 里定义了‘若x是变量，则x是逻辑公式’，所以 A 是逻辑公式。”米尔嘉说道。
“莱布尼茨？那是谁？”尤里回过头。
“学长你经常提到‘自己动脑来思考’呢。”
“你跟尤里正确解释了没？”她直勾勾地盯着我。
米尔嘉稍稍放慢了语速。
“哇啊！好酷！不过，不可能靠计算判断就能让人不再争论吧？全世界还有那么多争论。”
“嗯……不太明白。”
“学长！”
“……”泰朵拉默默地举起了手。
“假设有两个命题，即 A 跟 B。把 A 跟 B 用‘若……则……’连起 来，形成一个新的命题‘若 A，则 B’。用式子写出来，就是下面这样。”
“你俩放学以后一直都在讨论？”
“嗯……虽说还有不太明白的地方，不过我明白怎么靠真值表来判断哪个适合‘若……则……’了。哥哥，谢啦。”
我在新的一页上总结了“形式系统 H”的重点。
真
推理规则（形式系统 H 的定义 4）
▷推理规则 MP 根据x和
，可推出y。
注意，x、y表示任意的逻辑公式。
“在看什么书？”
真
“那个……尤里你有没有想过，什么样的真值表才适合‘若……则……’？”
“嗯……会焦虑吧。时间分配得不好，而且没办法把思考到一半的题放弃而往下做别的……所以，我碰到考试就非常紧张，心想要是碰到难题了该怎么办。我很怕这种状况……”
“这个推理规则有个特殊的名字，叫作 MP，即假言推理 9，这里 MP 是 Modus Ponens 的首字母。如果不习惯这里的‘根据x和
“嗯……因为
“看公理的定义就知道了。”我答道，“公理的定义有四个，P1～P4。不管把任何逻辑公式套到里面的x、y、z里，都不会变成
“当然，我们研究形式上的数学本身也要用到数学。”
“当然，这是在照得好的前提下。”
我又深深地叹了口气，把笔记本新翻开了一页。她拉过椅子坐在我身旁，戴上了那副树脂边框的眼镜。
“你看你看，逻辑里不是有个‘若 A，则 B’吗？这个，我不理解。”
“我……没好好看。”泰朵拉轻轻敲了一下自己的脑袋。
“我很庆幸一上高中就开始跟学长你聊数学。我数学成绩进步相当大。多亏了学长你，我才好像掌握了一点诀窍。”
“习惯问题。只要能降低自己的体温就行。”米尔嘉冲我们投来了一个温柔的笑容，然后一边挥动着手指，一边讲道，“当然，人们是不可能不思考含义的。而且，这种形式系统也不是胡乱生成出来的。其背后肯定有目的 —— 生成这种有意思的系统的目的。重要的是，不能由人来进行思考，而要从形式上、机械性地进行思考。”
“莱布尼茨啊，把‘思考’看作了‘计算’。他想要用机械性计算来实现逻辑性思考。”
我们刚要过马路，信号灯就变成了红色。在我俩等红绿灯的时候，我突然意识到一件事。
“不对不对！……真是的。是发现万有引力定律的那个物理学家。”
B
“原来是担心高考啊。”
“高考要怎么准备才好啊？我一点都不懂。高考是一场超大型的实力考试吧？跟学校定期举行的考试不一样，没有范围。嗯……中考那会儿，我已经很紧张了。我要往笔记本上一遍又一遍地抄相同的知识，这花掉我好多好多时间……而我那些朋友理解得快，记得也快，所以我想，是不是我没找对方法啊……”
“命题就是判定真假的数学性观点。既然有命题 A 跟命题 B 两个命题，那真假的组合就总共有四种。对于每一种组合，命题
“就是说……如果能组织好式子，就能用式子解开能用式子解开的问题？这不是理所当然的嘛！”
5英文写作 Propositional Logic，亦称命题演算，是由命题逻辑的重言式组成的系统。由两种方式形成：给出公理，根据确定的推理规则推导出一系列重言式，这称作公理演算；还有一种是借助自然演算，不给出公理，利用一系列推理规则推出定理。——译者注
清晨。上学路上，泰朵拉过来跟我打招呼。
“很遗憾，答错了。”米尔嘉说道，“要注意是否有括号。”
3摘自莱布尼茨的著作《莱布尼茨著作集 1：逻辑学》（尚无中文版）。
“学长，那个……有点事想跟你商量。”
真
看着两位美少女讨论数学，我禁不住心潮澎湃。
“我不理解第一行和第二行。第三行和第四行我理解。”
根据公理 P1：
“掌握……授课内容，是吗？”
“这问题很深奥。”
“现在我们在讨论形式系统。没有什么‘真’和‘假’，泰朵拉。”
“有时，如果人们在思考了含义的基础上进行论证，根据就会变得不明确。如果不去思考含义，只关注形式，根据就会变得明确。因为不管怎么说，人们只会使用明确定义过的事物。”米尔嘉回答道。
泰朵拉往摊开的笔记本上迅速写着笔记。
“这个……这次是‘∨’。是，这个是逻辑公式。”
根据公理 P3：
尤里站起身，开始打量我书架上的书。咦？她够到了之前够不到的那一层。个子长高了不少啊。
假
假
(2)
“那我们来画个真值表吧。”
“全都不明白……啊，不，我明白你们在说公理，也明白公理就是某种形式的逻辑公式。我不明白的是……怎么说呢，为什么要把这个弄成公理。”
问题 5-1（形式系统中的定理）
A
“啊，没错，我就是想说这个。”泰朵拉说。
“啊！米尔嘉学姐，这……是‘装作不知道的游戏’吗？”
“我们刚刚定义了逻辑公式和公理。公理已经以公理模式的形式给出。把逻辑公式代入 P1～P4 的x、y、z里，就能生成无数个公理。不过……”
“这个很像皮亚诺算术里的后继数啊……”我说。
“……没。”我慑于米尔嘉的目光，把我跟尤里的谈话告诉了她。
真
我叹了口气，面向尤里。
公理和推理规则……必须运用这两个工具来生成逻辑公式的序列，然后到达目的地
“接下来看这道题。”
“在！”
假
“哦哦。”泰朵拉点头。
“那……那，那放学后再见……”
真
我认为
“请讲。”米尔嘉像老师一样说道。
“来，看看我们了解到哪儿了。”米尔嘉说道。
我跟泰朵拉在教室的最前排坐了下来。
真
“嗯。自己动脑来思考是非常重要的。下课以后也要花时间来思考。然后，真真正正地去理解。当然，没必要总是先理解了全部内容，再往下学习。有时候也会留下一些疑问。但是，这个时候我不会‘装懂’。我会提醒自己‘这里我还不懂’。要一直思考，直到自己真正理解为止。越较真，学习就越有趣。”
“很热的，别靠过来嘛。来，(1)～(4) 里哪个适合‘若……则……’？”
4日本与中国不同，新学期一般在每年四月开始，并在来年的三月左右结束，而大学升学考试一般在二月左右。——编者注
“公理、证明、定理……这些数学概念我们都很熟悉了。下面我们要在形式系统中定义这些概念，然后以数学的微缩模型的形式来感受生成好的形式系统 H。”
“嗯，我听说过，不过不知道具体内容。”
“啊……了解。原来这样啊，拿定义当理由就行了啊。”
“啥？哥哥你在说什么啊……莫名其妙！”
“喔，你是这个意思啊。”
“总之，前提都不成立了，命题还是真的那种情况太奇怪了！”
“嗯，这点我深有同感。”
泰朵拉眨了两三下眼，咬着指甲，努力想着。
今天是周六。尤里一进到我的房间，就嚷嚷道。
米尔嘉静静地把书放下，闭上双眼，沉默了一会儿。她闭眼的时候，不知为何，我总是不由自主地沉默。或许我是在等待由米尔嘉内部而生的某样东西。或者是因为，她毫无防备闭上双眼的样子，非常地……
“我数学成绩上去了很多。英语我也很喜欢，应该没什么问题。但是我有时候会想，需要为了备战高考特别地下一番工夫么？虽然我朋友说，数学跟英语好，就没什么好怕的了……”
“不对，并不出现真假。”米尔嘉说道。
“对对。用现代说法来表示‘莱布尼茨之梦’，应该就是这样吧。他是这么说的。”
符号“
▷符号IMPLY 把
。
“‘解题时不思考含义’跟列式子时的思路很像。一思考含义就容易出错。你看，上了初中，从算术课变成数学课的时候，老师不也说过让你‘列式子’吗？”
“很好。”米尔嘉点头，“那这个呢？”
尤里装傻，我笑着表示：别开玩笑了啦！
尤里说着，又开始打量我的书架。我看着她的辫子，辫子像小马的尾巴般晃来晃去……不知为何，我心里不太舒服。
假
“诶？”她抬起头，大大的眼睛滴溜转了一圈。
米尔嘉掸了掸手上沾到的粉笔末。
8德国著名数学家，被称为“数学界的无冕之王”，是天才中的天才。——译者注
“尤里跟你说这个？”她抬起头，一脸严肃。
“我觉得……不是。我们是在用句法学生成形式系统，所以不会出现真假的概念。这个推理规则也必须看形式吧？而不是思考含义……”
“还好吧。”
“怎么这么复杂……是，
6英文写作 Formal System。形式系统是一个完全形式化了的公理系统。就其本身而言，只讲符号、公式和公式的变换。在一个公理系统内，使用特殊的人工语言，用一系列特定的符号表示逻辑概念或简单命题，用公式表示复合命题或真值形式，把证明变成符号与符号之间的变换。形式系统包括各种初始符号、形成规则、公理、变形规则。命题演算就是一个形式系统。——译者注
“那个啊，是一种练习，好让你学会怎么在读了题，列出式子以后进行机械性的计算，也就是让你学会不思考含义地往下计算。从具体例子来理解问题，这固然很重要，但还需要从某一阶段开始，把思维从‘含义的世界’转移到‘式子的世界’。说白了，就是列式子。只要去到‘式子的世界’，不用思考含义，也能让式子变形。我们可以用各种各样的方法来解方程式。最后让得出的结果从‘式子的世界’返回到‘含义的世界’，就能解开原来的问题了。”
“‘若……则……’和‘相同’应该不一样啊，呜！”尤里哼唧道。
假
真
“那个！”
是逻辑公式吗？
“诶？不思考含义怎么可能解题啊？哥哥你也说过要好好思考问题的含义啊！这……到底是什么意思？”
“这、这个嘛，1, 2, 3, 4……嗯，这个是逻辑公式。”泰朵拉用心数完括号说。
“在谈备战高考这个重大话题之前，先谈谈具体怕什么。”
“为了从形式上研究数学，我们在前面以字符串的形式定义了逻辑公式。接下来我们要从形式上来定义公理、证明、定理等。以希尔伯特 8为首的数学家们发现了用于形式系统的公理。也就是说，他们想出了能用来生成形式系统中的逻辑公式的集合。”
……然而，她在原地踟蹰，没有挪动脚步。
“早安，学长！”
“啊……确实，F3 里写的是‘若x和y都是逻辑公式，则
“现在，假设我们要把几个逻辑公式排成一列，来做一个叫证明的东西。规则 (1) 是，公理可以随时排列。规则 (2) 是，可以把能根据任意一个已排列好的逻辑公式推理出来的逻辑公式排列在那些已排列好的逻辑公式的后面。根据这两条规则排列而成的逻辑公式的序列就叫作证明。当然，这里所说的‘公理’是指形式系统 H 中的公理，‘推理’是指使用了形式系统 H 中的推理规则的推理。明白吗？”
“嗯，我觉得……我正式考试很弱。”
放学后，我们班的教室。
真
天色已经完全暗下来了。
“唔……差不多吧。”
“也是啊，我应该怎么解释呢……”我发愁。
“嗯，是。”
“泰朵拉，你可以先不用理解，它马上就会变具体了。”米尔嘉温柔地回应道，继续写着板书。
“怎么了？”
“我？”
B
信号灯变成了绿色，我跟泰朵拉又走了起来。
“外文书啊……”
真
“为什么？”米尔嘉问道。
虽然泰朵拉慌慌张张地冲了进来，米尔嘉却毫无反应，仍然闭着眼，还在思考。
“那我给你们留个作业。”米尔嘉看着我微笑道，“
“我不明白‘若……则……’！”
“正式考试很弱……是怎么个感觉？”我温柔地问道。
“你看嘛，你想想‘若……则……’的意思啊！”尤里抢了我的话，“在第一行和第二行里，A 是假的吧？也就是说‘若 A，则 B’这个前提不成立。前提都不成立了，可‘若 A，则 B’仍为真，不觉得很奇怪吗？”
泰朵拉一下子提高了嗓门，我也不由得大声应道。她用大大的眼睛认真地、直直地注视着我。
假
117 世纪德国哲学家、数学家，历史上少见的通才，被誉为“十七世纪的亚里士多德”。——译者注
预备铃响了。
“那不用‘
“那是数学家们先天地假设了公理为真，对吧？”
（那家伙？）
“你还是这么有活力啊，泰朵拉。”
“唔……嗯，这么说也行。”米尔嘉略表同意，“讨论形式系统时，我们要降低体温，去感受机器的心情。不能让含义牵着我们的鼻子走。举个例子，逻辑公式
“A 为什么是逻辑公式……这个，怎么说好呢？”
……只要是人，都能单凭计算来判断当下哪怕是最复杂的真理。今后，人们不会再争论已经掌握的事物，而会奔赴新的发现。3
比起学校里的题，书上写的题、村木老师出的题，还有跟米尔嘉讨论数学时出现的那些题更令我感到兴趣十足。
“莱布尼茨曾经用计算来理解逻辑。”我说。
“没错，这就跟‘用数学研究数学’连上了。”
A 是逻辑公式吗？
“那个，我……我想问一下，‘为真’和‘已被证明’是……不同的概念吗？”
“尤里你还真是喜欢条件跟逻辑啊。很少有人初二就能理解到这种程度。”我说。
通过“式子的世界”来解题
这标记是什么？藏书印？
“是吗？”米尔嘉一脸平静，“哪里不明白？”
“嗯……因 为 A 是逻辑公式，而 F2 里写着‘若x是逻辑公式，则
“不出现真假，也有公理……吗？”
我翻开笔记本。这是用来做‘我自己的数学’的专用笔记本，上面还有米尔嘉和泰朵拉写的不少东西。
“简单来说，语义学就是使用真假值的方法。把真值或假值分配给命题，研究命题的关系。不过我们下面要用的是句法学。不用真假值，而是通过关注逻辑公式的形式来往下研究。总之，就是不思考含义，只思考形式。”
“跟牛顿一个时期的，17 世纪的数学家。牛顿你知道吧？”
“这……嗯，我觉得是。”泰朵拉答道。
假
“那个，我想问一下……”泰朵拉举起手，“形式系统……这个概念太抽象了，我不知道该怎么理解才好……”
“我们设这个 F1 里写的变量为 A, B, C, ... 这样的大写英文字母。不过，因为只有 26 个英文字母，所以到 Z 以后我们就得像 A1, A2, A3, ... 这么写，这样才可以生成无数个变量。”
真
这个……要怎么形容才好呢？有点像解谜，又不同于单纯的解谜。给出的条件非常有限，但是又与解数学题很像。确实像是数学的微缩模型。
假
“喂，看不起人嘛？比如最上面那行，意思就是‘若 A 为假且 B 为假，则
“数学的……微缩模型？！”泰朵拉感到不可思议。
米尔嘉说着用手指向泰朵拉。
“在定义逻辑公式时，我们使用了逻辑公式本身。”米尔嘉说道，“这就是所谓的递归定义 7。”
“这问题提得好，泰朵拉。确实不同，虽说这个话题有点跑偏了。——一看公理的示例就会发现，公理越来越复杂，让人们很难理解。像
“理由啊……因为 F2 里写着‘若x是逻辑公式，则
“先不说这个。其实，我也跟你一样，不清楚怎么备战高考。现在就在重复着‘听讲 —— 复习 —— 看参考书’这个过程。虽说我也一直在留心，尝试自己动脑来认真思考。”
米尔嘉说完，注视着我们。
“嗯，知道了。”
关于形式系统 H 的总结
▷逻辑公式 F1 若x是变量，则x是逻辑公式。
▷逻辑公式 F2 若x是逻辑公式，则
▷逻辑公式 F3 若x和y都是逻辑公式，则
▷逻辑公式 F4 只有 F1~F3 规定的内容是逻辑公式。
▷符号 IMPLY 把
▷公理 P1
▷公理 P2
▷公理 P3
▷公理 P4
▷推理规则 MP 根据x和
“句法学研究的是形式系统。接下来我们要生成一个形式系统，暂且将其称为‘形式系统 H’吧。”
“没事儿……我身边都没有人会跟我说这些。老师没有这么说过，爸妈也没有这么说过。我，对我，对泰朵拉来说，学长你果然非常……重要。”
“嗯，没错。那你不理解哪一行呢？”
我放慢脚步，倾听泰朵拉说的话。
“可是啊，尤里，你好好看看表格。(1) 只在 A 跟 B 都为真时为真。所以，(1) 指的是‘A 且 B’。”
根据公理 P4：
“原来如此。那练习一下‘计时赛’，也就是在规定时间内解题如何？就像练习限时考试似的。”
我盯着这几条公理……嗯？这不是很简单吗？
逻辑公式（形式系统 H 的定义 1）
▷逻辑公式 F1 若x是变量，则x是逻辑公式。
▷逻辑公式 F2 若x是逻辑公式，则
▷逻辑公式 F3 若x和y都是逻辑公式，则
▷逻辑公式 F4 只有 F1~F3 规定的内容是逻辑公式。
“话虽这么说……”泰朵拉开了口，“可是现在我们只得出了‘
“你回去晚了，你妈不会担心么？”
“这样，我们就能从形式上表示‘证明’了。我们基于公理，进行推理，然后构成证明 —— 这是数学中重要的一环。在此我们要做的是把证明从形式上表示出来。形式系统 H 中的证明可以如下定义。”
“好久不见？……今天早上我们不是才刚见过么？”我说。
“可是，哥哥你已经听懂了吧？”
虽说是证明，却不能像平时做数学那样去证明。不能用反证法，也不能用数学归纳法。因为下面我要进行的证明，其形式必须是形式系统 H 中定义过的那种。因此我只能用下面这两个“工具”。
“如果你还没有明白，那么就算全世界的人都说‘明白了，很简单啊’，你仍然要鼓起勇气说‘不，我还不明白’。这一点很重要。就算别人再怎么明白，如果自己不明白，那也没有意义。要花时间来思考，思考到理解为止。这样得到的东西就一辈子都属于自己。谁也抢不走，认真学习，细心积累，会带给你自信。那种‘就算考试也不会焦虑’的自信。”
“话说，形式上的数学……难不成……”
“没错。理由呢？”
“话说……我感觉这个‘装作不知道的游戏’到这里就已经难得不能再难了。原来一边听一边还不能被含义牵着走是这么难啊。”
“这就是所有的了？”尤里探出身子看着表格。
“说的是呢……”
“好的。下一道题。”
根据公理 P2：
“学长！米尔嘉学姐！好久不见！”
“就是说，只排列‘公理’或者‘根据公理推理出的逻辑公式’？”泰朵拉一脸纠结地问道。
“(3) 是 A ＝ B。也就是说，A 跟 B 的真假相同时，(3) 为真。”
“诶？‘若 A，则 A’总为真……对吧？”泰朵拉回答道。
到学校了。
“也有省略的写法。不过，在句法学里，字符串……也就是字符的排列方法很重要，为了强调这一点，我们暂且把括号也明确地写出来吧。”
假
我们穿过住宅区的曲折小道，向着学校走去。
假
9复合判断的推理方法之一。从一个假言判断的前提出发，通过断定它的前件或后件(包括其否定)，而推出它的后件或前件（包括其否定）的演绎推理。例如：如果两个角是对顶角，那么这两个角相等。——译者注
“那家伙说‘思考意思以后，肯定会觉得奇怪’。可是他光说‘这样就对啦’，却不给我讲。”
“莱布尼茨之梦啊……嗯。”
“那么，思考时能不思考含义吗？”米尔嘉继续往下讲，“连不能描述含义的机器都能思考的事情是什么呢？机械性的思考、形式上的数学 —— 该怎么研究这种形式上的数学呢？”
真
“唔……”米尔嘉把手指贴在嘴唇上开始思考，“我们现在卡在含义和形式的夹缝中间。我们想从形式上研究数学，为此就要定义一个能从形式上表示数学中的观点的逻辑公式。然后，我们还想从形式上定义公理、证明、定理。在数学中，公理是证明的起点。在我们的形式系统中，公理 —— 也可以说成‘形式公理’—— 就是‘形式证明’的起点，即‘逻辑公式’。从‘形式公理’出发，通过‘形式证明’，就可以生成‘形式定理’。”
“不好意思，我再打断一下。”泰朵拉举起手，“我还卡在‘公理’这个词上。我记得……从 P1～P4 的形式来看的话，是不能构成
“既然你能理解第三行和第四行，那我们就先把它们放在一边。然后，我们把第一行和第二行的所有情况列出来，研究一下哪种情况才适合‘若……则……’。”
“不愧是哥哥喵！”尤里坏笑道。
“你说的‘真’是？”米尔嘉眼神一变。
用数学研究数学 —— 我细细品味着米尔嘉的这句话。
“我很开心你能这么说。”
持久不能成为衡量真假的标准。
虽然蜻蜓的一天、樟蚕的一夜，
在其一生中都只是一段短暂的时光，
但绝非没有意义。
——《来自大海的礼物》[6]
“因为我们才刚定义了‘逻辑公式’而已呀，泰朵拉。下面我们进入到‘公理’。”
根据逻辑公式
，可用推理规则 MP 推出
。
“哈哈……我还没怎么这么做过呢。”
泰朵拉重新看了一遍米尔嘉写的板书。
原来如此。刚刚，我们是在制作数学的微缩模型。讲皮亚诺算术那会儿，我们定义了自然数集
尤里“呜喵呜喵”地喊着，伸展着双臂。“呼 —— 啊，对了，哥哥，你知道哥德尔不完备定理吗？”
A
“它的意思是，一旦遇到
“你怎么想的？”
证明和定理（形式系统 H 的定义 5）
我们把以下逻辑公式的有限序列称为逻辑公式
注意，对于所有的
，下面 (1) 或 (2) 成立。
(1)
是公理。
(2) 存在小于k的自然数s,t，根据
和
可推出
此外，我们把存在“证明”的逻辑公式
“那放学后再见。”我说。
“我们刚刚定义了逻辑公式，下面来定义公理。在形式系统 H 里，公理指的是 P1～P4 中任一种形式的逻辑公式。”
真
虽然课上完了，班会也开完了，可米尔嘉还在看书。
“米尔嘉学姐……”泰朵拉带着哭腔说道，“你们在说什么，我一点儿都跟不上。”
“在此我们定义了形式系统 H 中的‘证明’和‘定理’。总体来说，证明就是逻辑公式的序列。不过，要想让逻辑公式的序列成为证明，那么排列顺序要遵循一定的规则。排在序列里的逻辑公式有两个条件：(1) 自己是逻辑公式；或者，(2) 自己前面一定存在能推理出自己的逻辑公式。你们明白我在说什么吗？”
“P1～P4 是公理的形式，也叫公理模式。只要把逻辑公式代入公理模式中的x、y、z里，什么都能成为公理。那这次换你来答。”
“啊，不好意思，我只顾着自说自话了。”
“当然，研究苹果掉下来的那个园艺家。”
“尤里你知道怎么看真值表吗？”
“莱布尼茨之梦……”我无意中小声说道。
“我们如下定义形式系统 H 中的逻辑公式。”
“数学，真的可以用形式系统来表示么？”
慌慌张张的小女生，给人一种谨慎认真的印象。
“放了学？”
“下一道题。”
“上课重要的是集中精神听讲。这点泰朵拉你应该基本上没什么问题。听老师讲的内容，然后原原本本地去理解。做笔记也很重要，不过先得好好听。一听讲，就会有疑问。不过，不能把老师的话抛到一边，自己想自己的。要先把在意的地方赶快记下来，课后再仔细讨论。上课期间要集中精神听讲，不能因为有疑问，就在上课期间一直想着，这样可能会听漏重要的知识点。这就糟糕了。学习是从认真听讲开始的。”
假
公理（形式系统 H 的定义 3）
▷公理 P1
▷公理 P2
▷公理 P3
▷公理 P4
注意，x,y,z表示任意的逻辑公式。
“嗯……这 个 Modus Ponens 指的 是，若‘x为真’且‘若x，则y为真’，则‘y为真’吗？”
“认真思考很重要，但速度也很重要。”
“理性的界限……这理解得不好。”米尔嘉评价道，“那你呢？”
我没说话，点了点头。泰朵拉深吸一口气，继续说道：
“尤里啊，你把话捋顺了再说。”
“嗯，是逻辑公式。”
“请问……‘不思考含义’的意义是什么呢？”
逻辑学的研究方法
语义学（Semantics） 使用真假值
句法学（Syntax） 不使用真假值
“啊，这样呀。‘若……则……’跟‘且’相同，有点奇怪喵……”
“那我出道题看一下你们是否理解了。”
我思考着米尔嘉留的作业。
“研究逻辑学的方法分为两种，语义学和句法学。”
“是吧？所以，除了 (4)，其他都不适合‘若……则……’。说起来，要拿什么放在‘若……则……’里，本来就是人为决定的事儿。”
假
“规则的含义……我完全没听懂。”泰朵拉说道。
假
“很好。”
学校的摸底考试就快到了，整个年级一起考。按理说我应该提前复习一下的，但现在却没有那个心情。我自己看课本，把后面的问题都提前解完了，所以上数学课就跟复习似的。高中难度的数学已经过完一遍了，课上的练习也基本都是满分。不管是课本还是问题集，都没什么难度。
“是喵？”
1019 世纪世界重要的作曲家之一，捷克民族乐派的主要代表人物，e 小调第九交响曲《自新大陆》享誉世界。——译者注
根据 P2 可知，
“接下来，我们按照下面这个顺序来逐一定义概念。”
“那个定理是怎么回事？”
2表示逻辑事件的输入和输出之间全部可能状态的表格，即列出命题公式真假值的表。通常以 1 表示真，以 0 表示假。——译者注
“顺便说一下，(2) 就是 B 本身。‘若 A，则 B’跟 A 没有关系，这很奇怪吧？”
“句法学是基于与‘证明’的关系来思考公理的。公理指的是能在证明时无条件地使用的逻辑公式。也可以说，公理就是‘即使没有证明，也可以视为定理’的逻辑公式。”
“学长，那个、那个……那什么，那个……学长，那个……”
“嗯……嗯！原来如此……哥哥你好厉害！”
“咦！话说，之前尤里跟我提过这个定理，是什么……证明了‘理性的界限’的定理？”
“怎么了，泰朵拉。”
假
“双仓图书馆。”米尔嘉睁开眼说道，“泰朵拉你也来啦。正好，我们来玩命题逻辑 5 的形式系统 6 吧。”
真
“什么啊？这么突然。”我抬起头，把视线从桌子上移开。
“……嗯。”
(3)
假
米尔嘉推了推眼镜，看着我。
“那下一道题。”米尔嘉不给留任何空档。
米尔嘉拿着白色粉笔，站在了黑板前。
“这也太顺利了吧？”尤里盘起胳膊。
“啊！嗯，说过说过。就算是那些能用心算回答的简单问题，老师也让我列式子，烦死了。还有些考试不列式子就会扣分。因为这样，我还曾经先写了答案再补式子呢，傻乎乎的。”
7也叫作归纳定义，是一种实质定义，指用递归的方式给一个概念下定义。——译者注
这里是我家。现在是夜晚，我一个人坐在桌前。
“稍微有点不同。”米尔嘉回答，“除了‘根据公理推理出的逻辑公式’，还可以把根据‘根据公理推理出的逻辑公式’推理出的逻辑公式也排列出来。也就是说，可以列出的逻辑公式包括‘公理’，或‘根据公理推理出的逻辑公式’，或根据‘根据公理推理出的逻辑公式’推理出的逻辑公式，等等。也就是列出能根据‘公理’通过有限次的连续推理得出的逻辑公式。”
“嗯，是公 理啊。”我答 道，“P1 里写着
“话说，我突然想到，泰朵拉，有没有什么东西是你很怕的？”
(1)
说到“语义学”时，她在黑板上写了个 Semantics；说到“句法学”时则写了个 Syntax。
“嗯……能。”泰朵拉走上前去，在黑板上写了下面这个逻辑公式。
