印符数论
螃蟹卡农和间接自指
对话《螃蟹卡农》中出现了三个间接自指的例子。阿基里斯和乌龟都描述他们所熟知的艺术作品------而那些作品却很偶然地恰好与他们所处的对话具有同样的结构。（你可以想象当我------对话的作者------注意到这一点的时候，该是多么惊讶！）而且，螃蟹描述了一个生物学的结构，也是具有同样的性质。当然，有人可能读了这个对话，理解了它，同时却没能注意到这对话本身也具有一个螃蟹卡农的形式。这就是只在一个层次上来理解它，而忽视了另外的层次。要想看出自指，必须即看到这个对话的内容，也看到它的形式。
在这一章里，我们将定义一个形式系统------印符数论，也就是把数论表示在印刷符号中。这个系统简称为TNT，这一方面是因为英文的”印符数论”是Typographical Number Theory，而另一方面是因为这个形式系统能释放出很强的能量。哥德尔的构造就不仅要依靠对这个形式系统中串的内容所作的描述，还要依靠对这些串的形式所作的描述。一个意想不到的回旋是：由于哥德尔所发现的奇妙的映射，串的形式能在这个形式系统自身里面描述。现在就让我们来熟识一下这个具有转圈绕弯本领的奇特系统。
我们希望在TNT中都能表示些什么
我们先列举一些数论里典型的句子，然后想法找一集基本的概念，使所有那些句子都可以用这些概念重新叙述出来。下一步再把这些概念一个一个地赋予符号。顺便说明，我们从一开始就得清楚，“数论”这个术语仅仅只涉及正整数和零（以及这样的整数的集合）的性质。这些数被称为自然数。负数在这个理论中没有位置。所以，当用到”数”这个词时，它仅意味着自然数。下面这一点对读者来说是很重要的------极其重要的：在你心里始终要区别开我们的形式系统（TNT），和那个比较起来规定得不是那么明确，然而却是令人感到舒适的古老的数学分支，即数论本身。后者我将称之为”N”。
N------即数论------中的一些典型的句子是：
(1)．5是素数。
(2)．2不是平方数。
(3)．1729是两个立方数的和。
(4)．没有两个正立方数的和本身又是一个立方数。
(5)．存在有无穷多个素数。
(6)．6是偶数。
现在看起来，似乎对每一个诸如”是素数”或”是立方数”或”正的”这样的概念，我们都需要有一个符号------但是这些概念其实并非最基本的。例如，素数性是与一个数所具有的因子有关的，而这些因子又与乘法有关。立方性同样要通过乘法来定义。那么，就让我们来重新叙述一下这些句子，这回用那些看起来更为初等的概念。
(1)．不存在这样的数a和b：它们都大于1，而且5等于a乘b。
(2)．不存在一个数b，使得b乘以b等于2。
(3)．存在数b和c，使得：b乘以b乘以b，加上c乘以c乘以c，等于1729。
(4)．对任何大于0的数b和c，不存在数a，使得a乘以a乘以a等于b乘以b乘以b加上c乘以c乘以c。
(5)．对每个数a，存在一个大于a的数b，具有这样的性质：不存在大于1的数c和d，使得b等于c乘以d。
(6)．存在一个数e，使得2乘以e等于6。
这种分析已经使我们大大接近了得到数论语言的基本成分。很清楚，有少数短语反复地出现：
对任何数b
存在一个数b，使得…
大于 等于 乘以 加上
0, 1, 2, 3…
这些短语的绝大部分都将被赋予单个的符号。一个例外是”大于”，它还能再进一步归约。事实上，句子”a大于b”可以变成
存在一个不等于0的数c，使得a等于b加上c。
数字
我们将不是对每一个自然数都赋予一个不同的符号。相反，我们将用一个非常简单、始终如一的方法，为每个自然数给出一个复合的符号------像我们在pq系统里做过的那样。下面是我们对自然数的记法：
零：
一： S0
二： SS0
三： SSS0
符号S有一个解释------是它后面的那个东西”的后继”。因此，SS0的解释按字面上就是”零的后继的后继”。这种形式的串被称为数字。
变元和术语
显然，我们需要有一个方法来表示那些非指定的数------或者说可变的数。为此，我们将使用字母a、b、c、d、e。但就这五个是不够的。我们需要有一个无限制的供应方法，就像我们对命题演算中的原子所做的一样。我们将用一个相类似的方法去制造更多的变元：在数上面加撇。举例来说：
e
d
c”
b”
d""
都是变元。
从某种角度来说，用字母表的前五个字母多少是种奢侈，因为我们本可以只用a和撇号就行了。后面，我将真的不用b、c、d和e，结果将得到TNT的一种”简朴的”版本------此处所谓的”简朴”是说读懂复杂的公式变得较难了。不过当前我们还是奢侈一点。
那么，加法和乘法怎么办呢？非常简单：我们用习惯的符号”+“和”•“。然而，我们还要引进一个关于打括号的要求（我们现在正慢慢地滑入定义TNT良构串的规则中）。例如，要写”b加上c”和”b乘以c”，我们用这样的串
(b+c)
(b•c)
对这样的括号不能马虎。违反了这个约定就会产生一个不良构的公式（“公式”？我用这个术语来代替”串”，是因为习惯上是这样做的。一个公式不多不少就是TNT的一个串）。
顺带说一下，加法和乘法总是被认为是二元运算------也就是它们只把两个数联结起来，而从来不把三个或更多的数联结起来。因此，如果你希望去翻译”1加2加3”，你必须判定下面两个表达式中哪一个是你想要的：
(S0+(SS0+SSS0))
((S0+SS0)+SSS0)
下一个我们将要符号化的概念是等于。这非常简单：我们用”=“。直接把在N------非形式的数论------中所用的标准符号拿来的好处是明显的：容易读懂。而缺点则类似于对几何作形式处理时使用”点”和”线”这些词：除非一个人头脑非常清楚并仔细小心，否则他会很容易把词的普通意义与形式符号的严格受规则管辖的行为相混淆。在讨论几何时，我把形式术语写成黑体，以示日常用词与形式术语之间的区别。于是，在椭圆几何里，一个点是两个普通的点的结合体。但在这里，我们没有作这样的区分。因此需要特别小心，不要混淆一个符号与随它而来的所有联想。参考一下pq系统：像我以前说过的，”---“这个串不是3这个数，但它起着与3同构的作用，至少在加法的范围里是这样。对串SSS0可以做类似的说明。
原子与命题符号
命题演算的所有符号，除了用于构成原子的字母（P、Q和R）之外，都将在TNT中使用，并且仍然保持它们的解释。原子的角色将由这样的串来充当：当它们解释出来时，是一些关于相等的陈述，诸如S0=SS0或（S0·S0）=S0。现在，我们已经有了足够的准备来做一些从简单句子到TNT记号的翻译了：
2加3等于4：(SS0+SSS0)=SSSS0
2加2不等于3：～(SS0+SS0)=SSS0
如果1等于0，那么0等于1：＜S0=0<!-- -->{=html}0=S0＞
这些串当中的第一个是原子，其余的都是复合公式。
自由变元与量词
上述所有的良构公式都具有这样的性质：它们的解释是句子，而这些句子不是为真，就是为假。但有的良构公式却不具有这个性质，比如这一个：
(b+S0)=SS0
它的解释是”b加1等于2”。由于b是未指定的，没有办法为这个陈述指派一个真值。它像一个含有代词的脱离了上下文的语句，例如”她很笨拙”。它既不真也不假，它等着读者把它放进一个上下文中去。正因为它既不真也不假，这样的公式就被称为开公式，而变元b则称为自由变元。
有一个办法能把一个开公式改变成一个闭公式，或者说句子。这个办法就是在它前面加一个量词------或者是短语”存在一个数b，使得…”，或者是短语”对任何数b”。在第一种情况下，你得到的句子是
存在一个数b，使得b加1等于2。
显然这是真的。在第二种情况下，你得到的句子是
对任何数b，b加1等于2。
显然这是假的。我们现在来为这两种量词引进符号。这些句子翻译成TNT记号就是下面这样：
b:(b+S0)=SS0（""代表”存在”）
b:(b+S0)=SS0（""代表”任何”或”所有的”）
一定要注意，这些陈述不再是关于未指定的数了。第一个陈述是一个存在断言，而第二个是一个全称断言。即便用c而不是b来写它们，也还是意味着同样的事情：
c:(c+S0)=SS0
c:(c+S0)=SS0
在量词管辖之下的变元称为一个量化变元。下面的两个公式说明了自由变元与量化变元之间的区别：
(b·b)=SS0 （开的）
～b:(b·b)=SS0 （闭的，是一个TNT的句子）
第一个公式表达了可能为某个自然数所具有的一个性质。当然，没有任何自然数具有这个性质。而这正是由第二个公式表达出来的。理解这两者之间的下列区别是很关键的：一个是带自由变元的串，它表达了一个性质，而另一个串里的变元是量化的，它表达了一个真实或虚假断言。至少带一个自由变元的公式------开公式------翻译成自然语言后就称为谓词。它是一个不带主语的句子（或者是这样的句子，它的主语是一个脱离上下文的代词）。例如，
-
“是一个不带主语的句子”
-
“会是一个反常现象”
-
“同时朝后和朝前跑”
-
“一经请求就即席演奏六声部赋格”
都是非算术的谓词。它们所表达的性质，对具体的事物来说可以具有，也可以不具有。人们当然也可以坚持”哑主语”概念，比如”某某”。一个带自由变元的串就像一个用”某某”来当作其主语的谓词。例如，
(S0+S0)=b
就像是在说”1加上1等于某某”。这是一个带变元b的谓词。它表达了数b可以具有的一个性质。如果有人用各种各样的数字去替换b，他就会得到一连串公式，其中的大部分都将表达”假理”。下面是关于开公式与句子之间的区别的另一个例子：
b:c:(b+c)=(c+b)
当然，这个公式是一个表示加法交换律的句子。相反，
c:(b+c)=(c+b)
却是一个开公式，因为b是自由的。它表达了未指定的数b可以具有，也可以不具有的一个性质------即，与所有的数c可交换。
翻译我们的例句
这样，我们的词汇表就全了。我们将以此来表达所有的数论语句！得有大量的实践才能掌握这些本领：如何用这种记法去表达N中复杂的陈述，以及倒过来，如何给出良构公式的意义。为此，我们还回到开始那六个例句，想法给出它们的TNT翻译。顺便说说，不要以为下面给出的翻译是唯一的------远不是如此。每一个句子都能由许多------无穷多的------方法来表达。
我们从最后的一个：“6是偶数”开始。这个例句我们用更初等的概念重述出来就成了”存在一个数e，使得2乘以e等于6”。这很容易：
e:(SS0·e)=SSSSSS0
注意必须有量词。仅仅像下面这样写是绝对不行的：
(SS0·e)=SSSSSS0
这个串的解释当然既不真也不假，它只是表达了数e可以具有的一个性质。
奇怪的是，因为我们知道乘法是可交换的，于是我们可以很容易地就把上式写成：
e:(e·SS0)=SSSSSS0
或者，知道相等是一个对称关系，我们换一下次序去写等式的两边：
e:SSSSSS0=(SS0·e)
现在，关于”6是偶数”的这三个翻译是完全不同的串，而且还有一件事也绝不是显然的：它们之中任何一个是否是定理，受到其它任何一个是否是定理的制约（但是—p-q---是定理这个事实，几乎一点也不依赖下面这一事实：其”等价的”串-p—q---得是个定理。因为，作为人，这种等价性是在我们的心里，所以我们几乎是自动地去想到解释，而不考虑公式的结构方面的性质）。
我们可以很快解决句子2：“2不是一个平方数”，它的翻译几乎立刻就可以写出来：
～b:(b·b)=SS0
然而，我们又一次发现了歧义。如果我们选用下面这种写法将如何呢？
b:～(b·b)=SS0
第一种写法是说，“不存在一个数b，具有这样的性质，b的平方是2”，而第二种写法是说，“对任何数b，b的平方不是2。“再一次地，在我们看来，它们在概念上是等价的------但是对TNT来说，它们是不同的串。
我们接着来看句子3：“1729是两个立方数的和”。这次的翻译要含有两个存在量词，一个跟在另一个后面，如下所示：
还有许多其它可采用的写法。颠倒量词的次序；交换等式的两边；换变元为d和e；颠倒相加的次序；以不同方式相乘；等等，等等。不过，比较起来我更喜欢下面这两种翻译：
b:c:(((SSSSSSSSSS0·
SSSSSSSSSS0)·SSSSSSSSSS0)
+((SSSSSSSSS0·SSSSSSSSS0)
·SSSSSSSSS0))
=(((b·b)·b)+((c·c)·c))
和
b:c:(((SSSSSSSSSSSS0·
SSSSSSSSSSSS0)·SSSSSSSSSSSS0)
+((S0·S0)·S0))
=(((b·b)·b)+((c·c)·c))
你看出来是为什么了吗？
这一行中的窍门
现在我们来对付与此相关的句子4：“没有两个正立方数的和本身又是一个立方数”。假设我们只是要表述”7不是两个正立方数的和”。做这件事最简单的方法是，把断定7是两个正立方数的和的公式加以否定。这很像前面那个含1729的句子，只是我们在此必须加进去这样的条件：那两个立方数是正的。对付这个问题的窍门是在变元的前面加符号S，如下所示：
b:c:SSSSSSS0
=(((Sb·Sb)·Sb)+((Sc·Sc)·Sc))
你看，我们不是用b和c做立方，而是用它们的后继，那一定是正的，因为不论b还是c，能取的最小值就是零。于是，右边就表示两个正立方数的和。附带说一下，要注意当把短语”存在有数b和c使得…”翻译出来时，并不包含代表”和”的符号""。这个符号只是用来连接整个的良构串，而不是用于结合两个量词的。
现在我们已经翻译了”7是两个正立方数的和”，我们希望否定它。这只要在整个东西前边加一个弯号。（注意：虽然想要的短语是说”不存在数b和c使得…”但你不要把每个量词都否定）于是我们得到：
～b:c:SSSSSSS0
=(((Sb·Sb)·Sb)+((Sc·Sc)·Sc))
可是我们原本要断言的性质不是对7而言的，而是对所有的立方数。因此，让我们把公式中的数字SSSSSSS0换成串（（a·a）·a），它是”a的立方”的翻译：
～b:c:((a·a)·a)
=(((Sb·Sb)·Sb)+((Sc·Sc)·Sc))
目前这个阶段，我们拥有一个开公式，因为其中的a是自由的。这个公式表达了一个数a可以具有也可以不具有的一个性质------而我们的目的是要断言所有的数都具有这个性质。这很简单------只要在整个东西前面加上一个全称量词：
a:～b:c:((a·a)·a)
=(((Sb·Sb)·Sb)+((Sc·Sc)·Sc))
一个同样好的翻译是：
～a:b:c:((a·a)·a)
=(((Sb·Sb)·Sb)+((Sc·Sc)·Sc))
在简朴的TNT中，我们可以用a来代替b，a”代替c，于是这个公式将成为：
～a:a:a”:((a·a)·a)
=(((Sa·Sa)·Sa)+((Sa”·Sa”)·Sa”))
那么句子1：“5是素数”又怎么样呢？我们已经把它改写成了这个样子：“不存在数a和b，它们都大于1，使得5等于a乘以b”。我们可以将它稍加改变如下：“不存在数a和b，使得5等于a加上2，再乘以b加上2”。这又是一招------因为a和b被限定只能取自然数值，所以这种方法同样也是可行的。现在，“b加上2”可以翻译成(b+SS0)，但是还有一个更为简短的写法------SSb。同样，“c加上2”可以写成SSc。现在，我们的翻译非常的简洁：
～b:c:SSSSS0=(SSb·SSc)
如果没有前面的弯号，它就是断言这样的两个自然数存在：当它们分别增加2之后，其乘积等于5。带上前面的弯号，整个陈述就被否定了，结果就成了断言：5是素数。
如果我们想断言d加e加1是素数，而不说5，那么，最经济的方法是用串（d+Se）来替换代表5的那个数字：
～b:c:(d+Se)=(SSb·SSc)
又一次，得到一个开公式，它的解释是一个既不真也不假的句子，它只是一个关于两个未指定的数d和e的断言。注意，用串（d+Se）来表示的数必然是大于d的，因为已经为d加上了一个虽然是未指定的但一定是正的数值。因此，如果我们在变元e上进行存在性的量化，我们将得到一个公式来断言：
存在一个数，它大于d，并且它是素数。
e:～b:c:(d+Se)=(SSb·SSc)
好，我们现在剩下要做的全部事情就是要断言：不管d是什么，这个性质实际上总是有的。做这件事的方法是在变元d上进行全称性的量化：
d:e:～b:c:(d+Se)=(SSb·SSc)
这正是句子5的翻译！
翻译习题
这样，我们就完成了六个典型数论句子的翻译练习。但是，这并不一定就使你成了一个使用TNT记号的专家。还有一些技巧需要掌握。下面的六个良构公式可以检验你对TNT记法的理解。它们的意思是什么？哪些是真的（当然，是在解释之下），哪些是假的？（提示：对付这个练习的方法是逐步向左移。首先，翻译原子；其次，想出加上一个单个的量词或一个弯号会对翻译起什么作用；然后向左移，加上另一个量词或弯号；然后再向左移，再做同样的事情。）
～c:b:(SS0·b)=c
c:～b:(SS0·b)=c
c:b:～(SS0·b)=c
～b:c:(SS0·b)=c
b:～c:(SS0·b)=c
b:c:～(SS0·b)=c
第二个提示：或者它们中有四个为真两个为假，或者有四个为假两个为真。）
怎样区分真和假？
到了这个时候，值得停一下好好想一想：一个能筛选出真公式与假公式的形式系统是什么意思。这个系统要去处理所有这些串------它们在我们眼里像是陈述------它们作为一种制品只有形式，没有内容。并且这个系统要像一个筛子一样，只能通过那些带有特殊样式------“真理样式”------的制品。如果你自己已经走通了上述六个公式，并且考虑了它们的意义，从而分离了真的和假的，你将领略到这种系统必须要具有的那种精妙之处，它们能够做同样的事情------但却是印符地来做！用来区分真陈述集合与假陈述集合的界线（用TNT记法写成）绝不是笔直的；这个分界线有着许多莫测的弯曲（回想一下图18），数学家们在这里和那里描绘其走向，一直工作了好几百年。不难想象，如果有一个印符的方法，能保证把任何一个公式放到这分界线的适当的一边，那该多棒！
关于良构性的规则
有一张良构公式的形成规则表是必要的。下面就给出这张表。先要做些准备，定义数字、变元和项。这三种类型的串是良构公式的组成成分，但仅就它们本身还谈不上良构。最小的良构公式是原子；然后有一些将原子结合起来的规则。这些规则中，有许多是递归加长规则，它们把某个给定种类的东西作为输入，产生出同一种类的长一些的东西。在这张表里，我用”x”和”y”代表良构公式，而用”s” “t”以及”u”去代表其他种类的TNT串。不用说，这五个符号没有一个本身是TNT的符号。
数字：
0是一个数字。
一个前面加上了S的数字仍是一个数字。
例子：0 S0 SS0 SSS0 SSSS0 SSSSS0
变元：
a是一个变元。如果我们不限于简朴版本，那么b，c，d以及e同样也都是。
一个加了一撇的变元仍是一个变元。
例子：a b c” d” e""
项：
所有数字和变元都是项。
一个前面加了S的项仍是一个项。
如果s和t都是项，那么(s+t)和(s·t)也同样都是项。
例子：0 b SSa (S0·(SS0+c)) S(Sa·(Sb·Sc))
项可以分成两类：
(1)．确定项。这些项不包含变元。
例子：0 (S0+S0) SS((SS0·SS0)+(S0·S0))
(2)．非确定项。这些项包含有变元。
例子：b Sa (b+S0) (((S0+S0)+S0)+e)
以上的规则是告诉我们如何制作良构公式的部件，下面的规则是告诉我们如何去制作完整的良构公式。
原子：
如果s和t是项，那么s=t是一个原子。
例子：S0=0 (SS0+SS0)=SSSS0 S(b+c)=((c·d)·e)
如果一个原子中含有一个变元u，那么u在它里面是自由的。所以在上面最后一个例子里有四个自由变元。
否定：
一个前面加了一个弯号的良构公式是良构的。
例子：～S0=0 ～b:(b+b)=S0 ～＜0=0S0=0＞～b=S0
一个变元的量化状况（就是说变元是自由的还是量化的）在否定之下并不改变。
复合：
如果x和y是良构公式，并且没有什么变元在它们中的一个里面是自由的而在另一个里面是量化的，那么下列都是良构公式：
＜xy＞，＜xy＞，＜xy＞。
例子：＜0=0～0=0＞ ＜b=b～c:c=b＞ ＜S0=0\rightarrow$$\forallc:～b:(b+b)=c＞
一个变元的量化状况在这种情况下不改变。
量化：
如果u是一个变元，x是一个良构公式，u在它里面是自由的，那么下面的串是良构公式：
u:x和u:x
例子：b: c:～b:(b+b)=c～c:Sc=d
开公式：含有至少一个自由变元。
例子：～c=c b=b ＜b：b=b～c=c＞
闭公式（句子）：不含自由变元。
例子：S0=0 ～d:d=0 c:＜b:b=b～c=c＞
这就完成了TNT良构公式的形成规则表。
再来几个翻译练习
现在，给你几个练习做，检验一下你对TNT记法的理解。试一试把下列N句子中的前四个翻译成TNT句子，把最后一个译成一个开的良构公式。
所有的自然数都等于4。
不存在等于它自身平方的自然数。
不同的自然数有不同的后继。
如果1等于0，那么每个数都是奇数。
b是2的某次方。
你可能发现最后的一个有点难对付。不过它和下一个一比，就小巫见大巫了：
b是10的某次方。
奇怪的是，这一个需要有极大的聪明机智才能翻译成我们的记法中的东西。我要告诫读者：只有在你乐意把几小时几小时的时间花在它上面------并且你还颇知道点数论的时候------再去尝试做这道题。
一个非印符系统
至此，我们结束了对TNT记法的说明，但我们还没有表明如何使TNT成为我们描述过的那个雄心勃勃的系统。这一点若是成功了，我们曾对各个符号做出的解释就会得到证实。不过，在我们做到之前，这些特定的解释并不比对pq系统的符号所作的”马-苹果-幸福”解释更有意义。
有人可能会建议按下列方法来构造TNT：（1）没有任何推理规则。它们是不必要的，因为（2）我们取数论的所有真语句（用TNT记法写成）来当作公理。多简单的处方！不幸的是，任何人一望即知这根本是空洞无物的说法。第（2）部分显然不是对串的一个印符描述。TNT的整个目的就是要确定：是否可能，以及如何印符地刻划所有对应于真理的串。
TNT的五条公理及第一组规则
于是，我们将遵循一条比上述建议困难得多的路线走下去：我们将有公理和推理规则。首先，按照约定，命题演算的全部规则都被接受进TNT里来。因此，下面这个式子将是TNT的一个定理：
＜S0=0～S0=0＞
推导出它的过程与推导＜P～P＞的过程是一样的。
在我们给出更多的规则之前，让我们先给出TNT的五条公理：
公理1：a:～Sa=0
公理2：a:(a+0)=a
公理3：a:b:(a+Sb)=S(a+b)
公理4：a:(a·0)=0
公理5：a:b:(a·Sb)=((a·b)+a)
（在简朴的版本中，用a来代替b）。它们都很容易理解。公理1陈述了有关数0的一个特殊事实；公理2和3是关于加法的性质的；公理4和5是关于乘法的性质的，并且特别涉及到与加法的关系。
五条皮亚诺公设
顺便说说，公理1的解释------“零不是任何自然数的后继”------是自然数的五条著名的性质之一，这些性质是由数学家和逻辑学家朱·皮亚诺于1889年首次明确认定的。皮亚诺沿着欧几里德的路线提出他的公设，他的做法是：不去致力于把推理的原则加以形式化，而是力图给出一个自然数性质的小小的集合，从它出发，其余的每样东西都能由推理而得出。因此，皮亚诺的努力也许可以认为是”半形式化的”。皮亚诺的工作具有重要影响，所以，介绍一下皮亚诺的五条公设是会有好处的。由于”自然数”概念是一个皮亚诺设法去定义的东西，所以我们将不使用这个充满了内涵的熟悉的术语”自然数”。我们将用一个未经定义的术语”神怪”来替代它，这个术语是一个来得很新鲜的词，并且对我们来说这个词是没有内涵的。于是，皮亚诺的五条公设是在神怪上加了五条限制。另外还有两个未定义项：“怪物”与”元”，我留给你自己去想出它们是要表示通常的什么概念。五条皮亚诺公设是：
(1)．怪物是一个神怪。
(2)．每一个神怪有一个元（它也是一个神怪）。
(3)．怪物不是任何神怪的元。
(4)．不同的神怪有不同的元。
(5)．如果怪物有X，并且每个神怪都把X递送给它的元，那么所有的神怪都得到X。
在《和声小迷宫》中的那些灯的启发下，我们将把众神怪的集合命名为”造物神”。这又回到了盖奥尔格·康托尔的死对头，德国数学家和逻辑学家列奥波尔德·克罗内克的那句名言：“造物神造出了自然数，其余的一切都是人的事。”
你可能认出来了，皮亚诺的第五条公设就是数学归纳法原理------继承性论证的另一说法。皮亚诺希望他加在概念”怪物”、“神怪”以及”元”上的五条限制是如此之强，以至于如果两个不同的人在心里对这些概念形成意象，这两个意象会有完全同构的结构。举例来说，每个人的意象都会包括无穷多个不同的神怪。并且，大概每个人都会同意，没有一个神怪与它自身的”元”完全相同，或者与它的”元”的”元”完全相同，等等。
皮亚诺希望把自然数的本质纳入到他的五条公设之中。数学家们一般都承认他成功了，但是这并没有减少下面这个问题的重要性：“怎样区别关于自然数的真陈述和假陈述句？“为了回答这个问题，数学家们又转向完全形式化的系统，比如TNT。不管怎么说，你将在TNT中看到皮亚诺的影响，因为所有他的公设都以这样或那样的方式被引进到TNT里来了。
TNT中的新规则：特称和概括
现在我们来看TNT中的新规则。许多这种规则使我们能深入并改变TNT原子的内部构造。在这个意义上，它们是在和串的更”微观”的性质打交道，而不像命题演算的规则，把原子当作不可分割的单位。举例来说，我们想从第一条公理中抽出串～S0=0。为此，我们需要有一条规则使我们能去掉一个全称量词，同时，如果我们愿意，能改变剩下的串的内部构造。下面就是这么一条规则：
特称规则：假设u是一个出现在串x中的变元。如果串u:x是一个定理，则x也是定理，并且，对x中的u做任何替换而得到串同样也都是定理，但不论u出现在什么地方，都要用同一个项去替换。
（限制：用来替换u的项必须不包含任何在x中被量化了的变元。）
特称规则使我们能把刚才那个串从公理1中提取出来。这是一个一步的推导：
a:～Sa=0 公理1
～S0=0 特称
注意，特称规则将允许某些包含自由变元的公式（即开公式）成为定理。举例来说，用特称，下列的串也能从公理1导出：
～Sa=0
～S(c+SS0)=0
还有另一个规则，概括规则，使我们能把全称量词放回到一些定理中去------那些定理所含的变元由于以前使用了特称规则而成为自由的了。举例来说，把概括规则作用到上面的那两个串中的第二个，我们就得到：
c:～S(c+SS0)=0
概括正好取消了特称的作用，反过来也一样。通常，概括总是用于某些中间步骤已经以各种各样的方式对开公式作了一番变换之后。下面是这条规则的严格叙述：
概括规则：假设x是一个定理，其中的变元u是自由出现的。那么u:x是一个定理。
（限制：在一个幻想里面，不允许对任何自由出现在该幻想的前提中的变元作概括。）
在这两个规则上加限制的必要性很快就会清楚地表现出来。附带说一下，这个概括与第二章中提到过的欧几里德在证明素数有无穷多时所用的概括是一回事。我们已经可以看到，符号变换规则开始靠近数学家们所使用的那种推理了。
存在量词
刚才的两条规则说的是如何取走全称量词以及如何把它们放回去，下面的两条规则说的是如何处理存在量词。
互换规则：假设u是一个变元。那么串u:～与～u:在任何定理中的任何地方都是可互换的。
举个例子，让我们把这条规则应用到公理1：
a:～Sa=0 公理1
～a:Sa=0 互换
附带地，你可能注意到，这两个串都是”零不是任何自然数的后继”这个句子在TNT中的完美自然的表述。所以，它们能够容易地变来变去是一件好事。
下一条规则则更为直观了。它对应于非常简单的一种推理，即我们从”2是素数”到”存在一个素数”所做的推理。这条规则的名称是自明的：
存在规则：假设一个项（可以含有变元，只要是自由的）在一个定理中出现一次或多次。那么，这个项的任何（或者是一些，或者是所有）出现都可以用一个不在定理中出现的变元来替代（替代之后当然就在这个定理中出现了），相应的存在量词则必须放在最前面。
让我们------像往常一样------对公理1来应用这条规则：
a:～Sa=0 公理1
～b:a:～Sa=0 存在
你现在可以试试根据迄今所给出的规则去调拨符号，产生出定理～b:a:Sa=b。
等号规则和后继规则
我们已经为变换量词给出了规则，但到目前为止还没有一个针对符号和”S”的规则。我们现在就来纠正这一状况。以下，r、s和t都代表任意的项。
等号规则：
对称：如果r=s是一个定理，那么s=r同样也是定理。
传递：如果r=s和s=t都是定理，那么r=t也是定理。
后继规则：
加S：如果r=t是一个定理，那么Sr=St是一个定理。
去S：如果Sr=St是一个定理，那么r=t是一个定理。
这些规则能够为我们提供极其丰富的各式各样的定理。比如，下列推导就产生出一些相当基本的定理：
(1) a:b:(a+Sb)=S(a+b) 公理3
(2) b:(S0+Sb)=S(S0+b) 特称（S0对a）
(3) (S0+S0)=S(S0+0) 特称（0对b）
(4) a:(a+0)=a 公理2
(5) (S0+0)=S0 特称（S0对a）
(6) S(S0+0)=SS0 加S
(7) （S0+S0）=SS0 传递（第3、6行）
(1) a:b:(a·Sb)=((a·b)+a) 公理5
(2) b:(S0·Sb)=((S0·b)+S0) 特称（S0对a）
(3) (S0·S0)=((S0·0)+S0) 特称（0对b）
(4) a:b:(a+Sb)=S(a+b) 公理3
(5) b:((S0·0)+Sb)=S((S0·0)+b) 特称（(S0·0)对a）
(6) ((S0·0)+S0)=S((S0·0)+0) 特称（0对b）
(7) a:(a+0)=a 公理2
(8) ((S0·0)+0)=(S0·0) 特称（(S0·0)对a）
(9) a:(a·0)=0 公理4
(10) (S0·0)=0 特称（S0对a）
⑾ ((S0·0)+0)=0 传递（第8、10行）
⑿ S((S0·0)+0)=S0 加S
⒀ ((S0·0)+S0)=S0 传递（第6、12行）
⒁ (S0·S0)=S0 传递（第3、13行）
非法的捷径
一个令人感兴趣的问题是：“怎样为串0=0做一个推导？“看起来，要走的路线显然会是先推出串a:a=a，然后用特称。那么，下面这个a:a=a的”推导”怎么样…有什么问题吗？你能把它修补好吗？
(1) a:(a+0)=a 公理2
(2) a:a=(a+0) 对称
(3) a:a=a 传递（第2，1行）
我用这个小小的练习来指出一个简单的事实：在变换熟悉的符号（诸如”=“）时，不要跳得太快。你必须遵循规则，而不是你关于符号的被动意义的知识。当然，后一种知识在指引一个推导该走什么路线时是极有价值的。
为什么对特称和概括要加限制
现在让我们来看为什么对特称和概括二者都有加限制的必要性。下面有两个推导，两者当中都有一个限制被违反了。看看由此产生的灾难性后果：
(1) ［ 推入
(2) a=0 前提
(3) a:a=0 概括（错了）
(4) Sa=0 特称
(5) ] 弹出
(6) ＜a=0Sa=0＞ 幻想规则
(7) a:＜a=0Sa=0＞ 概括
(8) ＜0=0S0=0＞ 特称
(9) =0 以前的定理
(10) S0=0 分离（第9，8行）
这是第一个灾难。另一个灾难是由于用错了特称而产生的。
(1) a:a=a 以前的定理
(2) Sa=Sa 特称
(3) b:b=Sa 存在
(4) a:b:b=Sa 概括
(5) Sa=Sa 特称（错了！）
因此，现在我们看到，为什么那些限制是必要的。
这里有一个简单的谜题：把皮亚诺的第四条公设翻译成为TNT记法（如果你还不曾这样做的话），然后把这个串当作一个定理而推导出来。
少了什么东西
现在，如果你用迄今所介绍过的TNT规则和公理四处试一会儿的话，你将发现，你可以产生出如下的定理金字塔（这是一个串的集合，所有这些串都是从同一个模子里翻铸出来的，相互之间仅有的不同是填在里边的数字分别为0、S0、SS0等等）；
(0+S0) = S0
(0+SS0) = SS0
(0+SSS0) = SSS0
(0+SSSS0) = SSSS0
事实上，这个塔中的每个定理都能从恰在它之上的那个定理中推出来，只需一两步。因此它是一种定理的”多级瀑布”，每一级触发下一级（这些定理很容易让人想起pq系统中的定理，在那里，左端和右端的短杠组是同时增长的）。
这里有一个我们能很容易地写下来的串，它概括地说出了它们作为整体时的被动意义。这个全称量化了的概述串是：
a:(0+a)=a
用迄今为止所给出的规则，这个串还产生不出来。你若不信，可以自己试试。
你可能会认为，用如下的规则，我们立刻就可以扭转这个局面：
（草拟的）全规则：如果在一个金字塔中的所有的串都是定理，那么，用来概述它们的全称量化的串同样也是定理。
这条规则的问题是：它不能在J方式下使用。只有从外部对系统进行考察的人，才有可能知道串的一个无穷集合全都是定理。因此这不是一条可以安放到形式系统里去的规则。
ω不完全系统与不可判定串
于是我们发现我们处于奇怪的境地：我们能印符地产生关于任何特定的数之间相加的定理，但是像上面那样的一般地表达了加法性质的串，虽然那么简单明了，却不是一个定理。你可能觉得这并不那么奇怪，因为在pq系统里我们曾恰好就处于这种情境中。但是，pq系统并没有声称它该做到什么；并且，事实上，用它的符号体系也的确无法表示加法的一般性质，更不用说证明它们了。pq系统根本没有这样的装备，我们因而也就没想过那是它的缺陷。但在这里，表示能力要远远强得多了，所以我们相应地对TNT比对pq系统有更高的期望。如果上述的串不是一个定理，那么我们就有充分的理由认为TNT是有缺陷的。事实上，有一个名字是专为带有这种类型缺陷的系统准备的------称为”ω不完全性”（所谓”ω”------“欧米伽”------来自于这样的事实：自然数的全体有时候被记作”ω”）。下面是精确的定义：
一个系统是ω不完全的，如果在一个金字塔中的所有串都是定理，而全称量化的概述串却不是一个定理。
顺带地，上述概述串的否定------
～a:(0+a)=a
------也不是TNT的定理。这意味着，原先的那个串在系统里是不可判定的。如果两者之一是定理，那么我们就说它是可判定的。虽然这听起来像是个神秘的术语，但一个给定的系统中的不可判定性是没有什么神秘的。它仅仅是该系统还能够扩充的一个标志。举例来说，在绝对几何学里，欧几里德的第五条公设是不可判定的。它必须作为一条特别的几何公设加进来，从而导致欧几里德几何学；或者相反，它的否定是能够加进来的，从而导致非欧几里德几何学。如果你回想一下几何学，你会记起为什么会出这种稀奇古怪的事情。这就是因为绝对几何学的四条公设没有固定住”点”和”线”这些术语的意义，从而为这些概念具有不同外延留下了余地。欧几里德几何学的点和线提供了”点”和”线”这些概念的一种外延；非欧几里德几何学的点和线则是提供另一种。然而，两千年来，使用先入为主的词”点”和”线”则使人相信那些词必须是单值的，只能有一个意义。
非欧几里德TNT
我们现在就TNT而言面临着一个类似的情况。我们曾沿用的记号使我们带上了某些成见。例如，使用符号”+“就使我们很容易地想：每个里面带有一个加号的定理都应该是在说那个已知的、熟悉的、“可感知”的、我们称为”加法”的运算的事情。因此，如果我们提出增加一个如下的”第六公理”，会让人觉得很是格格不入：
～a:(0+a)=a
这与我们关于加法所持的观念不相适应。但这是我们迄今为止所描述的TNT的一个可能的扩充。采用它为其第六公理所得到的系统是一个一致的系统，就是说，不会同时有两个形式为x和～x的公式都是定理。然而，当你把这条”第六公理”与前面列出来的那个定理的金字塔并置在一起时，你也许会由于那个塔和这条新的公理之间的似乎不一致而感到困惑。但是，这种不一致性不像另一种（在那里x和～x二者都是定理）那么有害。事实上，这并非一个真正的不一致，因为存在有一种解释符号的方法，使每样事情结果都是顺理成章的。
ω不一致性与不一致性不是一回事
这种不一致性的产生是由于下面两件事的对立：（1）一个由一些定理组成的金字塔，它们集合起来断言所有的自然数具有某种性质，与（2）一个单个的定理，它看上去是断言并非所有的自然数具有该性质。我们称这种不一致性为ω不一致性。一个ω不一致的系统更像一个被人们”初拒后纳的”非欧几里德几何。为了能对这些东西形成一个心智上的模型，读者得想象存在有一些”额外的”，未曾料到的数------让我们不称它们为”自然”的，而称它们为”超自然”的数------它们都不具有相应的数字。因此，有关它们的事实不能在金字塔里表示出来。（这有一点像阿基里斯对造物神的想象------是一种”超神怪”，一种比任何神怪都大的东西。这曾遭到怪物的嘲笑，但这是一个合理的想象，并可以帮助你去想象超自然数）。
这就告诉了我们：迄今所介绍的TNT的公理和规则并没有完全固定住对TNT符号的解释。在一个人的心智模型中这些符号代表什么概念，这仍然还有种种变化的余地。这种种可能的外延中的每一个，都可以进一步固定住其中的某些概念，只是以不同的方式而已。如果我们加上上面的那个”第六公理”，那么哪些符号会带上被人们所”初拒”的那种被动意义？是所有这些符号都会染上，还是它们中的一些仍然会代表我们想让它们去代表的意义？我将让读者去考虑这个问题。在第十四章里我们会碰到一个类似的问题，然后再来讨论这件事。总而言之，我们现在不沿着这个扩充走，而是继续尝试去修补TNT的ω不完全性。
最后一条规则
“全规则”的问题是：它要求知道一个无穷高的金字塔中所有的行都是定理------这对一个有穷的主体来说是要求得太多了。但是让我们假设这个塔的每一行都能够用某种模式化的方法从它的前一行推出来。这样就能用一个有穷的推理去说明在塔里的所有的串都是定理。于是，技巧仅在于去找出造成多级瀑布的那个模式，并证明那个模式本身就是一个定理。这就像是去证明每个神怪递送一个信息给它的元，正如机关里的层层上报那样。留待证明的另一件事情即为，是怪物最先引发了这个信息多级瀑布------也就是说，要确定金字塔的第一行是一个定理。这样你就知道了造物神将得到这个信息！
在我们谈过的那个特定的金字塔里有一个模式，可以从下面的推导中的4-9行获得。
(1) a:b:(a+Sb)=S(a+b) 公理3
(2) b:(0+Sb)=S(0+b) 特称
(3) (0+Sb)=S(0+b) 特称
(4) [ 推入
(5) (0+b)=b 前提
(6) S(0+b)=Sb 加S
(7) (0+Sb)=S(0+b) 把第3行搬入
(8) (0+Sb)=Sb 传递
(9) ] 弹出
前提是(0+b)=b，结果是(0+Sb)=Sb。
金字塔的第一行也是一个定理，它直接从公理2就可以得到。现在我们所需要的全部东西就只是一个规则，它能使我们推出那个概述了整个金字塔的串本身也是个定理。这样的一条规则将是皮亚诺第五公设的形式化陈述。
为了表达这个规则，我们需要几个记号。我们用如下的记号来简写一个带自由变元a的良构公式：
X{a}
（可能还会有其它的自由变元，但那与此不相干。）另外用记号X{Sa/a}来代表该串中a的每个出现都被Sa替换后得到的结果。类似地，X{0/a}代表这个串中a的每一个出现都已被0所替换。
一个具体的例子是令X{a}代表要考察的串：(0+a)=a。于是X{Sa/a}就表示串(0+Sa)=Sa，而X{0/a}就表示(0+0)=0。（提醒：这种记号不是TNT的组成部分，只是为了我们在谈论TNT时方便而采用的。）
有了这新的记号，我们就能很精确地叙述TNT的最后一条规则了：
归纳规则：设u是一个变元，X{u}是一个u在其中自由出现的良构公式。如果u:＜X{u}X{Su/u}＞以及X{0/u}二者都是定理，那么u:X{u}也是一个定理。
把皮亚诺第五公设纳入TNT里来的努力最多也就能做到这个地步。现在让我们用它来证明a:(0+a)=a的确是一个TNT定理。我们先用幻想规则从上面推导中的那个幻想里出来，得到：
(10) ＜(0+b)=b(0+Sb)=Sb＞ 幻想规则
⑾ b:＜(0+b)=b(0+Sb)-Sb＞ 概括
这是归纳规则要求输入的两个定理之中的一个。另一个所要求的是金字塔的第一行，这是我们已经有了的。因此，我们可以应用归纳规则，去推演我们所想要的东西：
b:(0+b)=b
特称和概括将允许我们把变元从b改为a，于是a:(0+a)=a就不再是TNT的一个不可判定串了。
一个长推导
现在我想介绍一个TNT中较长的推导，以便你能够看到这种推导是什么样的。这个推导证明了一个虽然简单，但却是很重要的数论事实。
(1) a:b:(a+Sb)=S(a+b) 公理3
(2) b:(d+Sb)=S(d+b) 特称
(3) (d+SSc)=S(d+Sc) 特称
(4) b:(Sd+Sb)=S(Sd+b) 特称(第1行)
(5) (Sd+Sc)=S(Sd+c) 特称
(6) S(Sd+c)=(Sd+Sc) 对称
(7) [ 推入
(8) d:(d+Sc)=(Sd+c) 前提
(9) (d+Sc)=(Sd+c) 特称
(10) S(d+Sc)=S(Sd+c) 加S
(11) (d+SSc)=S(d+Sc) 把3搬入
(12) (d+SSc)=S(Sd+c) 传递
(13) S(Sd+c)=(Sd+Sc) 把6搬入
(14) (d+SSc)=(Sd+Sc) 传递
(15) d:(d+SSc)=(Sd+Sc) 概括
(16) ] 弹出
(17) ＜d:(d+Sc)=(Sd+c)\rightarrow$$\foralld:(d+SSc)=(Sd+Sc) 幻想规则
(18) c:＜d:(d+Sc)=(Sd+c)\rightarrow$$\foralld:(d+SSc)=(Sd+Sc) 概括
(19) (d+S0)=S(d+0) 特称(第2行)
(20) a:(a+0)=a 公理1
(21) (d+0)=d 特称
(22) S(d+0)=Sd 加S
(23) (d+S0)=Sd 传递(19、22行)
(24) (Sd+0)=Sd 特称(第20行)
(25) Sd=(Sd+0) 对称
(26) (d+S0)=(Sd+0) 传递(第23、25行)
(27) d:(d+S0)=(Sd+0) 概括
(28) c:d:(d+Sc)=(Sd+c) 归纳(18、27行)
(29) b:(c+Sb)=S(c+b) 特称(第1行)
(30) (c+Sd)=S(c+d) 特称
(31) b:(d+Sb)=S(d+b) 特称(第1行)
(32) (d+Sc)=S(d+c) 特称
(33) S(d+c)=(d+Sc) 对称
(34) d:(d+Sc)=(Sd+c) 特称(第28行)
(35) (d+Sc)=(Sd+c) 特称
(36) [ 推入
(37) c:(c+d)=(d+c) 前提
(38) (c+d)=(d+c) 特称
(39) S(c+d)=S(d+c) 加S
(40) (c+Sd)=S(c+d) 把30搬入
(41) (c+Sd)=S(d+c) 传递
(42) S(d+c)=(d+Sc) 把33搬入
(43) (c+Sd)=(d+Sc) 传递
(44) (d+Sc)=(Sd+c) 把35搬入
(45) (c+Sd)=(Sd+c) 传递
(46) c:(c+Sd)=(Sd+c) 概括
(47) ] 弹出
(48) ＜c:(c+d)=(d+c)\rightarrow$$\forallc:(c+Sd)=(Sd+c)＞ 幻想规则
(49) d:＜c:(c+d)=(d+c)\rightarrow$$\forallc:(c+Sd)=(Sd+c)＞ 概括
(50) (c+0)=c 特称(第20行)
(51) a:(0+a)=a 已有的定理
(52) (0+c)=c 特称
(53) c=(0+c) 对称
(54) (c+0)=(0+c) 传递(50、53行)
(55) c:(c+0)=(0+c) 概括
(56) d:c:(c+d)=(d+c) 归纳(49、55行)
TNT中的紧张与解决
TNT证明了加法的可交换性。即便你还没有完全弄清上面这个推导的每个细节，能体会到它有着自己的自然”节拍”，像一首乐曲那样，也是很重要的。它可不只是个随意的漫步，碰巧到了我们所希望得到的那最后一行。我插进了”呼吸记号”来显示这个推导的某些”乐段”。特别是第28行，它是这个推导里的转折点，就像某种在AABB式乐曲里的中途点似的东西，在这一点上，你获得了暂时的解决，即使不是在主调上。这样的重要的中间阶段常常被称作”引理”。
很容易想象，当一个读者从这个推导的第1行开始时，并不清楚它会在哪儿结束。他每新看到一行时，都会对它的进一步走向有所感觉。这就建立了一个内部的紧张，很像在一首乐曲中由于和声的模进所引起的紧张，你知道这调性是什么，但还未解决。到了第28行时，读者的直觉得到了肯定，他有了一种暂时的满意感，同时也增强了他的信心，去向着他认为是真正的目标前进。
第49行是一个极为重要的紧张增长因素，因为它引起了”就在那里”的感觉。在那里停下会使人感到极度的不舒服！从那儿往下，事情的发展几乎都是可以预计的了。但是你不会希望一首乐曲停止在最后的解决刚开始出现的地方，让你去想象它的结尾------你希望听到那个结尾。在这里也类似，我们必须把事情进行到底。第55行是不可避免的，它建立了最后的全部紧张，它们在第56行得到了解决。
这不仅是形式推导的典型结构，也是非形式证明的典型结构。数学家对紧张的认识是和他对美的认识密切相关的，并且正是这种东西使得数学值得花力气去做。但要注意，就TNT本身而言，似乎对这些紧张没有任何反映。换句话说，TNT并没有将紧张和解决、目标和子目标、“自然性”和”被迫性”等概念形式化，正像一首乐曲并不是一本讲和声和节拍的书一样。人们能不能发明出更为奇妙的印符系统，以感知推导中的紧张与目标呢？
形式推理之别于非形式推理
我很愿意演示一下如何用TNT去推导欧几里德定理（素数有无穷多），但这大概会使这本书的长度加倍。有了前面那条定理，下一步该做的自然是去证明加法的结合律、乘法的交换律和结合律、以及乘法对加法的分配律。这些将为我们的工作提供一个强有力的基础。
按照到目前为止所描述的，TNT已经达到了”临界质量”（这个隐喻用在叫”TNT”的东西上或许有点奇怪）。它和《数学原理》的系统有同样的能力。用TNT，人们可以证明在一篇标准的关于数论的专门论文中所能找到的每一个定理。当然，没有人会主张在TNT中推导定理是做数论研究的最好方法。那种想法相当于认为要想知道1000×1000是多少，最好的方法是去画一个横竖各1000道的网格，然后再去一个一个地数里面一共有多少小方块…不是这样的。在进行了彻底形式化之后，唯一可行的道路就是放松形式化原则。否则，形式系统会过于庞大而笨重，以至于对任何实际的目的而言都是毫无用处的。所以，把TNT嵌进一个更广阔的语境中是很重要的，这个语境能容许导出新的推理规则，从而能够加速推导过程。这就需要对用来表示推理规则的语言进行形式化------也即，对元语言作形式化。这样下去可以走得相当远。然而，这样的加速技巧并不能使TNT更强一点，只不过是使它更好用一些罢了。理由很简单，我们实际上已经把数论专家所借助的每个思维模式都放进了TNT。把它嵌入愈来愈大的语境并不能扩大定理的空间，只能是使得在TNT里面------或者说在每个”新的，改进的版本”里面------进行工作时，更像是在进行传统的数论工作。
数论专家赋闲
假定你事先不知道TNT会是个不完全的系统，而期望它是完全的------就是说，每个用TNT记法可表达的真陈述都是定理。在这种情况下，你就能为数论的一切东西造一个判定过程。方法很简单：如果你想知道N中的语句X是真还是假，就把它翻成TNT句子x。于是，如果X为真，完全性就说，x是一个定理；反过来，如果非X为真，那么完全性就说，～x是一个定理。因此，x和～x二者必有一个是定理，因为不是X为真，就是非X为真。现在让我们来系统地枚举TNT的定理，就用我们曾经对WJU系统和pq系统所用过的那种方法。过不一会儿，你就一定会到达x或者～x，而不管你碰上了哪一个，它都会告诉你X和非X之中哪一个为真（弄清楚这个论证了吗？关键的一点是能在心里区分开形式系统TNT与它的非形式对应物N。一定要确实弄清这个论证）。这样，从原则上说，如果TNT是完全的，数论专家就得赋闲了：只要有足够的时间，他们领域里的任何问题都能够用纯粹机械的方法解决。现在我们知道这是不可能的。至于这究竟是该为之庆贺还是为之悲伤，就全看你的观点如何了。
希尔伯特方案
本章我们要处理的最后一个问题是：我们该不该像信赖命题演算的一致性那样信赖TNT的一致性；以及，如果我们不那么信赖TNT，是不是有可能通过证明它是一致的，来增强我们对它的信任。人们可以像那位”马虎”在论及命题演算时所做的那样，提出同样的关于TNT一致性的”显然性”的那种论述------也就是说，每条规则体现了一个我们所完全信赖的推理原则，因此，对TNT的一致性的疑问就是对我们自己头脑的清醒程度的疑问。在某种程度上，这种论证仍然是有份量的------但不像从前那么有份量了。推理规则实在是太多了，而其中有些也确实有点”不对头”。更进一步，我们怎么知道这种称为”自然数”的抽象实体在我们心里的模型实际上是一个前后一致的结构呢？说不定，我们自己的思维过程，那些我们试着用形式系统中的形式规则来把握的非形式过程，它们本身就是不一致的！这当然不是我们所期望的事情，但是，我们的思维也可能使我们误入歧途，这是越来越可以想象得到的，尤其是当面临的课题很复杂的时候------而自然数决不是什么不足道的简单课题。所以，那位”严谨”所呼吁的关于一致性的一个证明，在这种情况下就必须更为认真地对待。这倒不是我们非常怀疑TNT会是不一致的------但确是有一点儿怀疑，我们心里闪了一下怀疑的影子，而一个证明会有助于消除这种怀疑。
但是，哪些证明手段是我们愿意接受的呢？又一次，我们碰见了不断出现的那个转圈子问题。如果在一个关于我们的系统的证明中，使用那些和我们已经嵌入到系统中的东西完全一样的手段，我们能达到什么目的呢？但如果我们能论证说TNT是一致的，而用的是一个比TNT弱的推理系统，那我们就战胜了那种说我们是在转圈子的反对意见！想一想让一条很粗的绳索飞越两条船之间的办法（大约我还是个孩子的时候读到过的）：先把一支很轻的箭射过这段空间，箭的后面牵引着一条细绳。一旦用这种办法在两条船之间建立起了联结，粗绳子就能被拉过这段空间了。如果我们能用一个”轻的”系统去说明一个”重的”系统是一致的，那么我们就的确做成一些事情了。
初看起来似乎是有一根细绳子。我们的目标是证明TNT具有一个特定的印符性质（一致性），即任何时候都不会有x和～x形式的公式同时都是定理。这类似于努力去说明WU不是WJU系统的一个定理。二者都是关于符号处理系统的印符性质的陈述。认为有一条细绳的观点是基于如下假设的：在证明这样一个印符性质成立时，并不需要有关数论的事实。换句话说，如果没有用到整数的性质------或者仅仅用到了少许极为简单的性质------那么我们就达到目标了：证明了TNT的一致性，而用到的推理手段比TNT自身内部的推理模式弱。
这正是二十世纪初大卫·希尔伯特所领导的数学家和逻辑学家的一个重要学派所持的期望。他们的目标是使用一个非常受限制的推理原则的集合来证明类似于TNT的形式化数论的一致性。这被称为推理的”有穷”方法。这就是细绳。有穷方法中包括了所有的命题推理，即命题演算中所体现的那种，另外还有某些种类的数值推理，但是哥德尔的工作表明，任何用有穷方法这条细绳去牵引TNT一致性这条粗绳的努力都是注定要失败的。哥德尔证明了，要想牵引粗绳，不能用更细的绳子，细绳中没有足够结实的。少来些隐喻，我们可以说：任何一个强得足以证明TNT的一致性的系统起码与TNT本身一样强。从而，转圈子是不可避免的。