哥德尔的形式系统P——哥德尔重读拆解汉译之三

又到了新的一年，时序交替总有人借文字而抒发心中情愫，而诗之简洁流畅常常是抒发情愫之首选。而文字之借，又以情寄古典最为便捷，还可藏自文之拙也。于是，在解读哥德尔之际，伴随岁月流转之叹，思绪飘忽之时，随意翻阅起那本厚厚的《唐诗鉴赏辞典》。无意中品味了初唐诗人刘希夷拟古乐府《有所思》中一段，那花相似与人不同的对照，颇让人找到点文字的寄托，且把这短短的诗句留驻在读哥德尔的文中。

古人无复洛城东，今人还对落花风。

年年岁岁花相似，岁岁年年人不同。

照片

时序交替不已，花开花落轮转。虽有古人无复，却有今人还对。这花相似而人不同，似乎在映衬着哥德尔关于时间的主观哲学。有灵魂的世界才会有时间，无灵魂的世界，大概就如同刘希夷的诗句，年年岁岁花相似矣，哪里会有时间的感觉。不过这时间的哲学，如同人的感觉一样，多种多样，各有各的道理，各有各的套路。而且，还各有各的根基。人文之问，不能没有哲学。但人问之问，还是得从经典中找到些支撑。继续读这个哥德尔，大概可以找到些哲学思考的元素吧。

接续上篇的导言部分，这一篇开始哥德尔原著文本的主体了，那就是哥德尔原著文本的第二章：主要结论（main result）。该章内容众多，恐怕又得多篇博客才能弄完，本篇主要拆解汉译其第二章的第一节。德文原本和Martin Hirzel英译本都用阿拉伯数字编码为2，然后就是节2.1。

一、哥德尔的形式系统P，本质上是先前数学家逻辑学家创造的叠加

先给出原著2000年英译本第二章的汉译。开译之前提请注意，除标题外，凡粗黑体字为原著文本英译本的拆解汉译，非黑体字为汉译者的衔接和评论。

原著文本拆解汉译

2 主要结论

我们现在将精确地执行以上所描述的证明，开首，先给出形式系统P的一个精确描述。对这个形式系统P，我们寻求去证明不可判定定理的存在。大体而言，P是这样的一个系统，它是通过给PM逻辑叠加上皮亚诺的公理而获得的（数作为个体，后继关系作为未定义的基本概念）。

这个译文告诉我们，哥德尔建构的系统P，主要是二个构件。一个构件是罗素与怀特海在其《数学原理》中给出的PM，熟悉逻辑史的人一般都知道。罗素等的PM，在更早的时候，则是德国人弗雷格的《概念语言》，也有较完整的逻辑系统描述。另一个构件是意大利人皮亚诺创建的公理化算术。而比皮亚诺更早的德国人戴德金，在其《自然数的意义与本质》的论文中，同样有很精彩的有关自然数的论述。但随后的描述表明，哥德尔所建构的系统P，显然还有第三个构件，那就是集合论，由康托创建，其后又由策墨罗和弗兰克尔发展而成的ZFC集论。

所以，可以用以下等式来简略表示哥德尔的形式系统P：

PM逻辑+皮亚诺公理+ZFC集论公理=哥德尔系统P

这三个构件的基本内容，哥德尔立刻就以基本符号，系统P公理，基本概念的方式在随后的文字中展现出来，一种清晰而且概略的描述风格。

二、数学家与逻辑学家积淀下来的人工语言基本符号

为了给出哥德尔的主要结论，在简略的第二章题头之后，哥德尔给出了他的P系统。整个第2章的第2.1节，即题为定义的这一节，就是哥德尔的系统P，本质上是先前数学家逻辑学家符号创造的叠加。

原著文本拆解汉译

2.1 定义

以下是系统P的基本符号（the basic signs）

I.常元符号：“Ø”（并非），“∨”（或者），”"“（对所有而言），”0“（零），“succ”（后继），“（”（左园括弧），“）”（右园括弧）。【英译者评注：哥德尔的原创文本使用了不同的符号，但读者应该更熟悉在这个英译中所使用的符号】

II.类型1变元（表示个体，也就是包括0的自然数）：

“x₁”,”y₁”,”z₁”,......

类型2变元（表示个体类，也就是自然数的子集subset）：

“x₂”,”y₂”,”z₂”,......

类型3变元（表示个体类的类，也就是自然数子集的集合）：

“x₃”,”y₃”,”z₃”,......

表示任何作为类型的自然数，则如此等等

原著文本评论：二元或者n元函数（关系）的变元作为基本符号是多余的，因为我们可以把关系定义为序偶类和序偶类的类。例如，用｛｛a｝,{a,b}｝定义序偶(a,b)，其中，｛x,y｝代表类，其仅有元素分别是x，y和x。

这里的常元与一级到n级类型变元，正是哥德尔以前的逻辑学家构建出来的东西。除了所描述的逻辑基本符号，接下来给出的，是皮亚诺算术的基本符号。紧跟原著评论之后，根据类型符号的定义，哥德尔随之给出了类型1符号的一个算术实例。在算术实例之后，以基本公式为基础，哥德尔继而给出了一阶逻辑中的复合公式，然后又给出了代入运算。很明显，这些复合公式和代入运算，也都是现代逻辑学科沉淀下来的智慧成果。

在描述代入运算时，2000年英译文本显然有误，把公式b错写成公式a。依张寅生汉译文，同时参照哥德尔德文原著在以上汉译中做了更改。此外，把这个第2章2.1节，题名为定义好像有点不大妥当。依据哥德尔文集卷1的英译本和德文原著本，哥德尔原著文本的各章各节均只有数字编号，无章节题名。这个题名为英译者所加。在哥德尔文集卷1的英译文中，并非精确定义，而是精确描述。用描述似乎比用定义要好（参见《哥德尔文集卷1》1986年版英德文对照本第151页）。2.1节的题头依然用英译本的定义，虽觉不妥，但更换它名好像也有难度。

我们继续看Martin Hirzel的英译本，然后给出它的汉译。

原著文本拆解汉译：

使用类型1符号，我们来理解这种形式符号的一个组合。

a，succ(a), succ(succ(a)), succ(succ(succ(a))),...。

其中，a为0，或者为类型1变元。在类型1的情况下，我们称这样一种符号为数字符号。对于n>1，我们将用一个类型n的符号来理解类型n的变元。我们称形式为a(b)的符号组合为基本公式（elementary formulae），其中的b是类型n的符号，a是类型n+1的符号。我们定义公式类为那个最小的公式集合，该公式集合含有所有的基本公式，并且对于a，b而言，总是含有Ø(a)，(a)ú(b)，"x(a)（其中的x是任意变元）。我们称(a)ú(b)是a与b的析取，Ø(a)是a的否定，"x(a)则是a的普遍化。一个不含自由变元的公式（其中的自由变元用通常的方式予以解释）称作命题公式(proposition-formula)。我们称一个恰带有n个自由变元的公式（没有其它自由变元）为n元关系符号，对于n=1，则称为类符号。

我们将代入符号（其中的a是一个公式，v是一个变元，b则是与v同类型的一个符号）理解为这样的公式，该公式是对在公式a中出现的v的每一个自由变元都用b来代入而获得的。我们称一个公式a是另一个公式b的类型提升(type-lift)，如果你能够通过增加在公式b中的出现的所有变元类型，并用同样数字来增加而获得a的话。

这里的类型提升好像有点诡异，其它的定义似乎不难理解，这里来尝试做点解读。哥德尔在给出类型提升的定义之前，有一个对于公式a(b)的解释，那应该是理解类型提升概念的一个启示。a(b)是一个符号组合，b是类型n的符号，a是类型n+1的符号，这样的公式被称为基本公式。而因为b可以属于a，a的类型就从b的类型n，提升到了类型n+1，但这里的类型是指称的基本符号类型，还不是公式的类型。其后哥德尔定义的公式类型提升概念，似乎与推理有关系。在哥德尔原著的1962年英译本中，翻译为：如果从b推出a（if a derives from b）,这和2000年英译本的译法，如果从b获得a（if you can obtain a from b）的翻译是一致的，显然也是推理的含义。那就是说，从一个命题导出另一个命题的时候，我们把公式a中变元所对应的个体类型增加了，或者说提升了，而且是变元的数量有多少，我们就用同样数量的个体来增加。好像还拿不出合适的公式实例来说明这种提升，暂且给出这样的尝试性解读吧。

三、数学家逻辑学家留下的五组公理

哥德尔随后给出五组共11个公理，一组皮亚诺算术公理，然后是命题逻辑的一组公理，接之是谓词逻辑的一组公理，最后两组，第4组组属于集论的内涵公理，最后一组属于集论的外延公理。

原著文本拆解汉译：

下述公式（从I到V）被称作公理（这些公理借助通常方式定义的省略式而得到表达，这些省略式分别是：“∧”（合取），“→”（蕴涵），“”（等价），“$x”（存在），“=”(等号）)，有关园括号的省略也遵照通常习惯。

I.皮亚诺公理，【英译者评论：也略称PA，它为自然数给出了基本性质】。

1.￢(succ(x₁)=0)，【英译者评论：我们总是从0开始计数】。

2.succ(x₁)=succ(y₁) →x₁=y₁，【英译者评论：如果两个自然数x₁与y₁ÎIN，它们有同样的后继，则这两个自然数相等】。

3. x₂(0)∧x₁,x₂(x₁)→ x₂(succx₁)))→x₁,x₂(x₁)【英译者评注：使用数学归纳法，我们可以证明在自然数上的一个谓词x₂】。

II.每一个公式都是从以下模式，通过对于p，q，r的任意公式替换而导出。我们称这些公式为命题公理。

1.p∨p→p

2.p→p∨q

3.p∨q→q∨p

4.(p→q) → (r∨p→r∨q)

III.从以下两个公理模式中获得的每一个公式

1.v(a)→Subst a

2.（(v,(b∨a)）→（b∨(v,(a)）

通过对符号a，v，b，c代入以下东西，（并且实施在上述模式1中指称的subst（代入）运算））：

代入任意的公式替换a；代入任意的变元替换v；代入任意公式替换b，在被代入的公式中，v不是自由出现；代入和v同类型的符号替换c，并且c不含有如下的自由变元，即该变元在a中某个位置被约束，但变元v在该位置上却是自由的。

【英译者评注：因为缺少更好的名称，我们将称这些公式为量词公理】

不知为何，Martin Hirzel译本英译为量子公理，张生汉译本循此，但此处的两个公理明显与逻辑中的量词相关，我将其更改为量词公理。

量词公理1通常理解为全称概括，v既然是自由变元，则这个自由变元覆盖的所有个体，都可以用来替换那个a。也就是如文本所言，执行在公理1中由Subst所指称的运算，用任意给定的公式来替换a。

而量词公理2中的自由变元v，如果出现在复合公式(b∨a)中，则蕴涵着这样的结论。

这里的v是任意变元；b则是这样的公式，即v不作为自由变元在b出现。如此，则原来辖域为b∨a的全称公式，就可以是全称辖域仅在a中的一个全称公式和b的析取。这个公理,应该是一阶逻辑公理系统K6的一个变形。

我们继续拆解汉译。

原著文本拆解汉译：

IV．从以下模式获得的每一个公式

1.u"v（u（v)a)),

分别用类型n或者n+1的任意变元替换v和u，并且为公式a替换不含有变元u自由出现的公式。这个公理表达了还原公理（集合论的内涵公理）

V.从以下类型提升导出的任意公式，（包括公式本身）

1.（∀x₁（(x₂(x₁) y₂(x₁)) x₂ = y₂

这个公理陈述了：一个类完全由其成员来决定。【英译者评注：我们称其为集合公理】

一个公式c称为公式a与b（关于a）的直接后承，如果a是公式Øbúc（或者，如果c是公式"v(a)，其中，v是任意变元））。可证公式类被定义为最小的公式类，该公式类含有公理并且相关于“直接后承”关系封闭。

最后两个公理，从逻辑跳到了集合论，给出了集合论的两个公理。但集论的这两个公理，是分别给出的。哥德尔文本以第四组的编号给出还原公理，也称内涵公理；以第五组的编号给出集合公理，也称外延公理。让人隐约感觉，哥德尔这样的编排，是不是别有一番意味？Martin Hirzel的英译没有对此作出评论，也许，随着原著文本的进一步展开，个中意蕴会有显露的吧。但互为对应的内涵和外延公理，各自作为一组公理单独给出，大概可以表明，这一对公理在哥德尔文本中的特殊意义。一个集合的成员由成员的性质来决定，这是内涵公理的要点。而一个集合的构成由成员所指称的客体对象来决定，则应该是外延公理的要点。任意一个集合，大概总是这两个公理中的一个来判定的。

除了以上的五组公理，2.1节最后一小段，给出系统P的直接后承概念和可证公式概念，直接后承容易理解。哥德尔用很为简洁的语句来定义直接后承，但含义是精准的。一个证明的公式序列，由在前的两个公式a和b，依据推理规则获得第三个公式c，其中在后的b，自然相关于在前的a，或者就是属于a的一部分，才能够依据规则获得c。由此，c就是a与b的直接后承，直接后承观念由此而得。但可证公式类定义为最小的公式类，因为出来一个最小公式类概念，则需要在此多啰嗦几句。

可证与最小公式类相衔接，这里大概既是数学的，逻辑的，也有点哲学的味道在其中，至少有两个方面的哲学意味吧。

一个是，在导言那一章就出现的可证，在标号（1）中以否定的形式呈现为“不可证”，以说明R_n(n)的性质。在那里，我们看到了一个数字不可证的标号（1），而且这样的数字性质还可以得到证明。这就让数字公式不仅具有了逻辑特征，也让数字公式有了那么一点哲学味。哥德尔的主要结论都与这可证不可证的观念相连，后续还有诸多与这类概念相关的讨论，似乎全都让人想到哲学。

另一个则是这段汉译文本的最后一段，竟然给了我们一个最小公式类的概念。因为最小很容易和最大，进而和无限联系起来，哥德尔文本的另一种哲学意蕴，也恰好从这个最小公式类开始有所呈现。

皮亚诺算术公理归结出了自然数的良序性，由这个良序性而得到定理：若一个自然数集L非空，则L必有最小数。这个源于良序性质的最小数概念，似乎在ZFC集论中另有一种风采，它和其中的无限公理产生了在最小特性上的关联。这就让我们把自然数的良序性质，牵扯上ZFC的无限公理。ZFC中的ZF6作为集论的无限公理，它陈述的是：存在一个后继集（或者归纳集）。这无异于告诉我们，存在一个可以无穷延伸的自然数的集合。也就是说，ZFC集论预设了一个实无穷（实无限）集合的存在。由这个公理预设，于是我们就有了几乎和良序集类似的客体对象，集论称之为：最小后继集（归纳集）。该客体对象也好像和皮亚诺中的一样，最小后继集就是指称的自然数集合。一般用希腊字母w，来表示这个最小后继集（参见程极泰《集合论》第27页）。

看来，哥德尔的最小公式类，是皮亚诺算术中的最小数概念，也是ZFC中的最小后继集概念的一个衍生客体，似乎是一个具有更为抽象性质的客体类型。哥德尔文本随后出现的w一致性概念中的w，应该就是ZFC集论中的最小后继集w。

2022年开年的第一篇博客，就暂且到此了，且待后续。