这篇介绍哥德尔证明的核心逻辑。你需要的不再是补充知识，而是澄明心思，清晰头脑，来跟上证明的思路。

哥德尔有一套计算可形式化的“原始递归函数”理论，将元数学里的命题：“哥德尔数为x的公式序列，是哥德尔数为z公式的形式证明”，对应着算术计算，映射成PM里的公式。这个带有自然数变量x和z的公式简记为Dem(x, z)。

PM里的公式原来只是无意义的字符串，无关真假，能够用演绎规则，从公理和其他定理产生出来的公式，称为定理，这个过程称为形式证明。将一些符号解释成逻辑关系，赋予公理真值，一些公式便有了逻辑的含义，称为命题，定理便是逻辑上为真的命题。将一些符号解释为算术符号，哥德尔的“对应引理”通过PA公理，建立起数论真理和算术命题的对应关系，因此赋予了这些公式的数学含义。元数学是在PM上层谈论公式性质和关系的语言。

这里将不时地在元数学和PM两边说道、对应，你必须留意这一点，才不会被绕晕了。以后除非强调，元数学命题里谈到“证明”都是指在PM里的形式证明，有时也略去哥德尔数对应的说明，简略地说成：“x是z的证明”。这两个范畴间命题间的映射是形式与语义间的关系，对两边相同的逻辑运算保持着形式和语义的对应关系。

哥德尔用Dem(x, z)，构造一个PM的公式G，它表达元数学的命题“公式G在PM内是不能被形式证明的。”

在构造新公式前，还需要介绍一个关于哥德尔数的函数表达式。假如在哥德尔数为k的公式中，有个自然数变量y（哥德尔数是17），将自然数k的PM表达（SSS…SSS0）代入这公式中所有y变量出现的地方，这个新公式的哥德尔数记为sub(k, 17, k)。

哥德尔努力显示这个置换操作是可计算的，sub(k,17, k)是原始递归函数，它对应的PM字符串的表达式，记为Sub(k, 17, k)。比如说k对应的公式是“∃x(x=Sy)”，代入后的新公式Sub(k, 17, k)是“∃x(x=SSSS…SSS0)”（这里SSSS…SSS0有k+1个S），它的哥德尔数是sub(k, 17, k)。

在Dem(x, z) 前加一个存在的量词(∃x)Dem(x, z)，对应着元数学里“存在着一个x，它是z的证明”，简言之，“z是可证的”。其否定式 ~(∃x)Dem(x, z) 对应着“z是不可证的”。

将哥德尔数函数sub(y, 17, y) 代入~(∃x)Dem(x, z)中的z，有

公式1           ~(∃x)Dem(x, Sub(y, 17, y))

这PM公式直接的含义是数学命题：“不存在着一个哥德尔数x，它满足dem(x, sub(y, 17,y))的算术关系。”它对应着元数学里的命题：“哥德尔数为sub(y, 17,y)的公式是不可证的。”

设公式1所对应的哥德尔数是n，这是一个确定的自然数，将它代入公式1的变量y，便有

公式G                   ~(∃x)Dem(x, Sub(n,17, n))

记哥德尔数g = sub(n, 17,n)，这也是一个确定的自然数。公式G对应着元数学里的命题：“哥德尔数为g的公式是不可证明。”

这g对应着哪个公式？sub(n,17,n) 是置换操作后新公式的哥德尔数。这新公式是将哥德尔数为n的公式（即公式1）里的变量y用n代入，这正是公式G！公式G的哥德尔数是g。

因此，公式G对应着元数学里的命题：“公式G是不可证明的。”公式～G即(∃x)Dem(x, Sub(n,17, n)) 则对应着元数学里的命题：“公式G是可证明的。”

我们已经把自我纠缠镶进了公式G！嘘一口气，慢慢消化这个公式和对应的含义。然后往下看这证明的辩驳。如果细心推敲，你可能会有些疑惑，这很正常，需要慢慢消化。哥德尔的证明手法很不寻常。当大数学家冯·诺依曼得知哥德尔证明时大为赞赏，细究之后，两次宣布找出了证明中的错误，后来他又两次修正了自己的错误。他惭愧地看到自己由这个插曲，轻易地改变了关于数学绝对真理的看法，而且相继改变了三次。

哥德尔用反证法证明在PM里，公式G是不可判定的。假如公式G可证，这件事的元数学陈述是：“公式G是可证明的”，~G对应的正是这句话，说明它是可证的。反过来，假如~G是定理，这公式对应的元数学命题“公式G是可证明的”为真，这元数学的判断是：PM里可以证明公式G，即公式G是定理。因此，公式G是定理，当且仅当公式~G是定理。【注】

PM是相容时，这种情况是不允许的，所以上述导致矛盾的假设都不成立。G和~G在PM里都不可证，也就是不可判定的。

G是不可证明的事实，说明元数学描写G的命题是真理，它对应着这公式G的含义为真。PM里一个表达真理的公式G，不能在PM里被证明，说明PM是不完备的。这（在元数学里）就证明了：

定理1：PM如果是相容的（consistent）则是不完备的（incomplete）。

在相容的PM里不可能判定G的真假，所以哥德尔这个定理有时叫做“不可判定定理”。

是不是在PM里加上这个不可判定的命题作为公设，系统扩张后就可以让它完备起来？哥德尔说，这是不可能的！加上新的公理，按照相同的逻辑，还可以证明有新的不可判定的命题。这让公理化的原始设想完全落空。这定理简单的推论是：数论里有无穷多个真理不能用初等方法（数论里的公理和定理）来证明，不断引进数论外的定理后，总是还有不能用形式逻辑证明的数论真理。所以古老数论难题的解决，常常意味着带来新方法的突破。

下面证明：相容性是不可能在PM里证明的。回顾一下“相容性”的含义，它说：系统里一个命题和它的否定不能同时是定理。这是数学系统无矛盾性的要求。如果不是这样，在系统里就可以证明任何的命题成立。所以“相容性”等价于“系统存在着一个命题，它是不可证明的。”

我们构造一个新的公式

公式A                   (∃z)~(∃x)Dem(x, z)

这个公式对应着元数学的直接解读是：“存在着一个公式z，不存在着公式序列x是它的证明”；即“有一个公式，它是不可证明的”，即“PM是相容的”。

公式G是否也有类似的解读呢？它的直接元数学的解读是：“公式G是不可证明的。”，我们已经从元数学证明：命题G是真的。它是真的又不能在PM里证明，这正是“PM是不完备的”的意思。所以，公式G的另一个解读是：“PM是不完备的。”

元数学里的定理1说：如果PM是相容的，则PM是不完备的。对应着PM里的公式：

(∃z)~(∃x)Dem(x, z) → ~(∃x)Dem(x, Sub(n, 17, n))

也就是说，如果我们能够在PM里证明它是相容的，(∃z)~(∃x)Dem(x, z)公式为真，按照上式和PM里三段论推理的分离规则，推出~(∃x)Dem(x, Sub(n,17, n))为真，即在PM里证明了公式G，这与公式G在PM里是不可证的事实相矛盾，所以公式A不能在PM里被证明。

这就有了

定理2：PM不能证明自身的相容性（consistency）。

（待续）

【注】这里沿用了【1】里PM公式与元数学对应关系的简化证明思路。这里的定理1是J Barkley Rosser 1936年证明在相容条件下的较强结果。实际上这不是哥德尔1931年的证明。哥德尔证明的是：如果PM是ω-相容的（ω-consistent），则是不完备的。

“ω-相容的”的定义是：对于算术谓词P，“(∃x)P(x)”和每一个自然数k的“~P(k)”不能同时为真。而“相容的”则是：对于任何命题p和~p 不能同时为真。“ω-相容的”是个较强的要求，它能够推出“相容的”条件。“ω-相容的”的定义里“~(∃x)P(x)”（不存在着一个数有这性质）和每一个自然数k “~P(k)”（每一个自然数都没有这性质）在语义理解上是同一回事，但在形式系统里，因为没有一个能处理无限的规则（希尔伯特计划中有限主义的限制），所以不能把它们看成是一样的。

哥德尔的实际证明逻辑如下。

假设G可证，这说明有个PM公式序列是G的证明，设这个公式序列的哥德尔数为k，这元数学命题对应着数论命题 dem(k, g)，已知g = sub(n, 17, n)，所以有 dem(k, sub(n, 17, n))，它陈述了一个算术的事实，表示为PM的公式 Dem(k, sub(n, 17, n))，这说明它是PM里的定理。有一个具体的数k满足这关系，逻辑上说明存在着一个数x满足这关系，也就是 (∃x)Dem(x, sub(n,17, n)) 能够被证明，这公式是~G。这说明从G可证，可以推出它否定形式~G也可证。从而，如果PM是相容的，G在PM里不可证。

假设~G在PM里可证。如果G不可证，也就是对于所有的k，dem(k, g) 都不是事实的，即~dem(k,sub(n, 17, n))都是真的，所以 ~Dem(k, Sub(n, 17, n)) 对每一个的自然数k都是个定理，~G可证意味着 (∃x)Dem(x, Sub(n, 17, n)) 是PM里的定理，如果PM是ω-相容的，这是不可能的。从而，如果PM是ω-相容的，~G在PM里不可证。

因此，如果PM是ω-相容的，G是不可判定的。不可判定的命题，根据排中律，G和~G必有一真，但在PM里都不能证明它们，所以PM是不完备的。

【参考资料】

【1】      内格尔和纽曼《哥德尔证明》http://bbs.sciencenet.cn/home.php?mod=attachment&id=32962

【2】      哥德尔不完全性定理(朱水林) http://ishare.iask.sina.com.cn/f/23413902.html

【3】      Gödel's proof summary http://www.jamieyorkpress.com/wp-content/uploads/2012/04/G%C3%B6dels-proof-summary.pdf