公理系统的不可判定命题、相容性和完备性问题是相联的。系统里的命题，如果既不可能证明它成立，也不可能证明与之相反的成立，这便是个不可判定的命题。相容的系统，不可能证明相反的一对命题同时成立。完备的系统，必须能够证明任何一对相反命题，必有一个成立。所以具有不可判定命题的系统，如果是相容的必定是不完备的。

如果在PM里，能构造出这样一个自相矛盾的命题：若证明它成立，等同于证明相反的命题也成立。它就是个不可判定的命题。就证明了“哥德尔不可判定定理”，或者根据上面简单的推论就有“哥德尔不完备性定理”。

“这个命题是不可证明的”这句话，如果能放在PM里，它便在证明时自相矛盾。但这句话是元数学的命题。我们必须用一个映射，将这命题变换成PM里自涉的（self-referent）算术命题。歌德尔先用编码将PM里的公式一一映射成自然数（哥德尔数），这个数就好比是身份证的号码，唯一代表着那个公式，从公式角度来看这个数就是它自己。这个公式里如果包含了这个数和它的含义，就能够谈论自己。这一篇介绍这个哥德尔编码。

前面说过，形式公理系统里的公式是由一组原始字符，按照形成规则构成的字符串，编码就是将字符串一一映射成一个自然数，称为哥德尔数。我们来看哥德尔是怎么编码的（这基本按哥德尔1931年论文的版本）。

包含着皮亚诺算术公理的形式公理系统PM，有12个固定符号，分别对应着哥德尔数如下：

公式在表中符号的含义解释下，具有逻辑和数学命题的含义，哥德尔“对应引理”证明了PM中原本只具有形式的定理，对应着其数学含义下的数论真理。不难看出，如果不再定义数字符号，n个S的字符串SSS…SSS0的含义是自然数n，这字符串称为数n在PM的表达。

继续说编码的规则。自然数变量x，y，z，…的哥德尔数分别是13，17，19，…依序对应着大于12的质数。命题变量p，q，r，…的哥德尔数是13²，17²，19²，…依序对应着大于12的质数的平方。谓词变量P，Q，R，…的哥德尔数是13³，17³，19³，…依序对应着大于12的质数的立方。

公式的编码是一组质数幂的乘积，这组质数的个数与公式中的字符数相等，从2开始依序列出前几个的质数，它的指数对应着相应位置上公式符号的哥德尔数。举例来说：

公式“∃x(x=Sy)”这里8个字符对应的哥德尔数依序是4，13，8，13，5，7，17，9，这公式的哥德尔数按照编码规则便是2⁴3¹³5⁸7¹³11⁵13⁷17¹⁷19⁹，它是一个很大的自然数。

形式证明是由几个公式组成的序列，序列中每一个公式如果不是公理或已知的定理，都必须是由序列里前面的公式按变换规则生成的，证明的结果是序列中最后一个公式。形式证明的编码也与公式的编码规则类似，只不过其指数是对应着次序上公式的哥德尔数，举例来说：

从“每个数有个后继数”用替换规则证明“零有一个后继数”，可以表示为两个公式的序列：“∃x(x=Sy)；∃x(x=S0)”第一个公式的哥德尔数为m，第二个为n时，这个形式证明的哥德尔数是：2^m3ⁿ，也是一个自然数。更细致的解释见内格尔和纽曼《哥德尔证明》【1】。

按照这样的编码，每一个公式或证明对应着一个哥德尔数。根据算术基本定理，每一个自然数可以分解成唯一的质数幂的乘积，依照质数指定的位置和其指数对应的字符或公式，哥德尔数可以解码出对应的公式或证明。这个编码规则建立起公式或证明，与（一部分）自然数的一一映射。每个哥德尔数通过这个一一映射，拥有它所对应字符串的信息。

既然公式和证明的所有信息都在对应的哥德尔数上，那么讨论公式和证明，这些谈论字符串性质的元数学问题，便是一个数论的命题，就可能把它用公式表达出来【2】。比如一个元数学的命题说：“~(0=S0)”是个否定式的命题。也就是判断它的第一个符号是“~”。这是个用自然语言表达的元数学命题，首先把它转化成数论的命题，然后用PM里的公式来表达。

这个公式的哥德尔数是2¹3⁸5⁶7⁵11⁷13⁶17⁹，符号“~”的哥德尔数是1，公式的第一个符号是“~”，对应着公式的哥德尔数是2的1次方的因子。记这个数为a，那么这个元数学命题对应的数论命题是：“a整除于2，且a不能整除于4。”前面说到，自然数a在PM里表达是有a个S的字符串“SSS…SSS0”，“a整除于2”等价于“存在着一个数x，有a=2·x”，可以表示为：∃x(SSS…SSS0=x·SS0)，这个数论命题不难用PM里的公式表示为：

~(~∃x(SSS…SSS0=x·SS0)V(∃x)(SSS…SSS0=×·SSSS0))；

这个直观的例子显示元数学上的命题，是怎样映射成PM里的公式。

现在考虑证明中要用到的一个重要元数学命题：“公式序列X证明了公式Z”。我们知道在形式证明的公式序列里的公式有个的顺序规则，与公理、已知的定理、变换规则及被证明公式的对应有关。所谓的“证明”就是有限次地从前面的公式递推出后面的公式，这叫做递归。将公式对应成数后，“证明”就是这些数间的递归函数。假定公式序列X的哥德尔数是x，公式Z的哥德尔数是z。从这些关系不难想象出自然数x和z之间的算术关系，将这个算术关系记为“dem(x, z)”。

哥德尔在论文中用了极大的努力证明了这个dem(x,z)是数x和z之间的“原始递归关系”，所以它可以形式地表示成一个PM的公式【2】，记为“Dem(x, z)”。我们已经将元数学的命题“X证明了Z”，映射成PM的公式Dem(x, z)。这完成了这一篇文章的目标。

学习计算机的读者可能疑惑，为什么要这么麻烦地编码？这质疑有道理。哥德尔证明这个定理时在1931年，那时候还没有计算机，哥德尔在编码、递归函数、可表达性等问题上都做了开创性的贡献。这里介绍哥德尔编码，是沿着哥德尔原来证明的轨迹，了解这个经常会被人们提及的内容。现代的计算机实践经验，已经在人们头脑里形成了新的直观，对计算机理论有更多了解的，更能落实到这些直观背后充分的理论根据。有了这些直观，理解这些就很容易了。PM里的公式和证明，可以用任何一种编码（比如说Unicode）变成0和1的字符串，也就是一个自然数了。这个自然数也可以通过解码得出原来的公式和证明。这就建立起一一映射。这时候同样可以通过递归函数理论，将上述的“证明”语句表达为PM里的公式Dem(x, z)。也可以想象写一个程序，解码自然数x得出一个公式序列来，然后验证这序列是可以递推出自然数z解码所得的公式，把这个程序用PM里形式语言写出来，便是个PM里的公式。

总之，我们可以把“X证明了Z”，映射成PM的公式Dem(x, z)。注意，表示式“Dem(x,z)”实际上不是PM里的式子，它只是一个方便的记号，联系了两个哥德尔数的变量x和z在一个公式里，我们用来代表PM里那个非常长的公式。

怎么在这个Dem(x, z)代表的公式里做到自我纠缠，这个技巧将在下一篇的核心证明里介绍。

（待续）

【参考资料】

【1】内格尔和纽曼《哥德尔证明》（中文版下载，谢谢徐晓）http://bbs.sciencenet.cn/home.php?mod=attachment&id=32962

【2】数论中有不可数多的命题，而PM只能有可数个式子，所以并非所有的数论命题都能表达成PM里的公式。哥德尔证明了原始递归函数可以表达成PM里的公式。