证明序列 证明公式和可证——哥德尔读后之十九

广州的天气依然很热，农历的暑期已过，农历的处暑也过了几天，处暑，暑热之终止也。但秋凉的感觉，在广州这里似乎全无，且暂留两张随意档来的秋照送别夏天吧。

秋天是出游的季节，连续不断的疫情依然在阻断你的游兴，只能让你困守宅屋。继续与那些诡谲的符号做伴，随意浏览有关处暑的信息，有诗曰：

处暑无三日，新凉值万金。

白头更世事，青草印禅心。

我好像不是这样的心境，但诗文，这个既可能是心外之客体，也可能是心内之客体的东西，颇有传染性。禁不住要在心内寻找点东西，为这广州的处暑时节，留下点感性的字符。

处暑历多日，潮热弥广州。

人生虽苦短，静敲叹春秋。

一、哥德尔第一不完全性定理的证明概述

（一）哥德尔第一不完全性定理的两种译本表述

首先给出两个哥德尔原著英文译本，1962年译本和2000年译本对于第一不完全性定理的两种表述。

命题6：（1962年英译本）

对于每一个w一致性的递归类公式c，都存在对应的递归类符号r，使得无论是对于v一般化r还是对于并非v一般化r，它们都不属于Flg(c)。其中，v是r的自由变元。（（这里的一般化是德语缩写Gen，v一般化r的符号在1962英译本中表示为v Genr。并非v一般化 r，则表示为Neg（v Genr）。而这里的后承集合是德语缩写Flg，后承集合c在1962英译本中表示为Flg(c)，请注意字体的不同。））

命题6：（2000年英译本）

对于每一个w一致性的原始递归类公式k，都存在一个原始递归类符号r，使得无论是对于所有的v,r,即forall（v,r），还是对于并非所有的v,r，即not(forall(v,r))，它们都不属于conseq(k)。（其中，v是r的自由变元）。

两个译本几乎完全保持一致，2000年的译本表述方式更为现代。以下证明解读，主要依据2000年译本（参见张寅生著《证明方法与理论》第4部分附录），参考1962年译本。

（二）哥德尔第一不完全性定理的证明结构

哥德尔第一不完全性定理的证明结构，大致分为这么几个部分：

1）命题6定理表述，如以上（一）所示。

2）一个假设的表述，紧跟证明之后。

3）标号（5）-标号（16）总共14个标号公式的表述，紧跟假设之后。

4）由此而获得A和ØA两个不可证公式，命题6得证，紧跟标号（16）之后。

在此，先列出哥德尔在定理证明中的假设，

命题6证明：假设c是任意给定公式的递归w一致性公式类。

（三）重温哥德尔系统P的基本符号和变元变域中的客体

解读标号（5）之前，重温哥德尔系统P中的最为初始的客体对象很有必要。其中最为基本的，应该是基本符号和变元变域的对象，这正是标号（5）至标号（8）中定义的证明序列，证明公式，还有可证概念的定义基础。

1）系统P有七个基本符号：

这七个基本符号分别是0（零），f（后继），Ø（并非），∨（或者），"（全称量词），”（‘’（左括号），“）”（右括号）。

2）系统P中的变元、变域客体和基本公式：

系统P中的变元底层或者根部元素是个体，这里的个体不是泛指的任意个体，不是指任意单独存在的专有名词指称的客体，而是限定在自然数范围内的个体。而且，这里的自然数个体还包括0。由此可知，自然数1，2，3，….中，每个单独的数字都是哥德尔变元变域中的个体

变元由此从个体起算，也就是从一个一个自然数数字起算。

如果变元变域中的个体是一个一个自然数来构成，这些自然数构成的类为第一类型，也称作个体类。

如果变元变域中的个体是一个一个自然数类来构成，这些自然数类构成的类为第二类型，也称作个体类的类。

依此类推，自然有第三类型，一直到第n类型，也就是个体类的类的类…等等。

3）由哥德尔的这个圈定的基本符号和变元的概念可知，以下标号（5）-（8）中的证明序列，证明公式和可证概念，它们所说的公式就是由基本符号和变元一起构成的命题或者语句。这里的公式、命题和语句也稍微做一点区分。

形式为a(b)的符号组合，其中的b是第n型符号，a是第n+1型符号，这样的组合就是基本公式。例如标号（6）中的(isproofseq_c(x))，就是一个公式实例，它表明x是一个证明序列。其中的x如果是第n型符号，则(isproofseq_c就是第n+1型符号。

于是命题公式propositionalformula的概念就出现了，命题公式自然可以简称为命题。何谓命题？一个没有自由变元在其中的公式，称之为命题公式，简称命题。哥德尔给出的命题1到命题6，都是作为命题公式的实例。

而‘’语句‘’statement或者sentence概念在未作特别解释的情况下，可以看做命题的同一概念替换，这里不再做近一步的区分。

由此可知，哥德尔定理所面对的公式和命题，首先是基本符号+自然数个体，这构成系统P中的第一类符号。然后是自然数个体构成的类与基本符号的组合，由此而有从1到n的各种类型的公式或者命题。

所以我们需要谨记的是，哥德尔的P系统，是以自然数为客体的形式系统。我们面对的，并非是可以泛指的任意客体对象。

好了，做了这么多的铺垫，我们该回到命题6的证明上来了。在给出命题6证明的假设之后，立刻遇到的就是标号（5）给出的证明序列概念。

二、标号（5）-标号（8）的证明序列，证明公式和可证概念

这个定理的证明过程，哥德尔列出标号（5-16），包括（6.1）（8.1），总共14个证明公式，根据这些标号公式，最后得出不可判定性的结论。计划分两到三篇博文完成证明解读，本篇博文解读全部标号中的（5）-（10），涉及到有关”证明”概念，“关系”概念，即谓词概念的八个公式。

这八个标号的公式，先给出三种有关证明的概念。一个是”证明序列“”概念proofSeg，一个是“证明公式“”概念proofFormula，一个是“可证”概念provable。

（一）证明序列proofSeg

我们先看哥德尔给出的标号（5），标号（6）和标号（7），如何来阐释这些概念。

第一个是标号（5）：

isproofSeq_c(x)≡("n(n≤length(x))→(isAxiom(x)(term(n,x))∨term(n,x)∈c))∨($(p,q)(0<p∧q<n)∧(consequence(term(n,x)∧term(p,x)∧term(q,x)))∧length(x)>0   (5)

这个定义标号为（5），意在说明一个证明序列是什么样的客体对象。

标号（5）解读：

这个定义类似于在前的哥德尔定义44所定义的概念。但需要注意的是，在前定义44，45和46都是有关证明的，但仔细品味文字，三种有关证明的表达式，表达的却是三个有区别的概念。

第一个是德文缩写Bew，表达的是可证，英文为provable。

第二个是德文缩写B，表达的是证明，英文为proof。

第三个是德文缩写Bw，表达的是证明模式，英文为proofschema

哥德尔定义44给出的是一个证明模式proofschema的定义，它告知，如果x是一个证明模式，那么这个模式就是一个证明序列，该序列中的每一个项或者是公理，或者是由两个在前公式导出的直接后承。

这的确和标号（5）很为类似，就此，标号（5）可以看作定义44的一个特例。这里稍稍提及逻辑理论中常常用到的两个观念，型与例，也可以叫做类与分子。最高的型似乎是范畴，我们无法再向上提升，而最低的例似乎是个体，我们似乎也没有办法向下降格。处在最高与最低之间的中间型或者中间例，则常常兼具型与例这两种角色。

简而言之，定义44是型，而标号（5）则是定义44的例。如何解读这个标号（5）呢？请注意哥德尔证明前的那个假设，它预设了一个递归w一致性类c。标号（5）比定义44多了一个定义条件，它所面对的公式序列是属于c的，不是更一般的定义44中的任意有穷序列x，而是递归的还有w一致性的c。由此，这个标号（5），依据哥德尔给出的定义，我们可以给出与定义44几乎同样的理解。

标号（5）左式isproofSeq_c(x)，表示：x是一个属于c的证明序列。这里给出isproofSeq_c，c放在最后的下标中，其实就是类型下降的一种常元表示方法，表示的就是这个证明序列处在c类条件之下。这样的处理还可以给人一种直观的理解，那个x就成为表达证明序列这个类别中的变元。

我们再看右式：

("n(n≤length(x))→(isAxiom(x)(term(n,x))∨term(n,x)∈c))∨($(p,q)(0<p∧q<n)∧(consequence(term(n,x)∧term(p,x)∧term(q,x)))∧length(x)>0

一个证明序列一般都是由若干公式来构成，有多少个公式这是可以计数的。所以，这里就有length(x)，表示x这个证明序列的长度数，n则按照哥德尔在先的约定，是任意自然数的符号。由此我们可以看到上述蕴涵式的前件表示这样的条件：对于任意自然数n而言，如果证明序列x的长度数为n。那么，就有如下后件所呈现的结果：

（1）或者x的任意n个项isAxiom，这表示任意n个项或者是公理；

（2）或者x的任意n个项∈c，这表示任意n个项或者属于递归w一致性类c；

（3）或者存在着公式p和q，p对应的数字位置长度大于0，q对应的数字小于n，使得证明序列x中的公式是在前公式p和q的直接后承；

（4）证明序列x的长度数字大于0，即x长度不能为空。

所以这个标号（5），给出的是具有递归和w一致性的证明序列的定义。记住这里的证明序列概念，证明序列概念与标号（6）所定义的证明概念不同，也和标号（6.1）给出的可证概念不同。

（二）证明公式proofFormula

且看下面的标号（6）和标号（6.1），先看标号（6）。

哥德尔接之就给出了标号（6）

proofFormula_c(x,y)≡(isproofseq_c(x))∧(term(length(x),x)=y))     (6)

这个定义标号为（6）

标号（6）解读

刚才有定义标号（5），那是针对证明序列给出的定义。这里又出现一个证明proof，后带formula，这是证明公式概念。一个证明序列是若干个公式的合成，而一个证明公式y则只是单独一个公式，并不是公式的拼接合成。这里又有逻辑与哲学经常要涉及到的观念，整体和部分。它和型例的关系几乎完全不同，公式不是公式序列的型，公式只是公式序列这个整体的组成部分。我最近听人宣扬一种哲学，说这个世界只有一个公理，叫做”宇宙只有一个”，由此可以推出当今的一切东西，包括科学和人文。但整体和部分的关系似乎很难逻辑处理，怎么能够出此狂言，真叫人难以理喻。

如果标号（5）是哥德尔定义44的一个例，则标号（6）是哥德尔定义45的一个例。

什么是一个证明公式呢？一个证明序列是一元的定义方式，只有一个变元x，证明公式则是一个二元的定义方式。

我们先看定义左式。

左式：proofFormula_c(x,y)

这可以解读为，x是公式y的一个证明，这个证明公式也如同标号（5）一样，给出了具有递归和w一致性的公式类c，所以比定义45多了些条件。自然，这个x作为y的一个证明，y也就是一个单独的公式，都在递归和w一致性的公式类c的条件之下。所以这个标号（6）是为公式变元y定义的，不是为x定义的，x依然是一个证明序列。

我们再看右式。

右式：(isproofseq_c(x))∧(term(length(x),x)=y))

可以看到，y要成为一个公式，需要满足合取支右式的两个要求：

一个要求是，x是一个证明序列，满足标号（5）条件的证明序列。

另一个要求是，x作为证明序列的长度达到长为x所对应的数字，即达到证明序列x的最后一个公式的时候，这个公式恰好就是y。

所以证明序列是一个一元的定义，而证明公式一定是个二元式的定义，它相关于证明序列而获得自身定义。它属于一个证明序列，并且它还是这个证明序列中的最后一个。由此，这个定义既需要递归和w一致性的公式类c的条件，还需要刚刚建立的标号（5）的条件，真还有点意思。

（三）可证概念

现在我们有了证明序列，证明公式的定义，标号（5）和（6）。别以为这个证明的概念就被搜罗干净了，还有一个可证公式概念。看起来和证明公式很相近，其实是很有差异的，且看哥德尔的标号（6.1）。

在标号（6）之下还有标号（6.1）

provable_c(x)≡($(y)(proofformula_c(y,x))       (6.1)

标号（6.1）解读

我们还是按照常规过程，先看标号（6.1）的左式。

左式：provable_c(x)

这可以解读为，x是可证的，或者更简单一点，x可证。因为有下标c，自然是在递归和w一致性的公式类c的条件之下。这显然是一个一元式定义，左式只有一个变元x。

那么x可证，需满足什么要求呢？我们且看右式。

右式：($(y)(proofformula_c(y,x))

可以从右式看到，有存在量词置于前，表示存在y，这是个什么样的y呢？一个二元关系说明了y的性质，而这个二元关系正好就是标号（6）所定义的关系。所以，这个标号（6.1）和标号（5）（6）一样，恰好就是哥德尔定义46的一个例，定义46是它的型。

存在y，那y是什么呢？y是x的证明公式。显然，获得这个（6.1）定义，需要先有标号（6）的定义，而标号（6），又需要标号（5）的定义。哥德尔这连续的三个定义，一环扣一环，没有前面的，自然就没有后面的。

（四）可证概念的延伸

有了以上有关证明序列，公式证明和可证概念的定义，可知以下公式明显地并且清楚地成立。有趣的是，这些明显成立的公式，都和可证概念相关。

先看标号（7）

"x（provable_c(x)≡x∈consequence(c)      (7)

这个公式标号为（7）

标号（7）解读

继续按照常规出牌，把定义拆分成左式和右式。

左式："x（provable_c(x)

对于所有x而言，x可证。

说一个具有递归和w一致性的公式类c中的公式可证，需满足右式所描述的条件。

右式：x∈consequence(c)

只要x属于c中的直接后承即可，这明显先根据标号（5）的证明序列定义。一个客体可证，首先得有一个证明序列。而要有一个成立的证明序列，至少得满足其析取中某一个选言支，而属于某个直接后承正好是其中一个要求。直接后承又是由在前两个公式，根据公理和推理规则推导而来，于是直接后承中的每一个公式，依据标号（6），就都是证明公式，这又用到标号（6）。再根据（6.1），x存在着证明公式y，就表明x可证，这又用到标号（6.1）。

标号（8），也是以上证明观念的延伸。

我们来看标号（8）：

"x（provable(x)→provable_c(x)）      (8)

这个公式标号为（8）

标号（8）解读

这个标号（8），左式可证不带下标，右式可证带下标c。这表明，属于型的可证性，蕴涵着属于例的可证性。用通俗的解读方式，一般蕴涵着特殊，自然反过来是不行的。在标号（8）之后依然是有关证明观念的表达式，但带上了一些新的观念，首先是关系，接之用证明公式观念，同时又用哥德尔数的观念来说明这种关系。

三、从证明概念到关系概念

不可判定和证明有着天然的联系，但要理解这个不可判定，还有一些重要的元数学概念你无法规避。这些概念在开始证明命题6之前就有了一些交代，深入到命题6的证明环节，它又走进哥德尔的视野。相关证明的概念有了以上的铺垫之后，又一个抽象观念，关系概念作为证明的必涉观念，再一次出现在读者面前，这就是标号（8.1）定义的关系Q。

关系概念历来是逻辑学家高度关注的逻辑概念，逻辑史上两个大师级的人物，一个是哥德尔，一个是塔尔斯基。前几年联合国科教文组织特设一个世界逻辑日，这个逻辑日的设定就和这两位学者有关。世界逻辑日的那个日子，恰好就是这两位学者诞生的同一天。

言归正传，继续关系概念的讨论吧。塔尔斯基在谈到关系概念时说：关系的理论是逻辑中一个专门的而且非常重要的部分，关系理论研究带有完全任意性质的关系。（参见塔尔斯基《逻辑与演绎科学方法论导论》第84页）。塔尔斯基这个评述似乎告诉我们，对关系概念的理解是在完全任意性质的视野下进行的。就此而言，关系是比函数更为宽泛和抽象的概念，关系应该是函数的型，而函数是关系的例。所以塔尔斯基在随后讨论函数时，说函数是另一类特别重要的关系。

在标号（8）之下继而有标号（8.1），那就是哥德尔又定义出来的一个概念，他称之为关系。哥德尔的关系概念没有涉及可证，它和证明公式相关联，但对关系的关注似乎自然要关联到谓词和性质，这也是哥德尔命题6证明很难规避的一些元数学观念。

本篇篇幅已经够长，有关关系的讨论且留给下篇吧。