可是，位数应该能无限增加的啊……
“形式系统有这么多种吗？”
泰朵拉想了一会儿，突然大声说道：
相容的形式系统
对于形式系统中的任意逻辑公式 A，
无法证明 A 和
两者在该形式系统中都成立时，
我们就说，这个形式系统相容。
“就是轮流加上正负号……对吧？”
“看来需要列一个‘含义的世界’和‘形式的世界’的词汇表。”我说道。
“如果能用自然数给某个集合里所有的元素都编上号，该集合就是可数集。”米尔嘉不紧不慢地解释道，“根据村木老师给出的这个‘给实数编号’来看，由满足 0 <x< 1 的所有实数构成的集合是可数集。但是，刚刚你们应该已经证明了，该集合不是可数集。”
“……除了可数集这个词以外，我应该都明白。”
“嗯……”
“……没事，我已经把秒表停了。什么东西啊？”
“如果没有这部分，就能写成 1 × 17 的乘积形式了。”我回答道。
为了使用对角论证法，我们换个角度理解一下这道题。把“给所有实数编号”改成“给满足 0 <x< 1 的实数编号”吧。
解答 7-1
“由满足 0 <x< 1 的所有实数构成的集合”跟“实数集
”是一一对应的关系。因此根据解答 7-1a，实数集
如此，我们就能根据所有的逻辑公式来构建“单独的编号”了。这里说的“单独的编号”就叫作哥德尔数。
“泰朵拉，你是不是想说‘因为自然数有无数个，所以当然能用它们给无限集合的元素来编号’？可是啊，卡片上写着呢，实数集
“比如说，有限集都是可数集 3 对吧？这是因为，如果元素数量有限，那么我们就能给所有元素都编上号。”
“这……这个，嗯，对不起。”泰朵拉答道。
“喏，泰朵拉，你想起来了没？”
“这可说错了。”米尔嘉立马否定了泰朵拉的说法。
“A 和非 A 都无法证明……”泰朵拉不安地自言自语。
“嗯……”
“不完备？难道是哥德尔的那个……”
接下来，我们如下定义实数 B。
6又称无矛盾性、协调性或者一致性，指的是逻辑上的一致，就是在一个逻辑体系下永远不可能同时推理出一个命题 P 和其否命题非 P 同时成立。——编者注
公理测定仪
该谓词用于判断给出的自然数是否为公理的哥德尔数。
“……因此，我们拿自然数来当用于构建算术的形式系统的符号吧。举个例子，我们就拿 3 替代
“嗯，是啊。”我答道。
问题 7-1a（问题 7-1 的另一个说法）
证明由满足 0 <x< 1 的所有实数构成的集合不是可数集。
“把这三个条件合起来，自然而然就能想到用‘算术’来处理‘形式系统’了。不过，我们能自然而然就想到，可能是因为我们身处于哥德尔之后的时代。”
她拿起我的笔记本和自动铅笔，写下了“逻辑公式”以及“公理和推理规则”。
“你理解得很对。”米尔嘉回答道，“在形式系统包含的大量逻辑公式里，哪怕存在一个能证明 A 和
把上述两项组合在一起，就能想到如下内容。
下面来说说哥德尔数吧。
“我差不多明白刚才是在干什么了。不过我想问个问题。”
“哎呀！是啊！”泰朵拉红了脸。
“我不理解这个词汇表里的‘
“自由变量……那是什么？”泰朵拉问道。
在这里，我们试着把“以‘0.’开头的数”写作一般的形式。
“啊！……诶？ A 和
米尔嘉缓缓地来回看着我跟泰朵拉。
“……”
7也称自由变元。——译者注
问题 7-3（挑战：有理数和对角论证法）
用对角论证法证明“实数集不是可数集”后，把其中所有的“实数”换成“有理数”。这样一来，我们就能证明“有理数集不是可数集”。该证明错在哪里？
“完全没感觉到你过来了。”我说道。
到了四月，我跟米尔嘉就升高三了，泰朵拉就升高二了。时间过得好快啊。
“唔……不明白是吧？”
“原来如此……”我跟泰朵拉一起点头。
由满足 0 <x< 1 的所有实数构成的集合，跟实数集
“反证法里的‘矛盾’……”泰朵拉继续说道，“一说到矛盾，我就有一种特别混乱，理不清思路的感觉。但是，我现在觉得，矛盾或许是一个步骤，这个步骤包含于一种更纯粹的思路之中。矛盾只不过是一个数学术语……”
“师曰……”黑发才女酷酷地继续说道，“‘他要是马上发现了这个说法的破绽，因而得意忘形的话，你就给他看这张卡片的背面’。”
用“算术”表示“形式系统”，再用“形式系统”表示这里的“算术”。
注意看这张表格的第m行和第m列的交汇处，可知以下式子成立。这里拿了 Am，也就是 B 的小数点后的第m位数字来与bm作比较。
8也称句子（Sentence）、闭公式（Closed Formula）。——译者注
接下来，我们把表格的第m行和第m列挑出来看看。
数列 {bn} 如下。若an,n为偶数，则令bn= 1；若an,n为奇数，则令bn= 2。
然而，就像
米尔嘉又在笔记本上写下了“证明和定理”。
“嗯。用哪种方法都行，重要的是给所有整数都编上‘单独的编号’。因为所有的整数都能用自然数来编号，所以我们可以说，整数集
不过，往细了说呢，当出现像
“至于无限集的示例嘛，比如说，我们假设存在一个下面这样的整数集
“我明白了。”我说道，“它的意思是‘17 是质数’。你看，它强调的是，不管把哪两个数代入m跟n里，乘积都不等于 17。”
事实上，在哥德尔不完备定理的证明中，这些“测定仪”会详细提及。这可是“压卷之作”呀。而且，哥德尔的证明里甚至还出现了以下内容。
不完备的形式系统
对于形式系统中的某个语句 A，
A 和
我们就说，这个形式系统不完备。
“因为自然数能用算术来处理。”
既然满足 0 <x< 1 的所有实数都有编号，那么这个范围内的所有实数就都能用 An来表示。n是我们编给实数的编号。
她突然上扬了句尾的语调问道。我们不置可否地点点头。
或者，用圆周率 π 除以 10 也可得出这种小数。
这道题，肯定是能一下子答出来的题。
“从公理开始，用推理规则推导出逻辑公式，然后把逻辑公式加以排列，就能得到逻辑公式的有限序列。这种逻辑公式的有限序列就叫作‘证明’。在证明的结尾处出现的逻辑公式叫作‘定理’。”
我看着双手叉腰的米尔嘉，不由得很紧张。
“这说法有前途。”米尔嘉点点头。
“自然数的有限序列”的有限序列→自然数的有限序列→自然数
“呀！”泰朵拉叫道。
“嗯。在对角论证法的末尾部分，我们斜着选了一个
“我在等啊。”米尔嘉回道。
“相容的话，我们就能证明 A 和
“刚刚这个‘无法证明’说得比较简单，不过其含义显然就是‘不存在形式证明’。在理解不完备定理时，必须意识到‘数学上的证明’和‘形式证明’这两者的差别。‘无法证明’体现为‘不存在形式证明’。我们再用‘形式证明’这种表述，换个说法来描述一下第一不完备定理吧。”
“实数集
根据这个数列
把变量“把变量x用自指代换就称作对角化”用自指代换就称作对角化。
无法证明把“无法证明把x对角化了的语句”对角化了的语句。
——《没有书名为〈没有书名为〇〇的书〉的书》
“‘无法证明 A 和
我混乱了。
证明测定仪
该谓词用于判断给出两个自然数x、y时，
- x 是否为形式证明 A 的哥德尔数。
- y 是否为某语句 B 的哥德尔数。
以及 A 是否为 B 的形式证明。
“为……为什么
“嗯……我想起来了。形式系统中的证明指的不是数学意义上的证明，而是作为逻辑公式的有限序列来定义的‘形式证明’。学姐之前还列了五个逻辑公式来当
“什么意思？”
到底该说些什么好呢？
在这里我们使用反证法。
不过，判断可证明性这回事儿跟判断逻辑公式、公理、语句、证明相比，本身性质就不一样，“测定仪”的说法不是很恰当。
反证法中的假设：由满足 0 <x< 1 的所有实数构成的集合是可数集。
因此，根据反证法可知，由满足 0 <x< 1 的所有实数构成的集合不是可数集。
“哦哦……”
“你们知道我打算干什么吗？”
……关键在于这里么？
“m< 17 和n< 17 的部分呢？”泰朵拉问道。
“我想说的就是这个。”米尔嘉说道，“我们需要注意泰朵拉刚才所说的‘正确的解释’。对解释进行思考是归在数理逻辑里的模型论这个范畴里的。确实，一旦我们定义了解释，也就给形式系统赋予了含义。但是，正确的解释不单单只有一个。对于一个形式系统，我们可以想到很多解释。解释不同，形式系统的含义也会发生变化。然而，还是存在常用的标准解释的。”
“原来如此……应该找出实数跟有理数本质上的差异啊。”
问题 7-1
证明实数集
“相容性……也就是说，跟矛盾有关？”
“当然。”米尔嘉说道，“形式系统存在‘矛盾’指的是对于某个逻辑公式 A，我们能够证明 A 和
“为什么？”
“形式系统的……性质？”泰朵拉眨了几下眼。
“导入缺少的符号、变量、常数等，定义公理和推理规则。”
米尔嘉推了一下眼镜。
“可是……”泰朵拉说道，“米尔嘉学姐在写这个逻辑公式的时候，是想让我们以为‘17 是质数’的吧。从形式系统的角度来说，可能确实不应该考虑含义。但是，要是进行正确的解释，这个式子不也是为真……吗？”
接下来，我们把an,k列成一个像下图这样的表格，各行表示的是 An。
“把刚刚用对角论证法进行的证明里的……”米尔嘉开口回答，“‘实数’一词统统代换为‘有理数’。也就是说，假设 An表示有理数，列一个 An的表格，表格里写有在 0 <x< 1 这个范围内的全部有理数。然后挑出对角线上的数字，构成一个不存在于表格中的有理数 B。这样一来，就证明了‘有理数集不是可数集’。然而，有理数集应该是可数集。那么，到底是哪儿出错了呢 —— 这道题就是这个意思。”
可数集
可数集指的是能用自然数给所有元素编号的集合。
泰朵拉举起了手。
这样你就能理解了吧？
——能用符号来写；
“你忘了‘两者都无法成立’的情况。”米尔嘉说道。
“实数（或者有理数）中包含无限小数。”我说道，“当然，在 0 <x< 1 这个范围里也存在这种小数，例如
“有无数种，这要看定义。”
“这个嘛，因为我很了解对角论证法……”
“这个……”泰朵拉一脸快要哭出来的样子，“可是，要是能这么随便干的话，感觉就收不了场了……不管是谁都能随便创造数学，这样就会出现一波又一波乱七八糟的数学……”
“自由变量指的是不受
——能用算术来处理。
“村木老师简直就是千里眼啊。”米尔嘉说。
解答 7-3（挑战：有理数和对角论证法）
因为构成的数 B 不一定是有理数，所以不能使用对角论证法。
“这样吗？”米尔嘉在笔记上“沙沙”地列出了一个词汇表。
“没错。”
米尔嘉足足停了好一会儿才开口，看上去似乎很乐在其中。
“啊，这……也是呢。”泰朵拉说道。
可证明性测定仪
该谓词用于判断给出的自然数是否能成为某个语句的哥德尔数，以及是否存在针对该语句的形式证明。
背面还写着一道题。
哥德尔第一不完备定理（换言之）
在满足某个条件的形式系统中，存在满足以下两个条件的语句 A。
- 无法证明 A 成立。
- 无法证明 成立。
符号
“……谢谢。是什么题？”
“而下面这个逻辑公式 2 不包含自由变量，所以它是语句。”
如果想要从形式上表示算术这种在自然数的基础上进行加法或乘法运算的简单的数学，就需要把上面这些缺少的部分补上。”
“证明就是为此而存在的，泰朵拉。这就是这次要讨论的问题。”
“为什么要拿自然数当符号来用？”我问道。
“啊，麻烦等一下，米尔嘉学姐！”泰朵拉叫道。
“比方说，
证明完毕。
哥德尔第一不完备定理
满足某个条件的形式系统是不完备的。
这是因为，命题逻辑的形式系统里缺少以下内容。
“不行不行，这样是搞不定的。”
“你会这么问，就是说你已经忘记了形式系统吧？”
“先不说这个，我们来谈谈哥德尔当时证明第一不完备定理时用的技巧吧。这是一场往返于两个世界的旅行。”
我沉思。持续增加位数的话……
也就是说，我们可以规定，若an,n是偶数，则bn= 1；反过来，若an,n是奇数，则bn= 2。这样一来，对于所有的自然数n，以下式子都成立。
“泰朵拉，你能答吗？”米尔嘉问道。
“嗯？”我停下秒表。
“原来如此。Countable，可数的，就是能够 Count 的集合呀。”
解答 7-1a
采用反证法。
假设实数的集合
是可数集。
集合
的元素都可以像下面这样来表示。
如下定义实数 B。
但是，bn要像下面这样来定义。
根据bn的定义可知，对于任意自然数，
都成立。
因为实数 B 是集合
此时再看实数 B 的小数点后的第m位数字，就会发现
根据上面第 4 条可知，
在此，第 6 条与第 7 条相矛盾。
根据反证法，集合
泰朵拉说着，坐到了我左边的座位上。
改写成下面这样会更一目了然吧。
泰朵拉在我身旁抱着头呻吟。
米尔嘉拿出一张卡片放在桌子上，迅速在我右边坐下。
“否定也是如此。”米尔嘉说道。
请看下图。
这里也同时回答一下泰朵拉你拿来的那张“快递”卡片上的问题吧。
满足 0 <x< 1 的实数都可以用 An来表示。换句话说，这个表格里写的就是满足 0 <x< 1 的所有实数。我们来看一下这个表格的对角线。
“我明白了。”
泰朵拉一脸疲惫地举起双手。
“那个……米尔嘉，”我插了句嘴，“就是说，我们能从公理出发，沿着推理规则一路摸索到达 A 和
4即 0～9 这 10 种情况。——译者注
“可……可是，就算我说的方法不行，也许别人能想出个好方法呢？给有理数编号就办得到，给实数编号却绝对办不到？怎么就能这么说呢？”
“呜呜呜呜，好难啊，好复杂呀……”
“对，虽然形式系统相容，但不一定就能证明 A 和
她继续讲道：
“我们还可以用‘不完备’的定义来换一种说法。”
“有。第二不完备定理是关于相容性的定理。不过，现在就讲它的话，你会消化不了的。我们就留到下次再讲吧。”米尔嘉说道。
“话说，米尔嘉，”我插嘴道，“如果换成算术的形式系统，这个逻辑公式 1 表示的就是‘x是质数’这个谓词，逻辑公式 2 表示的就是‘17 是质数’这个命题吧？”
“这……是什么问题啊？”泰朵拉问道。
我再写得具体点吧。比如，An可能是下面这样。
“学长也是这样想呀。”泰朵拉回应道，“那个……我说一下别的哈。刚刚的证明里出现了反证法吧？”
“嗯，就是这样。另外，再比如说有理数集
2即 Cantor's Diagonal Argument，又称对角线证明等。——译者注
“米、米尔嘉学姐……我快不行了。”
解答 7-2（挑战：给实数编号）
讨论不正确。
5“元”字出于英语的 Meta，元问题就是在现有问题上延伸出来的问题，比现有问题讨论的程度更深一些。——译者注
完备的形式系统
对于形式系统中的任意语句 A，
能够证明 A 和
我们就说，这个形式系统完备。
我们用质数的乘积这种算术上的计算，根据逻辑公式得出了名为哥德尔数的自然数。那么反过来，用质因数分解（这也是算术上的计算）应该也能根据哥德尔数得出逻辑公式。不过，我们需要验证一下，看看使用质因数分解得到的自然数的有限序列是不是符合逻辑公式的形式。这就相当于构建一个谓词，也就是“逻辑公式测定仪”。例如，如果我们把 792179871410815710171884926990984804119873046875000 给逻辑公式测定仪，那么判断结果会为真。这是因为，这个大数是
◎ ◎ ◎
“嗯，很可能。我已经快消化不了了……”
当我们想把这个自然数的序列统合成一个自然数时，就需要另外准备一个把质数从小到大排列的序列（2, 3, 5, 7, 11, 13, .. .）。然后，把刚刚的自然数的序列
除了“逻辑公式测定仪”，我们还可以构建一些其他的有意思的谓词，例如下面这两个。
用“形式系统”表示“算术”。
“没错。不过表格是无限大的，所以我们并不能看到右下角的对角线。”
“……话虽这么说，数学家还是很了不起的。”泰朵拉说道，“皮亚诺的公理、戴德金的无限定义，还有魏尔斯特拉斯的
“是我说的……”我有点儿不镇定。
米尔嘉目光中带着几分顽皮，开心地解说道。
“是么？”清脆的声音从我们背后传来。
“可数集指的是‘能用自然数给所有元素编号的集合’。”
“我明白了。用这个方法只能给位数有限的小数编号。”
“并非如此。”米尔嘉说道，“虽然谁都能创造形式系统，但并不会收不了场。这一点跟谁都能创造音乐，但优美的音乐并不多很像。因为还有些重要性质是形式系统应该满足的。”
“只是举例子而已。现在只是随便分配一下。”米尔嘉微笑着回应道。
“能用算术来处理？”
“嗯，你这么想也行。”米尔嘉点头，“总之，语句指的是不包含自由变量的逻辑公式。好了，我们回到正题吧。假设对于形式系统中的语句 A，A 和
“啊，对不起！你在计时啊！”
由上图可知，如果我们在x轴上的 0 <x< 1 这个范围内选定一个实数a，则y轴上会出现一个对应的实数b。反过来，如果我们在y轴上选定一点b，则x轴上会出现一个满足 0 <x< 1 的实数a。满足 0 <x< 1 的实数跟所有实数之间的这种关系是一一对应的，不会出现遗漏，也不会重复。
“真的？”
你看，出现矛盾了吧？
米尔嘉用双手在胸前比划着一个小小的鸟笼，若有所思。她的手指也是弹钢琴的手指，不过跟盈盈的还不一样。她的手指纤长，形状秀美。
用“算术”表示“形式系统”。
“学长……学长你，为什么能一下子就回答出我的问题呢？”
“嗯。这么排列的话，会不会有遗漏呢……每一个数位上出现的数字肯定只有 10 种情况。我们可以无限增加位数，因此……咦？”
“有理数集也是 Countable Set 啊。”泰朵拉点了点头，又歪了歪头，“可是……能拿自然数来编号，不是理所当然的么。因为自然数是 1, 2, 3, ...，有无数个呀。”
“啊！原来如此。”
“喔……是用词的问题吧？”米尔嘉说道。
用具体例子来说会好些吧。
“学长，我找你好久了！有东西给你！”
形式系统
我看着米尔嘉，不由得提高了说话声。
“别说这些没用的，刚刚你说自己‘很了解’对角论证法？”
“提得好，但这不是问题。如果在意这些，就跳过那些不在范围内的实数，还有已经编完号的实数即可。你们之前讨论有理数的时候，应该也跳过了相等的数。”米尔嘉回答道。
“唔……”我集中精神想着。
“啊啊啊啊！别说出来呀！”泰朵拉喊道。
存在矛盾的形式系统
对于形式系统中的某个逻辑公式 A，
能够证明 A 和
我们就说，这个形式系统存在矛盾。
“解这题要用到康托尔的对角论证法 2——需要我解释吗？”
3也有一些学派主张有限集不属于可数集。
因为逻辑公式
实数跟有理数的差异是什么呢？实数的一部分是有理数，有理数可以用分数来表示。不过，现在是用小数来表示的。用小数来表示的话……啊！
拿刚刚的例子来讲的话，
“来聊聊算术的形式系统吧。”她突然来了这么一句。
“这个……”我说，“在小数点后面每一个数位上可能出现的数字是 0～9 这 10 个数字中的一个。也就是说，如果我们不胡乱给实数编号，而是从位数少的开始依次编号，就能都编上号？不不，应该不是这样……”
跟逻辑公式一样，形式证明也能定义哥德尔数。形式证明是“逻辑公式的有限序列”。因为用“自然数的有限序列”能表示逻辑公式，所以用“‘自然数的有限序列’的有限序列”就能表示形式证明。把上面那种将自然数的有限序列统合成一个自然数的方法连续用两次，就能像下面这样转换。因此，形式证明也能用“一个自然数”来表示。
“你的对角论证法是不是错了啊？每一个数位上出现的数字是有限的，所以要是分门别类来编号的话，就能说 0 <x< 1 是可数集了哦。”
“表现力？”我不解。
“不过，实际上泰朵拉说的没错，我就是想让你们以为这个式子表示的是‘17 是质数’……”米尔嘉俏皮地挤了挤眼说道，“我们回到正题。在命题逻辑的形式系统中，以下逻辑公式是写不出来的。
我们的目标是从以上假设出发，也就是通过“能用自然数给满足 0 <x< 1 的所有实数编号”，推导出矛盾。
我们使劲摇头。
“啊……是这么回事儿。——不对，这个不正确！”
“您有黑猫泰朵拉的快递，是村木老师的卡片！”
哥德尔第一不完备定理（再换言之）
在满足某个条件的形式系统中，存在满足以下两个条件的语句 A。
该形式系统中不存在 A 的形式证明。
该形式系统中不存在 的形式证明。
而且，用质数指数记数法还能把“自然数的序列”统合成“一个自然数”。例如，假设有个像下面这样的自然数的序列。
“对，就是不完备定理的那个‘不完备’。”米尔嘉说道。
“那个……米尔嘉学姐，请问，我能提个问题吗？”
“我不理解什么意思。”泰朵拉探头看着卡片。
“唔……那么，我们再来简单复习一遍形式系统吧。”米尔嘉说道，“形式系统中定义了‘逻辑公式’。逻辑公式只是符号的有限序列 —— 我们先不考虑这句话的含义。然后，选出几个被称为‘公理’的逻辑公式。另外，为了由逻辑公式推导出逻辑公式，还要准备‘推理规则’。”
“啊……是呀。我这是个关于问题的问题呢。”泰朵拉微笑，“采用这个方法的话，0 也会被编号。这样一来，实数就不在 0 <x< 1 这个范围内了。而且，像 0.01、0.010 和 0.0100 这样的实数是相等的，但可能会被重复计数。这就不准确了吧？”
“把缺少的部分补上……指的是什么呢？”
我们分别用自然数 3、5、17、7、19、9 来表示符号
问题 7-1
证明实数集
“诶？这题这么有名吗？”
“师曰：‘如果他在给泰朵拉讲完以后，说自己很了解对角论证法的话，就给他看这张卡片’。”
米尔嘉的话让我哑口无言。
首先，从表格里挑出位于对角线上的数字。
“根据辞典里的含义来看，‘否定’可能也是一个很容易令人误解的术语呢。”我说道。
“我们再试着好好思考一下形式系统这东西。形式系统中最根本的是符号。如果是命题逻辑的形式系统，就是用
自然数
“啊，这题我知道，是数学读物里常出现的题。”
我回过头，发现米尔嘉正站在我们身后。
我把桌子上的卡片翻了过来。
“……嗯。如果不妨碍你的话，还请解释一下。”
“解释的话，一下子就能解释完。我们先不说这个，你明白这道题的含义吗？”
“我们假设 A 是任意一个语句。泰朵拉刚才说的‘能证明 A 和
“啊！”对了！不该思考含义的。
——能用自然数来表示；
“要是实数 B 不在表格里，我们能把它追加到表格里吗？”
“学长，我们把这个方法叫作对角论证法，是因为我们关注的是表格的对角线，对吧？”
那么，接下来介绍一下康托尔的对角论证法。
“问题是哪里不正确。”米尔嘉说道。
“哥德尔不完备定理是什么？”泰朵拉问道。“
“米尔嘉学姐，这个式子的意思是？”泰朵拉问道。
下标有两个字符，看起来挺费劲的，不过你应该明白吧？an,1 表示的是实数 An的小数点后的第 1 位数字。an,2 是小数点后第 2 位数字，an,3 是小数点后第 3 位……以此类推。一般来说，an,k表示的是实数 An的小数点后的第k位数字。
“没事……”我把思绪移回这个世界，“呼 —— ”地舒了一口气。在解数学题时，我会进入异世界。现实中的自己身处于哪个时代、哪颗星球、哪个国家……全都失去了意义。
米尔嘉到底要把我们带向何方呢？
“嗯。出现了好多词，我已经晕了。”
“不行，如果 B 原本就不在表格里，就会产生矛盾，所以 B 不能不在表格里。就算我们把它追加到了表格里……因为追加后得到的是一个新的表格，所以如果用这个新的表格来像上面那样讨论，我们就还需要定义一个新表格中没有的实数 C。”
1日本的小学和初高中在学期末还举行结课典礼。——译者注
在村木老师出的‘给实数编号’这道题里，不管小数的位数有多少，我们都能给它编上号。但是，这只限于位数有限的情况。当位数无限时，就不能用这个方法了。因为用于编号的自然数会变得无限大。而自然数里没有无限大的数，所以我们不能用自然数给 0.333 ... 编号。”
因此，给满足 0 <x< 1 的所有实数编号，就相当于给所有实数编号。
“不，我不会。”泰朵拉摇摇头，“我只知道，学长的对角论证法里，某个地方对于‘实数’成立，而对于‘有理数’不成立……”
关于形式系统的定理。”米尔嘉答道，“哥德尔不完备定理包括两条定理，分别是第一不完备定理和第二不完备定理。第一不完备定理的内容如下。”
然而，如果我们在此回忆一下 B 是怎么来的，就会发现：对于所有的自然数n，
“卡片的背面？”
我赢了老师的“挑战”，不由得露出了笑容。
“很好。”米尔嘉点头。
“诶？诶诶诶诶？”
米尔嘉趁着兴头继续“上课”。
数列
没错。我们正在通过构建“逻辑公式测定仪”和“证明测定仪”等，来实现用“算术”表示“形式系统”。
——现在是放学后，这里是图书室。
“略有不同。”米尔嘉回答道，“之前是‘命题逻辑的形式系统’，这次是‘算术的形式系统’。”
我们就能顺藤摸瓜，找到所有大于等于 0 的有理数。接下来，只要跟上面处理整数时一样，轮流加上正负号即可。
卡片的问题告一段落，我们稍稍歇了一会。
话说回来，我们一开始就提到过构建“算术的形式系统”。这指的就是，把“算术”通过“形式系统”来从形式上表示出来。
泰朵拉也很认真地在思考。我可不能输给她。
“这样你就能理解了吧？”我说道。
“这么写的话，应该更容易理解吧。”
“你们还真是喜欢思考含义啊。”米尔嘉冷冷地说道。
“原来如此。”我想。形式系统中连矛盾这个概念都不用真假来定义啊。通过能不能证明来定义矛盾……原来如此。
嗯？
“啊……确实。我把质数的定义给忘了！”
米尔嘉轻轻点头，对我的话予以回应。
◎ ◎ ◎
沉默。
“了解。”
“用自然数来编号……”
“啊，就是之前那个‘装作不知道的游戏’吧。”泰朵拉说道。
“确实……不过那可不是白雪公主，是灰姑娘。”我说道。
“这个是元问题 5。”
例如，以 A5 = 0.31415 ... 为例，a5,k就会变成下面这样。
那么，我们现在忙的是什么呢？
季节是冬季，但已略有春意。已是二月末了，下个月就是毕业典礼跟结课典礼 1，还有春假。
这样一来，我们就得到了实数 B。
随后，米尔嘉停顿了一下说道：
“哥德尔不完备定理粉碎了这个性质。”
为什么要改成这样呢？这是因为，能给满足 0 <x< 1 的实数编号，就相当于能给所有实数编号。
不管位数多大都能编上号 —— 话虽这么说，可是这里的位数不是有限的吗？比如说 0.333 ... 这个数，这是一个无限小数，位数会无限增多。而村木老师的方法是能给那些位数有限的小数编上号，而不能给无限小数编上号！
“这样啊……”我自言自语般说道，“重要的是，就算是像对角论证法这种著名的论证方法，也需要好好确认自己是否已经完全理解了它的含义啊。看来，‘我听说过’‘我在书上看到过’跟‘我已经完全理解了’相比，差距还是相当大的呀。”
“用什么样的符号序列来当逻辑公式，用什么样的逻辑公式来当公理，准备什么样的推理规则……”这时米尔嘉将双臂大大伸展开来，“我们可以根据这些条件来构建各种各样的形式系统。我前一阵提到过的命题逻辑的形式系统算是其中比较简单的。玩起来很有趣，但是表现力却很低。”
“比如说，你们刚刚将m跟n默认为自然数，把m跟n认定成自然数，把‘×’认定成自然数的乘积，把‘≠’解释成表示不相等的符号。的确，这么解释的话，那个式子表示的就是‘17 是质数’这个命题。但是，如果m和n是实数呢？这样一来，那个式子表示的意思就不是‘17 是质数’了。所以，要给形式系统赋予含义时，我们需要切实定义解释。”
不不，现在不是盯着人家女生的脸看的时候。……确实，这样一来就证明了有理数集不是可数集。这……不好办呀。
“啊，是呢！平常我们用‘否定’这个词，就很有负面、消极的感觉，而在数学里就完全没有这种感情色彩，可以毫无顾忌地否定。”
“例如相容性 6。形式系统需要相容。”
“因为这个方法不能保证给所有的实数都编上号。”
“原来如此……”泰朵拉感叹道。看得出她松了口气。
这就是“形式系统的形式系统”。
问题 7-2（挑战：给实数编号）
以下关于“给实数编号”的讨论是否正确？
给以“0.”开头的数编号。小数点后第 1 位数字只有 10 种情况 4，因此，对于小数点后只有 1 位数字的数，我们可以无一遗漏地全都编上号。而对于小数点后第 1 位数字的 10 种情况下的每一个数，其小数点后第 2 位数字也都只有 10 种情况。因此，对于小数点后只有 2 位数字的数，我们也可以无一遗漏地全都编上号。重复以上步骤，不管以“0.”开头的数的位数增加到多大，我们都可以无一遗漏地为其编上号。因此，由以“0.”开头的所有数构成的集合是可数集。
在反证法中，我们要先假设一个想证明的命题的否定形式，然后推导出矛盾。现在我们想证明的命题是“由满足 0 <x< 1 的所有实数构成的集合不是可数集”，因此我们可以假设这样一个该命题的否定形式。
把对角线上的数列挑出来，排列如下。
我跟泰朵拉望着米尔嘉写的式子，看了好一会儿。
活力少女在沉思默想。没过多久，她举起了右手。
此外，0 < B < 1 在任何时候都成立对吧？也就是说，刚刚那个写着“满足 0 <x< 1 的所有实数”的表格里应该有这个实数 B！此处很重要！我们假设实数 B 在表格的第m行。那么，以下式子成立。
我原本以为，自己已经把对角论证法这个数学读物上常出现的知识理解得很透彻了。可是，我却没能找出“给实数编号”中的错误。
“还有第二不完备定理吗？”泰朵拉问道。
米尔嘉用认真的语气说道。可是，我却看到她眼里满是笑意。她在跟我开玩笑。
“什么问题？”
“不……不对吗？”泰朵拉双手放在头上思考着。
“嗯。”
“人们把进行自然数的加法、乘法等运算的系统叫作‘算术’。如果能构建这个形式系统，也就是‘算术的形式系统’，就能在形式上定义自然数的加法、乘法等运算。而且，顺利的话，或许还能用‘算术的形式系统中的语句’来表示‘2 是质数’‘5 的 17 次方等于 762939453125’这种‘算术的命题’。那么……”
