博文
[转载]来自赵昊彤科学网博客：“哥德尔不完备定理”到底说了些什么？（4 of 5）
||
“哥德尔不完备定理”到底说了些什么？——（四）
|||
“哥德尔不完备定理”到底说了些什么？——（四）
第四重：“目无全牛”——“哥德尔不完备定理”的核心证明过程
哥德尔的核心证明过程是极为严格、缜密的，如果真的把他的核心证明详细阐述一遍，工作量相当于把他的论文翻译五遍以上。本文作为一篇普及性文章，虽然普及的层面越来越深，但是我还是不希望采用这种方法。因此，在不影响读者读懂的前提下，我会尽量略掉一些过于基础且严谨的内容，对由此可能带来的不缜密，希望读者理解。
另外，哥德尔的证明过程花了极大的篇幅来给出基础定义、原始递归的定义、相关引理等，真正到证明不完备定理的时候，反而没有多少篇幅了。因此读者在阅读的时候，如果觉得前面的部分特别是“（一）基本定义”部分过于枯燥，可以在了解情况前提下快速掠过。
最后，哥德尔之所以花费那么多笔墨来阐述这些基础定义，给出“原始递归”的概念，并在论文中表达了46个有含义的公式，其根本目的就是论证我们进行第三重修炼的时候给出的provable（x）是可在PM中表达的，且哥德尔所构造的命题是一条算术命题，恰恰是这个算术命题在PM中是不可证的。这样，哥德尔就避免了别人质疑他所构造的命题其实是一个类似“这不是谎话”的语言悖论。
好，下面开始进入哥德尔证明的详细过程。
（一）基本定义
哥德尔首先给出了PM公理体系的基本常量、变量和公式的定义，然后给出了基本公理组成的公理体系。这部分内容是理解哥德尔核心证明过程的基础。
（1）常量（基础字符）
定义“~”(逻辑非)、“∨”(逻辑或)、“∀”(对于任意)、“0”(数字零)、“succ”(直接后继)、“(”、“)”(左右括号)这7个字符为PM体系的常量。
可能有人会问，为什么没有“∧”（逻辑与）、“∃”（存在）、“⇒”（推出）以及其它一些常见符号呢？其实这些符号是可以通过上面的7个更基础的符号定义出来的，比如“a∧b”就是“~(~a∨~b)”、“a⇒b”就是“~a∨b”、“∃a∙b”就是“~(∀a∙~b)”等等。当然，后面我们还会使用这些非基本常量字符，只要大家知道，这些非基本常量都是通过基本常量定义出来的就可以了。
话又说回来，哥德尔也实在有点过分，别的符号不定义就算了，居然连“=”也没有定义为常量，这让后面构造表达式多麻烦啊？不过，哥德尔的论文中直接就使用了很多没有定义的常量，也不影响对论文的理解。我们对这点也就不深究了吧。
（2）变量
哥德尔论文中的PM体系的变量分为若干类（无穷多类），分类并起名如下：
“一级变量”：就是表示0和自然数的变量，比如x1如果是一级变量，它就可能是0、1、2、3、……。
“二级变量”：就是表示0和自然数的某些子集的变量，比如x2如果是二级变量，它就可能是{1}、{1,2,3}、{2,4,6,8,10}等等。
“三级变量”：就是表示以二级变量为元素的集合的变量，比如x3如果是三级变量，它就可能是{{1},{1,2,3}}、{{2,4,6,8},{1,3,5,7}}等等。
以此类推，以至于无穷级变量。
这些变量看起来莫名其妙，到底为什么要定义这么复杂的无穷级变量呢？别着急，一会介绍到哥德尔数的时候，会详细说明原因。
（3）公式
这里说的公式，就是前面说的PM表达式，以后将都采用公式这个名字了。
哥德尔首先定义PM中的基本公式，就是类似x、a、succ(a)、succ(succ(a))、a(b)之类的公式。特别的，如果b是n级变量，那么a(b)中的a就是一个n+1级变量。这是因为b每取一个值，a就会对应一个n级变量，于是随着b取了若干个值，a就成为了若干个n级变量的集合，也就是n+1级变量。
在基本公式的基础上，哥德尔定义了公式。公式包括基本公式以及由基本公式组成的~a、a∨b、∀x∙a类型的全体。
哥德尔还给公式分了类，对于不含有任何自由变量的公式，哥德尔称之为“命题公式”；对于含有n个自由变量的公式，哥德尔称之为“n元关系式”（n-ary relation sign）；特别的，当n=1时，就是前面提到过的“class-sign”（现在也可以叫做一元关系式了）。
哥德尔在这里特别提出了一个他定义的公式——subst(a,v,b)，其含义是把公式a中的变量v用b来替换，这里的v和b可以是任意相同级的变量。具体如下，设a是“v>10∧v<20”，则subst(a,v,10)就是“10>10∧10<20”，subst(a,v,x)就是“x>10∧x<20”。这个由哥德尔定义的公式很重要，后面构造出的不可证命题主要靠它。当然，这个公式也一定是可以在PM中表达的，哥德尔的论文在后面给出了46个不同含义的表达式，其中就包括subst，从中我们可以看出哥德尔其实是一个编程大师！
（4）公理体系
之后，哥德尔给出了我们一直说的PM公理体系的基本公理，共分为五组。考虑到这些公理是论文全部推导的基础，我就都列在这里了，涉及的相关基础知识比较多，就不一一详细说明了。
第一组：皮亚诺算术公理。其中的x1等表示一级变量，x2表示二级变量。
1、~(succ(x1) = 0)，把皮亚诺公理的起始数字定义为0。
2、succ(x1) = succ(y1) ⇒ x1 = y1，如果两个自然数有同样的直接后继，则他们相等。
3、x2(0) ∧ ∀x1 ∙x2(x1) ⇒ x2(succ(x1)) ⇒∀x1∙ x2(x1) ，这就是我们常说的数学归纳法，也是皮亚诺算术公理中的一条。
第二组：命题公理。这组公理就是《数学原理》中的基本推演公理。
1、(p∨p)⇒p
2、p⇒(p∨q)
3、(p∨q)⇒(q∨p)
4、(p⇒q)⇒((r∨p)⇒(r∨q))
第三组：无名公理。这组公理不知道叫什么名字合适，论文英文版的译者给它起名为quantor公理，这个名字有些不伦不类，我还是叫它无名公理吧。
1、(∀v∙a)⇒subst(a,v,c)，对于任意v，a都成立，意味着把任何变量c带入到a中的v之后都成立。
2、(∀v∙b∨a)⇒(b∨∀v∙a) 。
第四组：分离公理。哥德尔明确说，这个公理取代了分离公理（集合论中的分类公理）。
1、∃u ∙ ∀v ∙ (u(v) ⇔ a)
第五组：集合公理。
1、∀x1 ∙ (x2(x1) ⇔ y2(x1)) ⇒ x2 = y2
以上是哥德尔论文中的全部基础定义。所有基础定义都一样，枯燥无味，看懂就行了。
（二）哥德尔数
修炼第三重神功的时候，提到了哥德尔对应，哥德尔把PM中的公式对应到自然数。哥德尔是这样建立的具体对应关系的。
首先把7个常量（基础字符）对应到了7个数字，“0”对应1、“succ”对应3、“~”对应5、“∨”对应7、“∀”对应9、“(”对应11、“)”对应13。
其次，把常量以外的一级变量对应到大于13的质数，二级变量对应到大于13的质数的平方，三级变量对应大于13的质数的3次方，以此类推。
在这里，我们说明为什么要定义这么多级的变量。一级变量就是自然数，这容易理解。二级变量其实是一组自然数的序列，由于自然数对应着常量和变量，自然数的序列当然可以对应一个PM公式，我们也可以把它称为命题变量，这种变量可以代入不同的命题，如“x>y”、“0=0”、“∃x∙x=succ(y)”等。三级变量其实是一组自然数序列的序列，它对应着PM公式的序列，我们往往使用PM公式序列来定义一些“谓词”，或者阐述一个证明过程，因此三级变量其实就是某种“谓词变量”或者“证明过程变量”。如果熟悉编程序的话，谓词类似于C语言中的“函数”，它的结构类似一段程序代码，我们在后面“有含义概念的表达”中会看到哥德尔给出的大量“函数”。
最后，哥德尔采用一种规则，使得无论是公式还是证明过程，都可以对应到唯一一个自然数。设这个公式对应的自然数序列为（n1,n2,n3,…,nk），则它对应的唯一自然数为2n13n25n3…pknk，其中pk是第k个质数；再设一个由公式序列组成的证明过程或者谓词定义中，每个公式对应的自然数分别是（m1,m2,m3,…,mt），则这个证明过程或者谓词定义对应的唯一自然数为2m13m25m3…ptmt，pt仍是第t个质数。这种对应显然是依据素数唯一分解定理，确保了形成的每个自然数都是唯一的，当然，这样对应出来的自然数无比巨大。
为了便于理解哥德尔建立的对应关系，我们举个相对完整的例子，一方面有利于理解对应关系，另一方面也对PM体系中的公式的复杂程度有个感性认识。不过，由于哥德尔定义的基本常量实在太少了，我们补充定义一个常量“=”，并把它对应到自然数2，这样做对哥德尔的证明是没有丝毫影响的，否则通过逻辑来定义“=”太头疼了。
下面来看公式“∃z∙z=succ(x)”，含义是“存在z，使得z是x的直接后继”。首先，我们要把这个公式变换为仅仅使用哥德尔定义的基本常量来表达的公式。利用前面介绍过的“∃”与“∀”的关系，这个公式其实就是“~(∀z∙~(z=succ(x)))”。根据前的对应关系，并设x、z这两个一级变量分别对应质数17、19，同时因为“∙”这个符号仅仅是一个分隔符，在对应过程中忽略掉不会引起歧义，则这个公式对应的自然数序列是（5，11，9，19，5，11，19，2，3，11，17，13，13，13），于是它对应的唯一自然数是25311597191151311171919223329113117371341134313，这真的是一个天文数字，把这个数字后面加上一个“纳米”做单位，得到的长度也远远超出可观测宇宙的尺度。这个数虽然大，但理论上只要给出这个自然数，我们就可以通过上述原则唯一的把它还原为公式“~(∀z∙~(z=succ(x)))”。
以上就是哥德尔建立的PM公式与自然数之间的对应关系，在后面表达各种含义的时候，将充分利用这种对应关系。
（三）原始递归
原始递归关系是哥德尔首先提出来的，如今在可计算理论中是一个重要概念。哥德尔给出的原始递归定义至今仍然被部分采用。为了更清晰、准确的说明原始递归含义，我们给出如今的原始递归定义。
原始递归函数以自然数或自然数的元组作为参数并返回自然数。接受n个参数的函数叫做n元函数。基本原始递归函数用如下公理给出：
①常数函数：0元常数函数0是原始递归的。
②后继函数：1元后继函数succ，它接受一个参数并返回皮亚诺公理给出的后继数，是原始递归的。
③投影函数：对于所有n≥1和每个1≤i≤n的i，n元投影函数Pin，它接受n个参数并返回它们中的第i个参数，是原始递归的。
更加复杂的原始递归函数可以通过应用下列公理给出的运算来获得，
④复合：给定k元原始递归函数f和k个m元原始递归函数g1，…，gk，f和g1，…，gk的复合，也就是m元函数h(x1，…，xm) = f(g1(x1，…，xm)，…，gk(x1，…，xm))是原始递归的。
⑤原始递归：给定k元原始递归函数f和k+2元原始递归函数g，定义k+1 元函数h为，
h(0，x1，…，xk)= f(x1，…，xk)
h(succ(n)，x1，…，xk) = g(h(n，x1，…，xk)，n，x1，…，xk)
则h是原始递归的。
服从以上公理的函数是原始递归的。也就是说，如果一个函数是上述基本函数之一，或者它可以通过基本函数应用有限次的上述运算规则获得，则这个函数是原始递归的。
需要说明的是，哥德尔在论文中给出的原始递归的定义不包括上述公理的③条，且未明确包括④条。针对④中的复合函数，哥德尔只是在语言叙述中不很明确地提到，把任何原始递归的函数带入到某个原始递归函数的自变量中，得到的也是原始递归函数。另外，设一个原始递归函数Φ在定义它的运算过程中形成一系列函数Φ1、…、Φk直到Φ，哥德尔定义这个函数序列的最短长度为原始递归函数Φ的“度（degree）”。
给出了原始递归关系和原始递归函数的定义之后，哥德尔给出了原始递归的PM公式（按照哥德尔论文原文翻译过来，意思是原始递归的关系，primitive recursive relation，考虑到前面有PM公式的定义，个人认为还是翻译为原始递归PM公式更好一些）的定义：
如果一个有m个自由变量的PM公式R和一个原始递归函数Φ，满足
R（x1，…，xm）⇔(Φ（x1，…，xm）=0)
那么就说这个PM公式R是原始递归的。
从最原始递归基础函数可以推导出各种复杂的原始递归函数，其实我们日常接触到的大部分整数函数都是原始递归函数。在IT技术大发展的今天，大部分人都了解了计算机编程，我们可以粗略的理解原始递归函数是，能够通过编写计算机程序计算得到的函数都是原始递归函数。但是，要严格按照原始递归的定义来推导出某个函数是原始递归的，过程会很复杂。
我们举个简单的例子吧，证明h（x）=x是一个原始递归函数。
令0元函数f=0，二元函数g（x，y）=succ（x）；
按照原始递归公理定义h（0）=f；h（n+1）=g（h（n），n）；
由此得到函数h（x）=x。因为这个函数是按照原始递归公理定义的，因此必然是一个原始递归函数。
再举一个原始递归PM公式的例子，设R（x）是PM公式“∃z ∙ z+x<5”，意思是“对于数x，存在数z使得z+x小于5”。我们再找到一个原始递归的函数Φ（x）=x（x-1）（x-2）（x-3）（x-4）。可以看到，R（x）成立时，x只能取0、1、2、3、4，此时Φ（x）=0；x取其它值时，R（x）不成立，此时Φ（x）也不等于0。显然R（x）⇔（Φ（x）=0）。于是，“∃z ∙ z+x<5”是一个原始递归的PM公式。
弄清楚了原始递归函数和原始递归PM公式概念之后，哥德尔连续提出了有关原始递归的四个定理。
定理一：其实就是把原始递归公理④描述了一遍，区别在于扩展到了PM公式，意思是把任意一个原始递归函数带入到某个原始递归函数或原始递归的PM公式的自变量，得到的也是原始递归函数或原始递归PM公式。
定理二：如果R和S是原始递归的PM公式，那么~R、R∨S也是原始递归的PM公式（因此，基于∨、~定义的R∧S等也必然是原始递归的）。
定理三：如果φ（x1，…，xm）和ψ（y1，…，yn）都是原始递归的，那么PM公式“φ（x1，…，xm）=ψ（y1，…，yn）”也是原始递归的。
定理四：如果函数φ（x1，…，xm）和PM公式R（y，z1，…，zn）都是原始递归的，那么下面三个PM公式也是原始递归的，
S(x1，…，xm，z1，…，zn)⇔∃y≤ φ(x1，…，xm)∙R(y，z1，…，zn)
T(x1，…，xm，z1，…，zn)⇔∀y≤ φ(x1，…，xm)∙R(y，z1，…，zn)
Ψ(x1，…，xm，z1，…，zn) ⇔argmin y≤φ(x1，…，xm)∙R(y，z1，…，zn)
（第三个公式argmin的含义是，在满足y≤φ(x1，…，xm)和R(y，z1，…，zn)的条件下，返回最小的y；如果没有符合条件的y，则返回0）
这四个定理的目的很清楚，就是要证明原始递归的PM公式经过上述各种复合变换之后，仍然是原始递归的。哥德尔在论文里面给出了这四条定理的可信的证明。其中，定理一和定理三是显然的，我们着重介绍定理二和定理四的证明。
定理二的证明思路：这个定理的证明相对容易，哥德尔构造了三个简单的原始递归函数α（x）、β（x，y）和γ（x，y），分别对应着“逻辑非”、“逻辑或”和“逻辑与”，
如果R和S是两个原始递归的PM公式，那么它们必然对应着两个原始递归的函数r和s，使得R⇔（r=0）、S⇔（s=0）；再根据上面构造的原始递归的α、β、γ函数，就可以得到~R⇔（α（r）=0）、R∨S⇔（β（r，s）=0）、R∧S⇔（γ（r，s）=0）；也就是说，~R、R∨S和R∧S都是原始递归的。
定理四的证明思路：为了方便起见，我们把定理四中x和z的序列简记为
综上，哥德尔严格而准确地证明了某一类PM公式是原始递归的。之后，哥德尔将为我们构造46个PM公式，其中有45个是原始递归的，最终的目的就是为了表达出第46个公式provable（x）。
（四）有含义概念的表达
前面我们就说过了，哥德尔把PM公式对应到自然数，然后利用PM体系自身可以表达自然数及其关系的能力，再用PM公式来表达针对PM公式自身有含义的概念。希尔伯特把这种赋予形式化公理体系以含义后形成的数学称为“元数学”（Metamathematics），因此哥德尔自己把论文中这个章节的标题叫做“Expressingmetamathematical concepts”，表达元数学概念，我在这里翻译成“有含义概念的表达”。
哥德尔首先指出，根据前面“原始递归”概念，我们必然可以定义出类似x+y、x∙y、xy等形式的原始递归函数，表达出x<y、x=y等原始递归PM公式。再依据定理一至四进行相应的变换，哥德尔表达出了45个原始递归的、有含义的概念及关系。通过哥德尔列出的这些表达式，我真心觉得哥德尔是在电子计算机尚未发明出来的时候就出现的一个编程大师！由于表达式很多，我在这里就不一一列出了，仅举几个例子让大家欣赏。
（1）y|x ⇔ ∃z≤x∙ x=y∙z
这里y|x表示y能够整除x。
（2）isPrime(x) ⇔ ~(∃z≤x ∙ (z≠1∧z≠x∧z|x)∧ x>1)
isPrime(x)判断x是否为素数。素数判断对于哥德尔来说很重要，因为哥德尔对应主要是基于素数性质建立的，后面会看到，哥德尔大量利用素数的性质来把整数还愿为PM公式。
（3）prFactor(0,x)= 0；
prFactor(n+1,x) = argmin y≤x ∙ (isPrime(y)∧y|x∧y>prFactor(n,x))
prFactor(n,x)表示x这个整数所包含的第n个（按大小排列）素因子。比如1050=2×3×52×7，那么prFactor(2,105)=3，prFactor(3,105)=5，prFactor(4,105)=7。表达式中的逻辑关系非常清楚，定义方式也是原始递归形式的，因此这毫无疑问是一个原始递归的PM公式。
下面就不连续的列举了，再举几个后面主要涉及到的吧。
（6）item(n,x)= argmin y ≤ x ∙ ((prFactor(n,x)y|x)∧~(prFactor(n,x)y+1|x))
item(n,x)的含义是x这个整数对应的PM公式中，第n个字符对应的整数。这个函数当然要求变量x能够对应一个PM公式，并且n要大于0且小于x对应的PM公式的长度。
（8）x◌y = argmin z≤nthPrime(length(x) + length(y))x+y ∙
(∀n≤length(x) ∙ item(n,z)=item(n,x))∧(∀0<n≤length(y) ∙ item(n+length(x),z) = item(n,y))
x◌y是一个原始递归的函数，它把两个整数x和y所代表的PM公式连接在一起，并返回这个新PM公式所对应的整数。这里的nthPrime(n)返回第n个素数；length(x)返回x所代表的PM公式的字符长度。如果不看到哥德尔给出的表达式，我们很难想象这样一种关系也可以在PM中表达，而且还是原始递归的。
（43）immConseq(x,y,z) ⇔ y=imp(z,x) ∨∃v≤x ∙ isVar(v) ∧ x = forall(v,y)
immConseq（x，y，z）的含义是x是y和z的直接推论。其中，imp（z，x）的意思是~z∨x，isVar（v）的含义是v这个数字对应一个PM公式中的变量（其实就是大于13的素数或者这样的素数的整数次方），forall（v，y）的意思是对于任意v，y都成立。这三个表达式分别是哥德尔给出的第32、12、15个PM公式。
前面我们讲过，哥德尔只定义了7个基本常量，对于“⇒”这样的常量，可以通过“a⇒b就是~a∨b”来表示。那我们看immConseq（x，y，z）的第一部分y=imp（z，x），其实的意思就是“y=（z⇒x）”，这种情况下，如果y成立且z成立，按照修炼第二重神功时介绍过的变换原则二，得到x成立。因此，哥德尔称这种关系为“x是y和z的直接结论”。当然，还有另外一种特殊情况，当x直接与y关联的时候，相当于immConseq表达式的第二部分，x=forall（v，y），此时如果y成立，x必然成立，与z则无关了。
（44）isProofFigure(x)⇔ (∀0<n≤length(x) ∙ isAxiom(item(n,x)) ∨ ∃0<p, q<n ∙ immConseq(item(n,x),item(p,x),item(q,x))) ∧ length(x)>0
isProofFigure(x)的含义是x对应的一组PM公式是一个证明过程，也就是说这组PM公式的每一个要么是一个公理，要么是前面两个公式的直接推论。其中，isAxiom（x）表示x对应的PM公式是一个公理。因此，当isProofFigure（x）成立的时候，x中的每一个PM公式都成立。
（45）proofFor(x,y)⇔ isProofFigure(x) ∧ item(length(x),x)=y
proofFor（x，y）的含义是x能够证明y。其表达式的含义是，x首先要是一个证明过程，其次x这个证明过程的最后一个PM公式就是y。
（46）provable(x)⇔∃y ∙ proofFor(y,x)
provable（x）的含义我们之前已经提过多次了，表示x是可证明的。其表达式的含义也非常清晰，就是存在一个证明过程y可以证明x。哥德尔在表达完毕46个有含义的PM公式后，针对这第46个公式，特意说明，这是唯一一个不能断言是原始递归的PM公式。事实上，我们参照定理四可以看出，provable（x）与定理四中的S的唯一区别在于这里只是“∃y”而不是“∃y≤φ（x）”。
（五）对应引理
给出了46个表达各种含义的PM公式之后，哥德尔提出了一个很重要的定理——定理五，在《哥德尔证明》的这部书里面把它称为“对应引理”。但是如果今天在网上查找，基本上找不到所谓的“哥德尔对应引理”。这个定理实质的含义是，任意一个原始递归的PM公式，都对应着一个可证明的算术定理。个人觉得把这个定理叫做“对应引理”也还算恰当。
定理五：对于任意一个原始递归的PM公式R（x1，…，xn），都存在一个函数关系r（u1，…，un）满足，
R(x1，…，xn)⇒ provable(subst(r,u1，…，un,number(x1),…,number(xn)))
~R(x1，…，xn)⇒ provable(not(subst(r,u1，…，un,number(x1),…,number(xn))))
这里的函数关系就是指一个等式，比如f（x，y）=0之类的。subst这个PM公式我们前面讲过，它是哥德尔表达的第31个有含义的公式，意思是把后面的数字代入到r的变量中得到的公式。number（x）是哥德尔定义的第17个PM公式，意思就是返回表达数字x的PM公式，可以简单理解为就是x。
这个定理对后面的证明至关重要，但是哥德尔在这里却只是给出了说明式证明。其实，这里面涉及到的是原始递归函数的可计算性的问题。原始递归的函数，一定是可计算的。哥德尔给出的说明，其实也可以认为是证明。
对于任意一个R（x1，…，xn），因为是原始递归的，所以一定等价于某个原始递归的函数φ（x1，…，xn）=0。其实无非就是要证明这个原始递归的函数φ构成的函数关系φ（x1，…，xn）=0是可证明的。哥德尔解释说，因为φ是原始递归的，因此必然存在着一个函数序列，逐步构建得到了φ。而这个函数序列的起始函数必然是degree为1的函数，也就是基本原始递归函数0和succ，他们对应的函数关系一定是可证明的（其实也就是可计算的），于是根据递归定义，这个序列中的每个函数构建的关系都是可证明的。这里，
subst(r,u1，…，un,number(x1),…,number(xn))就是φ（x1，…，xn）=0
not（subst(r,u1，…，un,number(x1),…,number(xn))）就是φ（x1，…，xn）≠0
哥德尔这篇论文的贡献，除了证明了不完备定理以外，还奠定了可计算性理论的一些基础，间接地影响了冯∙诺伊曼、图灵等人构建的电子计算机的理论基础。今天，电子计算机已经普及到千家万户，如果我们通过计算机程序来类比的话，很容易让读者接受“原始递归的函数关系都是可证明的”这一结论。其实这里可证明的意思就是说，能够编写一个计算机程序，按照原始递归的定义，一步一步计算出φ（x1，…，xn）是否为0的这一结果。
（六）不完备定理
好，在证明完定理五之后，哥德尔论文终于进入实质性阶段了。
在这部分，哥德尔首先给出了我们在修炼第一重神功的时候就提到的“ω一致”概念的定义。设κ是一个公理体系，Conseq（κ）是包含κ中全部公理、定理以及这些公理、定理各级“直接推论”的公式的集合。换句话说，Conseq（κ）就是κ这个公理体系能够证明的全部“PM公式”。
定义公理体系κ是“ω一致”的，当且仅当不存在这样的一个PM公式a，使得（∀n∙ subst(a,v,number(n))∈Conseq(κ)）∧ not(forall(v, a)) ∈ Conseq(κ)成立。
这看起来很奇怪，每个a（n）都可以在κ中推导出来，同时~(∀n∙a（n）)也能推导出来。也就是说，每个a（n）都成立，同时“不是对于任意n，a（n）都成立”也能推导出来。这种情况发生时，我们就说这个公理系统不是“ω一致”的。严格地说，这种公理体系肯定是有矛盾的，但是这种矛盾又不足以同时推出a和~a。“ω一致”的公理体系肯定也是一致的，但是一致的公理体系未必是“ω一致”的，也就是说“ω一致”要比通常意义上的一致更严格一些。
明确了“ω一致”的概念之后，哥德尔给出了定理六——哥德尔不完备定理，我们在第一重修炼的时候就给出了原文。下面给出哥德尔对定理六的证明。
哥德尔先是扩展了前文提到过的“有含义概念表达”中的PM公式44、45和46，也就是isProofFigure（x）、proofFor（x，y）和provable（x）。扩展后的定义如下，
isProofFigureκ(x) ⇔ (∀n≤length(x) ∙ isAxiom(item(n,x)) ∨ (item(n,x)∈κ) ∨
∃0<p,q< n ∙ immConseq(item(n,x),item(p,x),item(q,x)))∧ length(x)>0
proofForκ(x,y) ⇔ isProofFigureκ(x) ∧ item(length(x),x) = y
provableκ(x) ⇔∃y ∙ proofForκ(y, x)
其实这次扩展只做了一件事，那就是在原来仅包括基本公理的基础上，把κ中的新公理也涵盖了进来。这样做的目的就是为了说明，不仅仅是PM体系的基本公理会导致后续结论，即使扩展进来更多的公理，也仍然会导致同样的结论。这也是为什么论文的题目中包括了“and related systems”的原因。
有了上述定义，下面两条结论是显然的，
∀x ∙ (provableκ(x) ⇔ x∈Conseq(κ))
∀x ∙ (provable(x) ⇒ provableκ(x))
之后哥德尔构造了一个PM公式，
Q(x,y) ⇔ ~(proofForκ(x,subst(y,19,number(y)))) （式2）
（式2）的意思是说“x不能证明y（y）”。y（y）指的是把PM公式y中的变量19（对应素数19的变量）替换为“y对应的自然数”之后得到的新PM公式。由于subst和proofForκ都是原始递归的，根据定理一，Q（x，y）也是原始递归的。于是根据定理五，一定存在一个原始递归的函数关系式q满足，
~proofForκ(x,subst(y,19,number(y)))⇒
provableκ(subst(q,17,19,number(x),number(y))) （式3）
proofForκ(x,subst(y,19,number(y)))⇒
provableκ(not(subst(q,17,19,number(x),number(y)))) （式4）
（式3）和（式4）看起来复杂，其实只是根据对应引理把PM公式Q（x，y）对应到了一个算术命题（或者叫函数关系）q（x，y）上。q（x，y）虽然是一个算术命题，但是它代表的含义仍然是“x不能证明y（y）”。注意到哥德尔这里用素数17和19分别代表变量x和y，我们后面也这样处理，不会每次都说明了。
然后，哥德尔定义了两个新的算术命题，
p=forall（17，q） （式5）
r=subst（q，19，number（p）） （式6）
很明显，（式5）中p（y）对应的含义是“任意x都不能证明y（y）”，或者说“y（y）不可证”。（式6）中r对应的含义则是“x不能证明p（p）”。请注意，p（y）的意思式“y（y）不可证”，因此p（p）的意思就应该是“p（p）不可证”，费尽千辛万苦到了这里，哥德尔终于构造出了一个含义是“自己不可证”的算术命题。
下一步就应该是把（式3）和（式4）中的y替换为p了。在此之前，我们先进行两项简单的算术推导，
subst(p,19,number(p)) = subst(forall(17,q),19,number(p))
= forall(17, subst(q, 19,number(p)))
= forall(17, r) （式7）
subst(q,17,19,number(x),number(p)) =subst(r,17,number(x)) （式8）
这样，我们把（式3）和（式4）中的y替换为p，并把（式7）和（式8）的结论代入后得到，
~proofForκ(x,forall(17,r)) ⇒ provableκ(subst(r,17,number(x))) （式9）
proofForκ(x,forall(17,r)) ⇒ provableκ(not(subst(r,17,number(x)))) （式10）
下面开始分析并形成结论，证明forall（17，r）就是我们说的不能证明也不能证伪的算术命题。
一方面，forall（17，r）不能证明。否则，就会存在一个n所代表的PM公式能够证明forall（17，r），也就是proofForκ(n,forall(17,r))，根据（式10）得到，
provableκ(not(subst(r,17,number(n))))
因为subst(r,17,number(n))的含义是“n不能证明p（p）”，所以上式的含义就是“能够证明’n能证明p（p）’”，也就是说“n能证明p（p）”；而forall（17，r）的含义是“任意x都不能证明p（p）”，这显然矛盾，说明公理体系κ是不一致的，当然肯定也不会是“ω一致”的了。注意这里只是违反了一致性。
另一方面，~forall（17，r）也不能证明。因为已经证明了forall（17，r）不可证，也就是说，
∀n ∙ ~proofForκ(n,forall(17,r))
根据（式9）得到，
∀n ∙ provableκ(subst(r,17,number(n)))
上式的含义是“任何PM公式都不能证明p（p）”，那么如果“~forall（17，r）”可证，也就相当于证明了“p（p）可证”。请注意，“任何PM公式都不能证明p（p）”与“p（p）可证”是矛盾的，但违反的是“ω一致”。
综上，无论是forall（17，r）还是~forall（17，r）都不可证。这样，哥德尔就构造出了一个算术命题，在公理体系κ内无法证明也无法证伪。哥德尔不完备定理终于被证明了。
最后再强调一下，哥德尔构造出来的是一个算术命题（也可以说是一个数论命题或者一个函数关系式），只不过它对应的含义是“自身不可证”，从这个含义出发，我们确定了它不可证明，并不是说这个算术命题表面上的意思是自己不可证明。很可能这个算术命题表面上只是一个极为复杂的算术关系或者数论猜想。
（七）讨论
在之后论文的讨论部分，哥德尔重点阐明了一个观点，那就是哥德尔不完备定理不是只适用于皮亚诺公理体系。不管人们如何扩充公理体系，即使把发现的无法证明且证伪的命题都定义为公理，也仍然会存在新的不可证明且证伪的命题。其实这个结论我们在之前的介绍和大量的说明中已经阐明了，只不过当年哥德尔在写论文的时候，非常担心这一点，因此又花费了不少篇幅来补充说明。
（八）第二不完备定理
哥德尔在论文的推广（Generalizations）部分详细分析了公理体系κ的一致性与构造的命题forall（17，r）之间的关系。根据上面的证明，我们知道了，
“公理体系κ是一致的”⇒“forall（17，r）不可证”，（注意前面的证明过程中表明，forall（17，r）可证只是违反了一致性）
也就是说，
“κ一致”⇒~provableκ(forall(17,r))
⇒~(∃x ∙ proofForκ(x,forall(17,r))) （依据基本逻辑）
⇒∀x ∙ ~proofForκ(x,forall(17,r)) （依据基本逻辑）
⇒∀x ∙ ~proofForκ(x,subst(p,19,number(p))) （依据式7）
⇒∀x ∙ Q(x,p) （依据式2）
⇒∀x ∙ provableκ(subst(q,19,number(p))) （依据式3）
⇒∀x ∙ provableκ(r) （依据式6）
⇒forall(17,r) （式11）
这样，我们严格的证明了“κ一致”可以推出forall（17，r）。由于forall（17，r）不可证，因此“κ一致”也必然不可证。这个结论由哥德尔在论文中以定理十一提出。
定理十一：κ是包含PM的一致的公理体系，那么陈述κ是一致的PM公式在κ中是不可证明的；也就是说，κ是一致的，那么κ的一致性是不可证的。
至此，我们完成了第四重神功的修炼。这部分内容超长，原因是哥德尔的证明相当严谨，以至于哥德尔原定再写一篇论文来进行更详细的阐述都是多余的了。如果读者完全理解了这部分的内容，恭喜你，你已经是“哥德尔不完备定理”的集大成者了。
转载本文请联系原作者获取授权，同时请注明本文来自赵昊彤科学网博客。
链接地址：http://blog.sciencenet.cn/blog-409681-1067025.html
https://blog.sciencenet.cn/blog-40692-1311648.html
上一篇：[转载]来自赵昊彤科学网博客：“哥德尔不完备定理”到底说了些什么？（3 of 5）
下一篇：[转载]来自赵昊彤科学网博客：“哥德尔不完备定理”到底说了些什么？（5 of 5）
