哥德尔要在形式公理系统里，放进一个“自我纠缠”的魔鬼，用系统里的公式表达“这个公式是不可证明的”含义，构造一个不可判定的命题。如果他做到了，这系统若是相容的就是不完备的（这不难推出，读者可以想一想）。他的想法来自于法国数学家理查德（Jules Richard）1905年的语义悖论。理查德悖论【1】【2】的一个变种是这样的：

用语言描述一类自然数的算术性质。模仿公理化的方法，从基本概念开始，依定义过的内容来描述新的定义。这些定义的内容总是用有限个字符来表达。比如说，定义了整数，乘除法后，定义“（平方数）是某个整数的自乘”，“（质数）是只能被1和自己整除的数”等等。把这些定义按描述句子的长短和字典顺序排列成一个表，这里每一个定义，在表中的序号是一个自然数。例如“（质数）是只能被1和自己整除的数”的序号是19，“（平方数）是某个整数的自乘”的序号是50。对照定义和它的序号，不外乎有两种情况：一类是这序号恰好符合定义的描述，例如序号19（它是质数，有定义的性质）；另一类是这序号不具有定义性质的情况，例如50（不是平方数，没这性质），将这些不具有定义性质序号的数定义为“理查德数”。这样50是理查德数，19则不是。理查德数是在这系统中有明确数学性质定义的一类自然数，它的定义也可以在这表中，假设它的定义对应着序号n。问：n是不是理查德数？论证一下，若n不符合它所对应的定义，按照理查德数定义的描述，n应该是理查德数，这是说n是符合理查德数定义了，即n符合它所标号的定义，这就和初始的假设矛盾了。

这个悖论说明：即使对自然数的算术性质，用任何语言（包括形式语言）来定义，也可能发生矛盾。这悖论有些疵瑕，但即使这个表长有限，矛盾仍在。重点是它与1901年的罗素悖论有着相同的逻辑结构——self-reference，而罗素悖论与谎言悖论都是因为自我纠缠惹得祸。

罗素和一些人认为：如果把对象语言和讨论对象语言的“元语言”区分开来，就可以避免这个纠缠。谎言悖论“这句话是错的。”在区分后就有了两层的意思，一个是用对象语言表达的语句，另一个是从元语言角度来讨论用对象语言表达的语义，在各自层次里都是一个简单的陈述。从元语言层次，这句话的含义，是评判句中“这句话”，指的是对象语言层次的句子错了，对象语言层次的句子不能评价元语言层次的句子，这就避免了纠缠引起的矛盾。

对于理查德悖论，分清层次后，按照算术的性质描述自然数，只能采用算术公理和算术运算的性质，理查德数的定义采用了有关算术性质的讨论，系统序号数和对应定义间的关系，这属于讨论数学性质的“元数学”（Metamathematics）【3】，不是数学层次的语言，所以它不应该出现在这表中。规定它们不能混在一起，就杜绝了这个悖论。

在PM里，用公理、定义和逻辑符号构成字符串的式子描写了数学，对于这些数学性质的讨论，即对于这些字符串的讨论，诸如“这个命题是否定式的”，“字符串x是字符串z的证明”，“z是不可证明的”，“PM是相容的”等等，则属于元数学的范畴。

希尔伯特用精确的形式语言构建的形式公理系统，已经严格区分数学和元数学，建立起隔离墙，堵塞了这个漏洞。

哥德尔要把“这个公式是不可证明的”的句子放在系统里，就必须绕过这堵墙，将这元数学的句子转换成数学和逻辑的式子。我们来看这该怎么设计。

首先要了解什么是PM中合法的式子。它是按一种形式语言写的字符串。写过计算机程序的人应该不难理解，因为Basic，C，Java等等，所有计算机语言都是形式语言。

希尔伯特的形式公理系统里的式子，是按照《数学原理》的思想，用很基本一阶谓词逻辑的形式言语来写的字符串。系统根据演绎规则来操作这个形式语言的字符串。

命题逻辑内容大家中学时都学过。谓词逻辑是命题逻辑的推广，在命题中可以带有变量，用谓词表述变量代表个体的性质和关系，可以用量词来约束变量，比如说，“存在一个数x，x的自乘等于4”，这里x是变量，“存在一个数”是量词，“的自乘等于4”叫谓词，表达成式子是“∃x(x·x=SSSS0)”，（SSSS0是数4在系统里的表达），只包含个体谓词和个体量词的谓词逻辑称为一阶谓词逻辑，简称一阶逻辑。包含PA的一阶逻辑系统称为一阶算术系统。这个大致的解释，让不熟悉数理逻辑的读者能够想象这些术语。下面假设读者已经有了数理逻辑的基本知识，这里通俗地介绍后面要用到一些术语和例子。这些式子只是作为例子，不必记忆。有数理逻辑知识的读者应该熟悉这些内容。不熟悉的，简单接受用字符串可以表达算术命题的事实，了解式子的含义和这些术语，可以略过其他的细节。读懂这系列科普只需要看懂这些式子表达的意思就行，不需要有深入的知识。（关于数理逻辑的简介见【4】，详细可看任何教科书有关“一阶谓词逻辑”部分。）

在这个系统中首先给出一些原始符号，PM包含12个固定符号：～ V →∃ = 0 S （），+ ·和数字变量x，y，…，命题变量p，q，…，谓词变量P，Q，…等等，以及式子形成规则（syntax），说明怎么组成合格的字符串。这些符合语法规则的字符串，称之为“公式”，如：“~(0=S0)”。系统中有一组初始的公式，称之为“公理”，两条变换规则：将公式代入变量的替换规则和三段论推理的分离规则，称之为“变换规则”。好比计算机解读程序产生输出的规则。由几个公式应用变换规则产生的字符串，也是个公式。若是从公理（和已知的定理）开始，由有限次演绎产生的公式，则称为“定理”，这个过程称为“形式证明”，简称为“证明”。这里的定理可能很平凡，只要能被形式证明的都是。

PM里有4个逻辑公理

pVp → p； p → pVq； pVq → qVp； (p → q) → (rVp → rVq)；

将这里的的“V”解释成逻辑上的“与”，“→”为“推出”，容易理解这些都是逻辑的规则。它们和变换规则一起，形成逻辑推理能力。

皮亚诺算术（PA）的公理可以表达为下面6个数字公理和一个数学归纳法公理（见【5】）。

~(0=Sx)；Sx=Sy → x=y；x+0=x；x+Sy=S(x+y)；x·0=0；x·Sy=x·y+x；

将这里的“～”解释为“否定”，“∃”为“存在一个”，“Sx”为变量x所表示的数的直接后继数，（想象x+1），其他的按算术中符号的约定，很容易理解这6个公理的含义。但这些含义只是便于理解的手段。形式公理系统不需要理解这些含义来演算，在这个系统中，只需要把这些公式看成没有意义的字符串，按照变换规则来得出新的字符串，进行形式性的运算。这些字符串并不代表着客观世界的事物，没有真假可言，这就是“形式”的意思。

形式公理系统可以操作没有含义的字符串，但是公理集合可以赋予这些字符串要描述对象的一种含义，这含义不被用在字符串的运算操作上，而建立起称为定理的字符串和描述对象真理间的一一对应关系。公式具有逻辑命题含义时称为命题，便有了真假之分，当公理被认为是真的，定理便是逻辑为真的命题。一个命题在系统内被证明，即被认为是真的，也就成为了定理。哥德尔1931年论文的命题V中，证明了存在着一个PM定理组成的无穷集合，其中每一条定理如果按照上面对于这些符号的解释，都表达了一条算术的真理；反之，有个算术真理的无穷集合（属于“原始递归的”，想象所有可以通过有限次算术运算的结果，它包括加法，乘法计算结果，判断质数等命题），如果这些真理按照上面符号含义的解释表达成公式，这些公式都是PM的定理。这种无穷多个对应关系，让你相信这字符串的确实具有那种被原始符号和逻辑定义解释的含义。这个哥德尔关键性的结论称为“对应引理”，它建立起PM定理和数论真理的对应关系。

形式公理系统不需要依赖含义可以独立存在和演算，但含义的对应让它易于理解和应用。以后我们在不会混淆时，有时用含义来形容它所对应的那个公式。

我们现在已经了解了什么是PM的公式和它的算术含义。要把讨论PM的元数学命题，变成PM里的命题，就需要建立起一个映射关系，把这个元数学的问题变成算术问题，然后应用“对应引理”表达为PM的公式。这就可以把纠缠的魔鬼引进防卫严密的PM殿堂。哥德尔用逻辑推理和算术运算间的一个对应，设计了这个映射。这便是“哥德尔编码”。

（待续）

【参考资料】

【1】      维基百科，理查德悖论http://zh.wikipedia.org/wiki/%E7%90%86%E6%9F%A5%E5%BE%B7%E6%82%96%E8%AE%BA

【2】      Wikipedia，Richard’sparadox  http://en.wikipedia.org/wiki/Richard's_paradox

【3】      Wikipedia，Metamathematics  http://en.wikipedia.org/wiki/Metamathematics

【4】      白冰博文，[转载]数理逻辑、谓词逻辑、一阶逻辑和公理系统http://blog.sciencenet.cn/blog-58025-573028.html

【5】      Wikipedia，Peano axiomshttp://en.wikipedia.org/wiki/Peano_axioms