不管是什么样的真理，
只要一经发现，就很容易被人理解。
重点在于，要去发现真理。
——伽利略·伽利莱
10.1 双仓图书馆
10.1.1 入口
“唉 —— 累死了啦。”
“是这里吗？”
“嗯。”
现在正值春假，我和尤里、泰朵拉三个人来到了双仓图书馆。双仓图书馆是建在小山坡上的一座三层小楼，有一个圆圆的屋顶。我们从车站一路爬上山，迎面就看见了入口处的图书馆标志。
图书馆里面很开阔，像酒店的大堂一样。抬头望去，每一层都像回廊一样环绕着整个室内中庭。透过玻璃可以看见一排排的书架。柔软的沙发摆放在各处，坐在上面的人们各自看着自己想看的书。四处漂浮着一种图书馆特有的气息 —— 由很多很多图书散发出来的气息。
“我们去哪儿好？”泰朵拉四下张望。
“米尔嘉说有人会来告诉我们……”我说道。
这时，前台一位英俊的男士告诉了我们房间的位置。
“说是一楼的叫‘氯’的房间。”我在走廊里一边走着，一边和她们说话。
“泰朵拉，刚才那个人真是帅得要命啊……”尤里说道。
“那个人应该是图书管理员吧？”泰朵拉说道。
“他可没戴结婚戒指呀！”
几句话的工夫，居然连戒指都注意到了……啊，到了。
我推开了写着 Chlorine 的门。
10.1.2 氯
“你们来啦。”米尔嘉说道。
“我说米尔嘉，这里是哪儿啊？”我坐在椅子上，四下看了看整个房间。
房间中央有一张椭圆形的桌子，桌子周围摆放着带靠背的椅子。四面墙中有一面整个是一大块白板，这让房间看起来像个多功能会议室。房间的角落里有内线电话跟书架。从宽敞的窗户望出去，可以看到一片绿色，像是个庭园。
“这里？是图书馆啊。”米尔嘉说道。
“我记得叫……双仓图书馆吧？”泰朵拉坐下说道。
“对。双仓博士的私立图书馆。”米尔嘉说道，“这里有很多数理方面的藏书。也有很多房间像这间一样，里面有用来开会或讨论的设备。据说这里偶尔也会召开小型国际会议。虽说我只参加过几次数学研究会，不过我觉得这里确实很方便。”
诶？米尔嘉还参加过那种会议呐。
“米尔嘉大人，今天讲什么？”尤里问道。
“我们要花上一整天，一起‘用数学研究数学’。”
“用数学研究数学？”尤里不解。
“就是一起思考现代逻辑的出发点 —— 哥德尔不完备定理。要是我们去高中图书室，会受很多限制，而且尤里你也去不了。”
“好高兴喵！啊，对了对了，米尔嘉大人，请收下这个！”
尤里递出一个小纸包，里面包着点心。
“喔……那这个就拿来配下午茶吧。”
米尔嘉面向白板，拿出一支马克笔。
“因为会讲很多，所以我们先来列个大纲。”
◎ ◎ ◎
首先，我要讲的是希尔伯特计划。数学家希尔伯特想要给数学一个牢固的理论基础，因而提出了希尔伯特计划。
其次，我要整体讲一下哥德尔不完备定理。哥德尔的不完备定理表明了希尔伯特计划用当时的方针是无法实现的。在证明哥德尔不完备定理之前，我要讲一下这个定理本身。
然后，就是仔细研究哥德尔不完备定理的证明。这里会讲很久，所以中途要吃个午饭，还有午后茶点。
最后是思考不完备定理的意义。关于不完备定理的负面评价很多，例如它破坏了希尔伯特计划呀，表明了数学的界限啊，等等。然而，不完备定理是创造了现代逻辑基础的定理。我们应该关注的是不完备定理具有的建设性意义。
那么，我们就进入正题吧。
10.2 希尔伯特计划
10.2.1 希尔伯特
戴维·希尔伯特是一位活跃在 19 世纪至 20 世纪初的数学领军人物。他为了给数学建立一个坚实牢固的基础而提出了希尔伯特计划。这个计划由以下三个阶段构成。
导入形式系统
- 以“形式系统”来表示数学。
证明相容性
- 证明用于表示数学的形式系统“不存在矛盾”。
证明完备性
- 证明用于表示数学的形式系统是“完备的”。
我来依次说明这三个阶段。
导入形式系统 —— 希尔伯特想要用形式系统来表示数学。数学是一门非常大的学问，涉及各种各样的领域。不弄清楚“数学是什么”，就不能建立起牢固的基础。因此希尔伯特决定把数学视为形式系统。于是，他把逻辑公式定义为符号的序列，并在逻辑公式中定义了公理这一概念。他还定义了推理规则，以根据逻辑公式推导出其他的逻辑公式。希尔伯特把那些源于公理，并通过推理规则接二连三地得到的逻辑公式叫作定理，把那些由被叫作定理的逻辑公式构成的序列叫作形式证明。如果形式系统中的形式证明在某种意义上表示了数学中的证明，那么就可以说，该形式系统确实摸清了数学的一个方面。如果数学能用形式系统来表示，那么我们只要研究该形式系统就可以了。
证明相容性——希尔伯特认为，既然建立了用于表示数学的形式系统，该形式系统就需要具备相容性。这里所说的“相容性”指的是，对于该形式系统的任意逻辑公式 A 都存在以下性质：无法从形式上证明 A 和 两者都成立。话说回来，在存在矛盾的形式系统中，所有的逻辑公式都能从形式上证明，所以这一条性质没什么意义。如果能够证明用于表示数学的形式系统具备相容性，那么就能断定我们无法从形式上证明 A 和 两者都成立。
即使证明了相容性，但是一旦有人置疑该证明的有效性，那也不好办。于是，希尔伯特想到用一个排除了含义的形式系统来明确证明该形式系统自身不存在矛盾。
证明完备性 —— 希尔伯特认为，要想给数学建立一个牢固的基础，光满足相容性还不够。用于表示数学的形式系统不仅要具备相容性，还必须具备完备性。这里所说的“完备性”，指的是对于该形式系统的任意语句 A，都存在以下性质：能从形式上证明 A 和 至少有一方成立。如果能够证明用于表示数学的形式系统的完备性，那么就能断定我们能从形式上证明 A 和 至少有一方成立。
希尔伯特想通过“导入形式系统”来表示数学，再通过“证明相容性”来表示无法从形式上证明 A 和 两者都成立，然后通过“证明完备性”来表示能从形式上证明 A 和 至少有一方成立。可以说，他想向我们展示的就是“不存在形式证明的光芒照射不到的黑暗角落”。
这就是通过导入形式系统、证明相容性、证明完备性给数学建立牢固基础的过程。
那么，你们理解希尔伯特计划了吗？
希尔伯特计划
导入形式系统
以“形式系统”来表示数学。
即用形式上的符号的序列来表示数学。
证明相容性
证明用于表示数学的形式系统“不存在矛盾”。
即证明对于任意逻辑公式A，都无法从形式上证明 A 和 两者都成立。
证明完备性
证明用于表示数学的形式系统是“完备的”。
即证明对于任意语句 A，都能从形式上证明 A 和 至少有一方成立。
10.2.2 猜谜
“米尔嘉大人！”尤里说道，“您刚刚提到的‘形式证明’跟‘证明’这两个词……”
“嗯？我吩咐你哥哥说‘让尤里好好预习’了啊。”米尔嘉说着看向我。
“前一段，我不是跟你详细说过吗？尤里……”我说道。
“你只讲了形式证明……”尤里支支吾吾道。
“那么，我们来简单复习一下。”米尔嘉说道，“在形式系统中，我们把‘逻辑公式’定义为‘符号的序列’，并从逻辑公式中定义一个叫作‘公理’的概念，然后再定义一个根据逻辑公式推导逻辑公式的‘推理规则’。”
她用食指比划着圈圈，继续往下讲。
“‘形式证明’指的是由逻辑公式构成的一种有限序列 a1, a2, a3, ... , an，它要满足以下条件。
- a1 是公理。
- a2 是公理，或通过使用推理规则能够根据 a1 推导出 a2。
- a3 是公理，或通过使用推理规则能够根据 a1 或 a2（或者 a1 和 a2）推导出 a3。
- ……
- an 是公理，或通过使用推理规则能够根据之前的任意一个逻辑公式推导出 an。
此时，我们把刚刚这个由逻辑公式构成的序列 a1, a2, a3, ... , an 叫作‘形式证明’，序列末尾的逻辑公式 an 叫作‘定理’。因此‘形式证明’只不过是形式系统中的‘由逻辑公式构成的序列’之一，说的是形式系统之内的事儿，也可以说是属于‘形式的世界’的概念。”
我们大家都点了点头。
“而‘非形式证明’是所谓的数学中的证明，说的是形式系统之外的事儿，也可以说是属于‘含义的世界’的概念。偶尔人们会把形式证明简称为证明，这就会引起麻烦。那么……尤里！”
“在！”尤里“唰”地一下子站了起来。
“我出个谜题来考考你理解了没。——在形式系统中，能把公理看成是定理吗？”
“……唔，我不明白。”
“那么，泰朵拉。”米尔嘉指着泰朵拉。
“我认为……能。”泰朵拉回答道，“定理指的是在形式证明的末尾出现的逻辑公式。例如，假设 a 是公理，然后思考仅由这一个公理构成的逻辑公式的序列 —— 这符合形式证明的条件。出现在该序列的末尾的逻辑公式 —— 虽说它既是第一个也是最后一个 —— 是 a 本身。因此，a 就是定理。所以，任何公理都能说是定理。”
“很好。”米尔嘉说道。
“唔……这样啊。”尤里嘀咕道。
“下一道题。”米尔嘉紧接着往下讲，“假设在完备的形式系统 X 中，语句 a 不是定理。现在，我们往形式系统 X 中追加一个语句 a 作为公理，生成了一个新的形式系统 Y。此时，形式系统 Y 存在矛盾。为什么？”
……无人应答。
“语句……是什么来着？”泰朵拉问道。
“不含自由变量的逻辑公式。”米尔嘉马上回答道。
接着大家又陷入了沉默。
“根据定义来思考吧。‘形式系统是完备的’指的是什么？”米尔嘉问道。
“对于任意语句 A，都能从形式上证明 A 和 至少有一方成立。”我答道。
“‘语句 a 不是定理’指的是？”米尔嘉又问道。
“就是说无法从形式上证明语句 a 成立。”泰朵拉答道。
“‘形式系统存在矛盾’指的是？”
“能从形式上证明某个逻辑公式 A 和 两者都成立。”尤里答道。
“那么，提示已经齐了。形式系统 Y 存在矛盾的原因是？”
回答米尔嘉的仍旧是沉默。
我思考着，不能从形式上证明语句 a，也就是说……
“我明白了！”尤里大喊道。栗色的头发一瞬间闪耀着金色的光泽。
“喔……那么，尤里你说。”米尔嘉指向尤里。
“因为 X 是完备的，所以应该能从形式上证明 a 和 中的一方成立。”尤里迅速说道，“因为 a 不是定理，所以不能从形式上证明成立。因此， 应该能从形式上证明成立。但是，Y 已经把 a 归为公理了。这样一来，就能从形式上证明 a 和 两者在 Y 里都成立！所以，形式系统 Y 就存在矛盾了……”
说到这里，尤里观察了一下米尔嘉的脸色。
“很好。”米尔嘉说道。
每当梳理逻辑时，尤里都会爆发出惊人的速度……
“就像这样。”米尔嘉用双手做了一个捧住大球的手势，“对完备的形式系统来说，哪怕往公理里加一个无法从形式上证明的语句，都会出现矛盾。因此比起‘完备’这个词，用‘完整’更适合 —— 需要的东西都齐全了的意思。”
“完整……”泰朵拉喃喃道。
“我再出一道题。”米尔嘉说道，“如果形式系统存在矛盾，那么就能从形式上证明该形式系统的所有逻辑公式都成立。现在我们不去证明这个说法，但是一旦认可了这种说法，那么就会发现存在矛盾的形式系统是完备的。为什么？”
“啊，的确是这么回事。”我说道。
“诶？！明明有矛盾还是完备的？”泰朵拉不解。
“泰朵拉，现在你被矛盾和完备这两个词的字面含义带跑了。”我说道，“如果形式系统存在矛盾，那么就能从形式上证明该形式系统的所有逻辑公式都成立 —— 米尔嘉刚刚是这么说的，对吧？那么，由于语句是一种逻辑公式，所以所有语句都能从形式上来证明。这样一来，该形式系统就是完备的了。因为对完备的形式系统而言，不管选择何种语句 A，我们都能从形式上证明 A 和 至少有一方成立 —— 这是刚刚已经定义了的，对吧？在矛盾的形式系统中，我们能从形式上证明 A 和 两者都成立。如果‘能从形式上证明 A 和 两者都成立’，那么就能说‘能从形式上证明 A 和 至少有一方成立’，因此存在矛盾的形式系统是完备的。”
米尔嘉点点头，表示同意我的话，然后说道：
“很好。如果被字面意思带跑了，那么一听到‘存在矛盾的形式系统是完备的’这句话就会觉得很不可思议。然而，从数学上的定义来思考，这一切就理所当然了。”
“存在矛盾就是完备的么……”泰朵拉嘀咕道。
“我先声明一下吧。”米尔嘉说道，“我们不能根据‘存在矛盾就是完备的’引申出哲学层面的意义或是人生警句。不，引申不引申是你个人的自由。但是，从数学的角度来说，这种引申是没有意义的 —— 那么，我们下面就谈谈哥德尔吧。”
10.3 哥德尔不完备定理
10.3.1 哥德尔
库尔特·哥德尔提出的不完备定理的证明发表于 1931 年，那时他 25 岁。论文的题目是《论〈数学原理〉及其相关系统的形式不可判定命题（I）》1。
1原论文英文题为 On formally undecidable propositions of Principia Mathematicaand related systems（I）。论文题目中的《数学原理》一书原书名为 Principia Mathematica，指的是怀德海和罗素所著的书。——译者注
我来读一下摘译的论文开头部分吧。
一直以来，数学都在朝着追求严谨性的方向发展。其结果众所周知，数学的大部分内容被形式化，甚至可以用几个机械性的规则来证明。
最全面的形式系统分为两个方面，一方面是数学原理（Principia Mathematica）系统，另一方面是策梅洛 - 弗兰克尔（Zermelo-Fraenkel）集合论公理系统。
这两个系统都很全面。时至今日，我们在数学上使用的所有的证明方法都能够用这些系统来形式化。也就是说，今天我们在数学上使用的所有证明方法都能够还原成形式系统中少数的公理和推理规则。因此我们往往会认为：在形式系统中能够用形式表现的所有数学性问题，都能够用该系统中的公理和推理规则来判定。
然而这是不正确的，原因如下所示。
哥德尔在这篇论文中证明了数条定理，其中就包括如今被人们称为“不完备定理”的两条定理，这两条定理分别叫作第一不完备定理和第二不完备定理。
哥德尔第一不完备定理
在满足某个条件的形式系统中，存在满足以下两个条件的语句 A。
该形式系统中不存在 A 的形式证明。
该形式系统中不存在 的形式证明。
哥德尔第二不完备定理
在满足某个条件的形式系统中，不存在“表示该形式系统自身相容性的语句”的形式证明。
哥德尔的两条定理对希尔伯特计划造成了很大的打击。这是因为这两条定理证明了对于满足某个条件的形式系统而言，我们既不能从形式上证明其“完备性”，也不能从形式上证明其“自身的相容性”。而且，这里的“某个条件”也非常地自然。
10.3.2 讨论
“米尔嘉学姐，我提个问题。”泰朵拉举起了手，“也就是说，因为‘无法证明数学的相容性’，所以从哥德尔的第二不完备定理可以得出‘数学全都蕴含着矛盾’喽？”
“错。刚刚你提出的‘无法证明数学的相容性’，还有‘数学全都蕴含着矛盾’这两个看法是非常模糊的。我们重新回顾一下第二不完备定理。”
哥德尔第二不完备定理
在满足某个条件的形式系统中，不存在“表示该形式系统自身相容性的语句”的形式证明。
“哥德尔第二不完备定理不是关于‘数学本身’的定理，充其量只是一个关于‘满足某个条件的形式系统’的定理。”
“看来不能随随便便就把‘数学’和‘形式系统’划等号啊。”
“而且，”米尔嘉继续说道，“无法从形式上证明的是‘自身的相容性’。也就是说，满足某个条件的形式系统无法从形式上证明该系统本身的相容性。但是，在某些情况下还是能够从形式上证明其他系统的相容性的。”
“虽然不能够说‘我具备相容性’，但是可以说‘你具备相容性’……是这样吗？”泰朵拉问道。
“这说得也有点笼统了，不过，也可以那么说。就算第二不完备定理存在，也不会妨碍到实际的数学。如果想证明某个系统的相容性，就要使用更强的系统。实际上，数学家们也一直在研究如何证明各种各样的系统的相容性。如果省略了数学方面的条件，那么哥德尔不完备定理听上去就比较过激了。另外，如果忽视‘不完备’这个词在数学上的含义，而被其字面含义迷惑，那么推导出的结论就有可能超出数学的范畴。”
“米尔嘉大人，”尤里说道，“我记得有本书里说‘不完备定理从数学角度证明了理性的界限’……”
“我说尤里，”米尔嘉的眼神变温柔了，“哥德尔不完备定理是数学定理，数学定理不会去证明什么理性的界限。”
“是吗？”
“比如，方程式 x2 = -1 不存在实数解。这表示的并不是理性的界限，由此明确的只是方程式具有的性质。哥德尔不完备定理也是如此，它只是明确了满足某个条件的形式系统的性质。当然，不完备定理给数学带来的影响的确很大。但是它带来的并不是让数学萎缩的消极影响，而是创造崭新的数学的积极影响。”
“喔……”
“话说回来，‘理性的界限’这个说法是哥德尔六十岁大寿时奥本海默 2 致的祝辞，并不是带有数学色彩的主张 3。但是不知道从什么时候起，这个说法就被人们单独拿出来用了。”
220 世纪的物理学家，美国籍犹太人，是曼哈顿计划的主要领导者之一。——译者注
3出自《哥德尔与 20 世纪的逻辑学 3》（原书名为『ゲーデルと 20 世紀の論理学 3』，尚无中文版）一书，详见参考文献 [30]。
“这么说来，不完备定理的‘某个条件’是什么来着？”我问道。
“相容，蕴含皮亚诺算术公理，还要是递归的。”米尔嘉说道，“换言之，就是相容、能研究自然数、能够机械性地判断逻辑公式的序列是正确的形式证明。虽然哥德尔的论文中使用了比‘相容性’更强的‘ω 相容性’这一条件，但是罗赛尔 4 证明了可以弱化这一条件，只取相容性。”
420 世纪的美国数学家、逻辑学家。——译者注
10.3.3 证明的概要
“来整体看一下哥德尔证明的大纲吧。这里把证明分为五个阶段，分别把它们叫作春天、夏天、秋天、冬天，还有新春。”
春天 —— 形式系统 P
- 定义形式系统 P 的基本符号、公理、推理规则。
夏天 —— 哥德尔数
- 把数分配给形式系统 P 的基本符号和序列。
秋天 —— 原始递归性
- 定义原始递归谓词 5，介绍表现定理（representation theorem）。
冬天 —— 探索可证明性的漫漫长路
- 定义算术谓词乃至可证明性逻辑谓词。
新春 —— 无法判定的命题
- 构成 A 和 都无法证明的命题，也就是不可判定命题。
5原始递归谓词（Primitive Recursive Predicate）是一类数论谓词。若数论谓词 P 的特征函数是一个原始递归函数，则称 P 为原始递归谓词。——译者注
10.4 春天——形式系统 P
10.4.1 基本符号
在“春天”阶段，我们要构建形式系统 P。P 是往数学原理系统中追加了皮亚诺公理和若干条公理后得到的产物。在这个形式系统 P 中，我们可以描述加法运算、乘法运算、幂运算、大小关系，等等。
我们接下来会证明该形式系统 P 中存在无法判定的语句，不过该形式系统 P 只不过是满足不完备定理成立这一条件的无数系统中的一个而已 ——这一点是毋庸置疑的。
下面我们把数记作 0, 1, 2, .. .，也就是不小于 0 的整数。
首先来定义基本符号。基本符号包括常量和变量。虽然我们不用考虑其含义，但是为了理解起来方便，还是给符号加上一点我们想要的含义吧。
定义常量。
▷常量-1 0 （零）是常量。
▷常量-2 （后继数）是常量。
▷常量-3 （非）是常量。
▷常量-4 （逻辑或）是常量。
▷常量-5 （任意的）是常量。
▷常量-6 ( （开括号）是常量。
▷常量-7 ) （闭括号）是常量。
定义变量。变量的类型包括 1, 2, 3, ...。
▷第 1 型变量 x1, y1, z1, ... 是用于数的变量。
我们将其称为第 1 型变量。
▷第 2 型变量 x2, y2, z2, ... 是用于数的集合的变量。
我们将其称为第 2 型变量。
▷第 3 型变量 x3, y3, z3, ... 是用于数的集合的集合的变量。
我们将其称为第 3 型变量。
像上面这样，一直定义到第 n 型变量。英文字母只有 26 个，所以这里我们假设可以根据需要使用可数的变量。
10.4.2 数项和符号
定义数项。数项用于在形式系统 P 中表示数。
- 用数项 表示数 0
- 用数项 表示数 1
- 用数项 表示数 2
- 用数项 表示数 3
- ……
- 用数项 表示数 n
▷数项 我们把 称作数项。
泰朵拉：“ 连成一串，感觉很像音乐符号。”
我：“这里的 跟皮亚诺公理中出现的撇‘'’的作用相同。”
定义符号。
▷第 1 型符号 我们把 或是 称为第 1 型符号，此处设 x 是第 1 型变量。
泰朵拉：“呃……我不太明白。”
米尔嘉：“具体来说，第 1 型符号指的就是 跟 这样的。”
▷第 2 型符号 我们把第 2 型变量称为第 2 型符号。
▷第 3 型符号 我们把第 3 型变量称为第 3 型符号。
像上面这样，一直定义到第 n 型符号。
10.4.3 逻辑公式
下面来定义基本逻辑公式。
▷基本逻辑公式 我们把呈 a(b) 这种形式的符号序列称为基本逻辑公式。
注意，这里设 a 是第 n + 1 型符号，b 是第 n 型符号。
米尔嘉：“例如像 x2(0)、 和 z3(x2) 这样的就是基本逻辑公式。”
我：“这……这是集合（元素）的形式么？”
米尔嘉：“算是吧。”
泰朵拉：“我们想让 x2(x1) 有 这个含义？”
米尔嘉：“对。不过类型已经定好了，比如‘x1 是数’‘x2 是其集合’这种。”
定义逻辑公式。
▷逻辑公式-1 基本逻辑公式是逻辑公式。
▷逻辑公式-2 若 a 是逻辑公式，则 也是逻辑公式。
▷逻辑公式-3 若 a 和 b 是逻辑公式，则 也是逻辑公式。
▷逻辑公式-4 若 a 是逻辑公式且 x 为变量，则 也是逻辑公式。
▷逻辑公式-5 只有满足以上条件的才是逻辑公式。
泰朵拉：“啊，我明白了。我们定义的是形式系统的逻辑公式呀。”
定义省略形式。
▷省略形式-1 我们将 定义为 。
▷省略形式-2 我们将 定义为 。
▷省略形式-3 我们将 定义为 。
▷省略形式-4 我们将 定义为 。
尤里：“定义省略形式是什么意思？”
我：“就是说为了简洁，我们要把 写成 。”
▷括号的省略 为了看起来方便，后面我们会省略冗长的括号。
10.4.4 公理
我们来把皮亚诺公理导入形式系统 P。
▷公理 I-1
▷公理 I-2
▷公理 I-3
泰朵拉：“皮亚诺的公理不是有五条来着吗？”（2.1.1 节）
米尔嘉：“因为我们之前在使用类型的时候就已经导入了 PA1 和 PA2 啊。”
尤里：“米尔嘉大人，‘=’的定义还没出来呢！”
米尔嘉：“哥德尔的论文参考了《数学原理》，在论文中他将 x1 = y1 定义成了 。就是说‘不管集合 u 是什么样，只要 x1 属于集合 u，那么 y1 就也属于集合 u’。”
尤里：“嗯？”
米尔嘉：“就是通过‘不存在只包括 x1 或只包括 y1 的集合’定义了‘x1 和 y1 相等’。第 n 型也同理。”
下面我们把命题逻辑的公理导入形式系统 P。
把任意的逻辑公式 p、q、r 代入下面的公理 II-1～公理 II-4 中就能得到公理。
▷公理Ⅱ-1
▷公理Ⅱ-2
▷公理Ⅱ-3
▷公理Ⅱ-4
下面我们把谓词逻辑的公理导入形式系统 P。
▷公理Ⅲ-1
注意，这里假设：
- 表示“把 a 的所有自由的 6 v 用 c 代换后的逻辑公式”。
- c 跟 v 是同一个型的符号。
- 在 a 里，v 只要是自由的，c 中就没有受约束的变量。
6这里指的是变量、未知数，等等。——译者注
我：“ 是什么？”
米尔嘉：“把 a 中的 v 用 c 代换，也就是 substitute 后的结果。我举例解释一下吧。”
- a 是逻辑公式 。
- v 是名为 x1 的第 1 型变量。
- c 是名为 的第 1 型符号（数项）。
- 此时， 是逻辑公式 。
▷公理Ⅲ-2
注意，这里假设 v 是任意变量，b 中不出现自由的 v。
我：“要是 b 里不出现变量 v，那么就不会受到 的影响呗。”
接下来，我们把集合的内涵公理导入形式系统 P。
▷公理Ⅳ
注意，这里假设：
- u 是第 n + 1 型变量，v 是第 n 型变量。
- a 中不出现自由的 u。
我：“内涵公理？”
米尔嘉：“对应的是集合的内涵定义。”
我：“什么意思啊？”
米尔嘉：“总之就是‘逻辑公式 a 能决定集合 u’。”
我们再把集合的外延公理导入形式系统 P。
▷公理Ⅴ
我们把这个逻辑公式，以及将该逻辑公式“形式提升”后的逻辑公式定为公理。形式提升指的是让符号的类型都增加相同的数。也就是说，下面这些全都是公理。
- ……
我：“这次是外延公理……”
米尔嘉：“也就是说，假设对于任意 x1，‘x1 是否属于集合 x2’和‘x1 是否属于 y2’总是相容的。此时，我们设想集合 x2 跟集合 y2 相等……”
我：“嗯？”
米尔嘉：“这是集合的外延定义。‘集合中的元素决定集合本身’。”
10.4.5 推理规则
我们继续把推理规则导入形式系统 P。
▷推理规则-1 根据 a 和 得到 b。
此时，我们称 b 是根据 a 和 得到的有效结论
。我：“这是假言推理吧。”
▷推理规则-2 根据 a 得到 。
此时，我们称 是根据 a 得到的有效结论。
注意，此处的 v 是任意变量。
泰朵拉：“这个是……我不明白。”
米尔嘉：“就是说，既然没有条件的情况下都能导出 a，那么即使加上‘任意的’这个条件也能导出 a。”
◎ ◎ ◎
至此，形式系统 P 的定义就结束了。
“春天”结束了。“季节”向着“夏天”——哥德尔数推移。
……在这之前，先吃个午饭吧。
10.5 午饭时间
10.5.1 元数学
我们跟着米尔嘉上到三楼，进了一间写着 Oxygen 的房间。这个房间布置得像是一间同时供应零食的咖啡馆。天气很好，于是我们选择坐在露天阳台的座位上。阳台一边可以看见海，另一边则可以看见森林。万里无云，阳光柔和。
我点了咖喱饭，尤里要了意大利面，泰朵拉要吃三明治，米尔嘉则点了巧克力挞。
“一牵扯到形式系统，感觉逻辑学就大不一样了呢。”我说道。
“是吗？”
“一提到逻辑学，我就只能想到三段论 7 或者德·摩根定律什么的。从数学角度来研究数学 —— 我没想到还有这种领域……”
7英文写作 Syllogism，是逻辑学中由大前提和小前提出发导出结论的一种逻辑推理。——译者注
“不过这可是数理逻辑学的一部分。”米尔嘉说道。
“为什么非得把数学形式化呢？”尤里问道。
“要想严谨地进行讨论，做到形式化是非常重要的。”米尔嘉说道，“例如，假设我们想说‘这个证明是不可能的’，此时就需要定义‘证明是什么’‘证明是不可能的指的是什么意思’。没有这些定义，就没法区分以下两者：到底是自己碰巧没法证明，还是从原理上来讲就没法证明。”
我们大家都对米尔嘉的话点头表示同意。
“形式化也是对象化，也就是把自己想要讨论的东西明确为‘对象’。我们把以数学为对象的数学称为元数学。意思是‘关于数学的数学’，懂吧？也就是以形式系统来表示数学，再从数学角度去研究‘数学’这个表示结果。”
“这个是……嗯……”泰朵拉说道，“就像是 语言出现之后，我们才能进一步研究‘极限’，对吧？”
10.5.2 用数学研究数学
“米尔嘉大人，”尤里说道，“关于哥德尔不完备定理，我看到过一本书。书里说‘人生是不完整的，因而有趣’，还说‘如果全都明白了，人生也就没意思了’。人家当时有种恍然大悟的感觉，可是……”
“嗯，也有人这么想。”米尔嘉苦笑，“看到不完备定理的结果，就认为‘因为不明白，所以人生才有趣’。不过，这个吧，简直就像……”
米尔嘉闭上双眼，轻轻点了点头，然后睁开眼。
“就像看到了样式漂亮的蕾丝图案就认为‘破了洞也很美’。这些人并没有理解蕾丝图案的样式所衍生的东西。他们只是从表面来观察这个世界，没有看穿其结构。这些样式明明还蕴含着更深的乐趣。数学形式化后，人们就能够研究数学本身拥有的丰富的数学性结构，可以从数学角度来研究以形式系统表示的数学。这就是‘用数学研究数学’。自己关注的理论有着怎样的结构，多个理论之间有着怎样的关系……这明明应该是一个能衍生出非常多乐趣的问题。”
“就是要超越‘伽利略的犹豫’吗？”我下意识问道。
“不完备不是失败或者缺点，有可能是通往新世界的入口。”
10.5.3 苏醒
饭后，我从自动贩卖机买了瓶水，然后回到了 Chlorine。房间里一个人也没有。白板上写着尤里的留言：
我们去图书馆观光啦！等我们回来哦
米尔嘉带她们去参观图书馆了啊……嘁。
我喝了一口冰凉的矿泉水，开始回顾之前的内容。
嗯，虽然并没有全部理解，不过大体还算跟得上吧。总之，我们正在构建一个形式系统，下面我记得是哥德尔数跟原始递归谓词的定理来着。最后应该是反证法吧？如果假设存在形式证明，那么就会发生矛盾……米尔嘉大概会朝这个方向讲吧？
不久，饭后睡魔袭来，我趴在桌子上睡着了。
开门声。
“……所以说，是鱼的标记。”泰朵拉的声音。
“跟密码似的。”尤里的声音。
看来女生们回来了。不过我还在半梦半醒之中。
“呀，哥哥睡着了！”
“他一定累坏了。”
“话说回来，你刚刚说的‘态度’是？”米尔嘉的声音。
“啊，这个……”泰朵拉的声音。“我一直认为自己学习起来‘虽然花的时间比较长但很有毅力’。可是，光有这点是解不开数学题的，还需要类似灵感的才能，对吧？”
“没错，没错。”尤里的声音。
“我有时候想，自己没法产生灵感，但拓展一下思维应该还是能做到的。所以每逢解题时我就想‘如果换成米尔嘉学姐……’‘如果换成学长……’。”
“喔……”
“我从米尔嘉学姐和学长身上学到了很多好东西，不只是解题方法和诀窍，还有……怎么说呢，就是类似于‘态度’的东西。应该说是‘乐在其中，并且认真面对’吧。不是光考试考高分就行了，重要的是‘想要去真正理解’的态度。”
“哥哥他呀，一直在研究数学哦。”尤里的声音。
“学长他，在自己家里是什么样子的？”泰朵拉的声音。
“这个嘛……哥哥他有点迟钝呢。”
（喂！尤里！别瞎说呀！）
“而且，明显有顶撞阿姨的倾向……”
“话说，差不多该叫这只懒猫起床了吧？”米尔嘉的声音。
（懒猫？）
霎时间，一个冰得够呛的玩意儿“咚”地撞到了我的脖子上。
我大声叫着跳了起来。
“你醒了？”
黑发才女微笑着，手中拿着我那瓶矿泉水。
“那么，我们继续。下面进入‘夏天’。”
10.6 夏天——哥德尔数
10.6.1 基本符号的哥德尔数
在“夏天”阶段，我们要谈的是哥德尔数。
哥德尔数是分配给形式系统 P 的“符号、符号序列、符号序列的序列”8 的编号。
8有些文献中也称“符号、符号串、符号串的序列”。——编者注
首先，我们来定义基本符号的哥德尔数。
我们把不大于 13 的奇数作为哥德尔数分配给常量。
常量
0
(
)
哥德尔数
1
3
5
7
9
11
13
泰朵拉：“为什么是奇数？”
米尔嘉：“马上你就明白了。”
把大于 13 的质数分配给第 1 型变量。
第 1 型变量
x1
y1
z1
...
哥德尔数
17
19
23
...
把大于 13 的质数的平方分配给第 2 型变量。
第 2 型变量
x2
y2
z2
...
哥德尔数
172
192
232
...
把大于 13 的质数的立方分配给第 3 型变量。
第 3 型变量
x3
y3
z3
...
哥德尔数
173
193
233
...
像上面这样，一直到把大于 13 的质数的 n 次方分配给第 n 型变量。这样一来，我们就把哥德尔数分配给了常量和变量，也就是基本符号。
10.6.2 序列的哥德尔数
我们来定义序列的哥德尔数。注意，这里的序列指的是有限序列。
因为我们刚才已经定义了基本符号的哥德尔数，所以现在可以用哥德尔数的序列来表示基本符号的序列了。例如，思考下面这样的哥德尔数的序列。
我们让这个序列对应下面这样的乘积。
然后把这个乘积定义为 这个序列的哥德尔数。这里的 pk 是从小到大排列的第 k 个质数。
例如，表示 2 的数项是 这个基本符号的序列。基本符号 f 的哥德尔数是 3，基本符号 0 的哥德尔数是 1，因此基本符号的序列 可以用下面这样的哥德尔数的序列来表示。
把这个序列放在质数的指数位置上，构成下面这样的乘积。
计算该乘积，得到 。1080 这个数就是基本符号的序列 的哥德尔数。
尤里：“咦？ 不是 2 喵？”
米尔嘉：“含义的世界里的数 2，在形式的世界里是用数项 来表示的。”
尤里：“了解。”
米尔嘉：“把 这个符号序列用哥德尔数表示就是 1080。”
尤里：“喔……”
米尔嘉：“泰朵拉，你想没想到为什么要在基本符号这里用奇数？”
泰朵拉：“这……我不知道。”
米尔嘉：“我们可以通过哥德尔数的奇偶来判断哥德尔数是否构成序列。”
泰朵拉：“哦哦，如果哥德尔数是偶数，就表示序列！”
刚才我们给出了基本符号的序列 的示例。符号序列的哥德尔数跟符号序列的序列的哥德尔数可以用同样的思路来考虑。也就是说，不管构成序列的是什么东西，我们只要把构成序列的那个东西的哥德尔数放到按升序排列的质数的指数部分，取它们的乘积即可。
多亏质因数分解的唯一性，我们才能根据哥德尔数还原出唯一的序列。哥德尔的论文中用的是我们刚才说明的方法 —— 质数指数记数法，不过换成其他方法也可以。
那么，因为逻辑公式是符号序列，所以我们就可以定义“逻辑公式的哥德尔数”了。又因为形式证明是逻辑公式的序列，也就是符号序列的序列，所以我们还可以定义“形式证明的哥德尔数”。
这样一来，我们就可以把形式系统的一切都用哥德尔数这个数来表示了。
泰朵拉：“关于序列是符号序列还是符号序列的序列，能用哥德尔数来区分吗？”
米尔嘉：“这道谜题就留给你来解答吧。”
泰朵拉：“诶？两者都要是偶数，对吧？”
我：“我明白了。”
米尔嘉：“闭嘴。”
泰朵拉：“……我明白了。要看把哥德尔数质因数分解的时候出现的 2 的个数。”
米尔嘉：“2 的个数怎么了？”
泰朵拉：“如果 2 的个数是奇数，就是符号序列；如果是偶数就是符号序列的序列。”
米尔嘉：“很好。”
对于不完备定理，我们关注的是“形式证明是否存在于形式系统之中”。但是，如果不是“能理解形式证明的形式系统”，这样的问题就没有意义了。哥德尔用哥德尔数把形式证明译成了编码。这样一来，只要一个形式系统“能理解数”，那么这个形式系统就能理解形式证明。
泰朵拉：“把一切都用哥德尔数来表示……这个想法跟计算机的思路 —— 把一切都用位来表示很像呀。”
米尔嘉：“泰朵拉，你说反了。世界第一台计算机诞生于 1940 年代，哥德尔的证明在那之前哟。”
那么，到这里“夏天”就结束了。我们进入“秋天”吧。
10.7 秋天——原始递归性
10.7.1 原始递归函数
在“秋天”阶段，我们需要先离开一下形式系统 P，去一趟含义的世界。
接下来，我们要定义一个函数的同伴 —— 原始递归函数。这个函数用一句话说就是：获取函数的值时需要的“重复次数”存在上限的函数。
例如，求 n 的阶乘 的函数 就是一种原始递归函数，我们可以像下面这样来定义它。
下面试着求一下 吧。
像这样，要计算 ，只要使用 4 次定义即可；要计算 ，只要使用 n + 1 次定义即可。这就是“重复次数有上限”的含义。
事实上，要想计算 的值，还需要用到“×”和“+”的运算，所以我们再说得详细点儿吧。
假设函数 F, G, H 是用于处理数 (0, 1, 2, .. .) 的函数。
如下定义函数 F 时，我们称函数 F 是由函数 G 和 H 经原始递归定义 9的。