896第一不完全性定理证明标号分类拆解汉译知识背景——哥德尔原著拆解汉译之一
2021-12-16 09:17阅读：
896第一不完全性定理证明标号分类 拆解汉译 知识背景——哥德尔原著拆解汉译之一
哥德尔原著中的第一不完全性定理证明的全过程，已经艰难地旅行了一趟。不是浮光掠影，却依然处在似懂非懂之中。静坐沉思，常自叹功力甚浅，未能力透纸背，了悟哥德尔符号玄机也。
刚刚学到两个对待知识态度的英文单词。一个是
know-it-all，中文翻译为无所不知，另一个是
learn-it-all，中文翻译为无所不学。我们这个社会好像有不少
know-it-all即无所不知的人和团体，所有人，所有团体都得听它的，因为它无所不知。好在还有一个正好与这个无所不知对应的无所不学，它恰恰是无所不知的反面。我们总有学不完的知识，我们应该用一种谦恭包容的态度对待人类的知识，用虔诚的学习态度来对待这人世间的一切存在。
无所不知图
上帝无所不知
无所不学
一个智慧的存在，谦恭的学习态度应该为第一要义。你准备去学习某种东西，除非不可抗拒的因素在给你困扰，不然，浅度漂学解惑不了，就不可不懂装懂，自以为无所不知。倒应该是提升强度，如同旅行中的普通游升华为深度游那样。在粗读哥德尔原著一轮之际，好像来了点这样的感觉，感觉非增加点深度游览，才有可能窥见哥德尔文字之奥妙，或者练出点功力，能够察知哥德尔符号之瑕疵。
于是，那计算机指令中经常用到的循环迭代，就起了一点启示作用。也许，这循环迭代产生的熟，继而生发出的灵性，能够映衬出孔老夫子的那句千古名言：温故而知新的。
由此，哥德尔原著英译本的迭代阅读就这样开始了，因为有第一轮的打底，可以先对哥德尔第一不完全性定理的证明流程，做一个概要性的描述了。
一、哥德尔第一定理证明流程分类
好几本哥德尔参考读物，都是从哥德尔定理的大背景角度来概括哥德尔证明的。我的第一着眼点没有大背景，仅在哥德尔原著本身。先对哥德尔证明第一不完全性定理给出的
16个标号，给出分类的描述。然后看有不有可能，捣鼓出哥德尔证明的一个路线图。
（一）18个标号与4个分类
哥德尔证明第一不完全性定理中的
16个标号，再加上标号（
6）之下的（
6.1），标号（
8）之下的（
8.1），总共
18个标号。按其符号性质分类，大致可以分为以下几类：
第一类：六个定义
1.标号（
1）自然数类
K定义
K=｛nÎN
|Øproveable(Rn(n)｝
（1）
2.标号（
2）原始递归定义
这是与哥德尔形式系统
P无直接联系的递归定义
一个数论函数
Φ(x1,x,…,xn)被说成是根据数论函数Ψ(x1,x,…,xn-1)和μ(x1,x,…,xn+1)而递归定义的，如果对于所有的x1,x,…,xn，k,以下等式成立：
Φ(0,x1,x,…,xn)=Ψ(x1,x,…,xn),Φ(k+1,x1,x,…,xn)=
μ
(k,Φ(k,x1,x,…,xn),x,…,xn)
（2）
哥德尔给递归所做的这个定义客体，现在称为原始递归函数。
3.标号（
5）
证明序列定义
递归
w一致条件下公式类k，一公式x可证定义，类似于哥德尔文本中提及的概念，也就是哥德尔46个定义中的定义44
isProofFigurek(x)('n(n≤length(x))→(isAxiom(x)(term(n,x))∨term(n,x)∈k))∨($(p,q(0
0
(5)
这个定义标号为（
5），意在说明一个在
w一致条件下，证明序列是什么样的客体对象。
4.标号（
6）
证明定义
递归
w一致条件下公式类
k，一公式
y是
x证明序列的定义，同样类似于哥德尔文本中提及的概念，也就是哥德尔
46个定义中的定义
45
proofFormulak(x,y)(isprooFiguresk(x))∧(term(length(x),x)=y))
(6)
5.标号（
6.1）可证定义
递归
w一致条件下公式类
k，一公式
x可证明的定义，也类似于哥德尔文本中提及的概念，也就是哥德尔
46个定义中的定义
46的类似定义，一个不是原始递归关系的定义。
provablek(x)($(y)(proofFormulak(y,x))
(6.1)
6.标号（
8.1）二元关系定义
Q(x,y)ØproofFormulak(x,subst(y,19,number(y)))
(8.1)
第二类：两个命题
1.标号（
3）肯定对应定理
1
R(x1,x2,…,xn)provable(subst(r,u1,…,un,number(x1)…number(xn)))
(3)
2.标号（
4）否定对应定理
2
ØR(x1,x2,…,xn)
provable(not(subst(r,u1,…,un,number(x1)…number(xn))))
(4)
第三类：两个假定
1.标号（11）带有一个自由变元的类符号p
p =forall(17,q)
（11）
2.标号（
12）带有一个自由变元的类符号
r
r = subst(q,19,number(p))
（12）
第四类：八个导出命题
1.标号（
7）全称等价公式
'x（provablek(x)x∈Conseq(k)）
(7)
2.标号（
8）全称蕴涵公式
'x（provable(x)
provablek(x)）
(8)
3.标号（
9）
运用对应定理获得的否定证明序列蕴涵式1
(Ø(proofFormulak(x,subst(y,19,number(y)))
(provablek(subst(q,(17,19,number(x),number(y)))
（9）
4.标号（
10）运用对应定理获得的肯定证明序列蕴涵式
2
((proofFormulak(x,subst(y,19,number(y)))
(provablek(not(subst(q,(17,19,number(x),number(y))))
（10）
5.标号（
13）对类符号
p使用代入运算获得的连续等式
subst(p,19,number(p))=subst(forall(17,q),19,number(p))
=forall(17,subst(q,19,number(p)))
=forall(17,r)
（13）
6.标号（
14）对二元符号
q使用代入运算获得的等式
subst(q,1719,number(x)number(p))=subst(r,17,number(x))
（14）
7.标号（
15）否定的证明序列蕴涵式
3
(Ø(proofFormulak(x,forall(17,r))
(provablek(subst(r,17,number(x)))
（15）
8.标号（
16）肯定的证明序列蕴涵式
4
(proofFormulak(x,forall(17,r))
(provablek(not(subst(r,17,number(x)))))
（16）
（二）最后导出两个不可证结论，获得不可判定命题forall(17,r)
由以上标号导出以下两种结果：
1.forall(17,r)不是k可证。
2.
not(forall(17,r))也不是k可证，
由此，
forall(17,r)在
k中不可判定，命题
VI得到证明。
以上哥德尔给出的这
18个标号，我按性质给予了分类。但在原文中，则是按标号顺序列出的。为了对哥德尔的思路有更好的了解，以下给出哥德尔原著
2000年英译本的汉译。分类之后做拆解汉译，这拆解汉译所翻译的内容，仅汉译出其中的标号部分和标号部分的联结语，包括英译者的评注。汉译中的英译者评注为英译本中原已附带的，汉译评注则是我另外给出的。
二、按照哥德尔18个标号顺序的原著2000英译本部分汉译
以上标号分类，来自哥德尔原著英译本中部分译文，我在这里将英译本再做一次中文转译。黑体字是从英文转为汉语的哥德尔原著，其中使用方括号的文字为英译者评注，非黑体字的汉译评注，则略略解读与联结这些原著英译文字。
在哥德尔原著英译文本导言的第
4段，哥德尔在给出他简洁的证明直观之后，很快就进入主题，构造了一个在
PM中的不可判定命题。请注意，这里是给定
PM中的不可判定命题，然后才开始构建哥德尔自己的系统
P。
再次提醒注意，以下拆解汉译形成的中文文字，黑体字是哥德尔原著英译的汉译，非黑体字则是我给出的评注和联结语。
（一）拆解汉译（1）（2）（3）（4）
我们开始哥德尔原著英译文本的第一段汉译，从原著的标号（
1）起步。
我们现在将构造一个系统PM的不可判定命题，那就是，它是如下给出的一个定理A，对于该定理A而言，既不是A可证，也不是ØA可证。
我们将把仅带有一个自由变元，该自由变元的类型为自然数的PM公式，称作类符号（class-sign）。我们将假定这些类符号可用某种方式按顺序编排，我们将把第n个顺序编排的类符号，称作Rn。请注意，概念“类符号”和序关系R都在系统PM内可定义。设α为任意类符号，我们用α(n)表示用n代入α
