哥德尔原著译本的前十四个定义—

哥德尔原著译本的前十四个定义——哥德尔读后之十三

广州的疫情依然紧张，我校昨晚还包括今天早上，员工都在奔赴南操场进行自5月底以来的第二次核酸检测。因为疫情，差不多有一个月都蜷缩在家中了，顶多因为生活必须，去一下家门口附近的便利超市。得感谢网络带给这个世界的便利，让我们在疫情封锁之下，能够足不出户获得来自万里之遥的货品，消融掉一些闭户不出带来的郁闷与纠结。
核酸检测

网上购物还算方便

现代网络来自计算机科学的迅猛发展，再往前追溯，一般会追到信息科学的源头。在格雷克那本《信息简史》中，最早的计算机灵感来自英国的巴贝奇（1791-1871），但那只是计算机的一个设想或者雏形，还不是现代意义上的计算机。
巴贝奇

真正计算机的出现，是在20世纪的50年代前后。吾辈仰苍天之福，拜计算机科学所赐，有幸于九十年代后拥有之使用之。但有一个问题常萦绕于心，这现代意义的计算机的出现，可以用时间之先后来做因果解释么？有20世纪算术公理化理论的出现，有现代逻辑的出现，再有哥德尔、香农、图灵、塔尔斯基等跨界英才的出现，才有现代的计算机么？没有香农和图灵等人，大概计算机就还漂浮或者潜藏在一个谁也不知的世界，还在等待人们的寻寻觅觅。这很容易被人们所接受，因为这些智者的理论和科学活动，紧密联系着这个新时代的产物。但哥德尔那个神秘的定理证明，也是计算机出现的一个前因么？恐怕很多人不会接受这样的因果解释。不看哥德尔的书，这个因果解释大概很多人会存疑。一个纯粹观念上的探索结果，与所谓三大实践活动完全不搭界，会是产生活生生的现代计算机科学的前因？至少在我这里就大有疑惑。
也许，正是这样的疑惑，以及对这种疑惑的解惑冲动，让我在逻辑历史的追溯之中，又一次走进哥德尔。这一次，不再是看他的那些评介性的文字，也是凭借网络，这一次竟然先后发现两个哥德尔原著英译本。两个译本的对照阅读，存疑很多，但解惑好像更有依赖。
那个剑桥的译本，导言部分花了不少时光，但疑惑重重，还真没有摸到门。无意间从科学网发现张寅生的博客和他的《证明方法与理论》一书，好家伙，买来一看，另一版本的原著Martin Hirzel英译本（2000）中译本都在书中，的确是深究哥德尔的好材料。这个发现有如久旱恰逢及时雨，剑桥译本常感到有错误，但又不知如何纠正，其实也是拿不准，这个识错是不是本来就是自身修炼不足之错。有对照本了，这下，腰杆子感觉硬朗了许多。
还是按部就班，继续跟进到第二章，开始哥德尔46个定义的那一部分。45个定义要一气呵成，博客篇幅太长，我计划分为三个部分，用三篇做完，这一篇读其中的前14个定义，剩余31个定义另作两篇吧。难怪内格尔在其《哥德尔证明》一书中说哥德尔难读，你只要看他的46个定义，其实，你只要先看其中的三分之一，你就有此言不虚的感觉。

一、哥德尔的前14个定义观念统计

哥德尔1962年译本，和刚弄到的2000年译本，定义表述上稍有差别，符号使用上差别更大。我估计，在后的译本应该可靠性更高，但在前的译本大概更接近哥德尔的原著。我将综合两个译本，主要依据在后译本，给出我的编译。
当读到定义6的时候，在为符号使用犯嘀咕之际，突然闪现一个念头。前5个定义全都是关于素数的，阶乘的。第6个定义又冒出一个GI，1962年译本称这是德文词项的意义，英文称作term。但2000年的译本则用item来表示，那就不是词项，而是“项”了。这时我就想，如果后面引出的又是这样一些解释有异的情形，那哥德尔的阅读，是不是在给出定义的理解之前，对哥德尔给出的观念，包括表达观念的符号、辅助符号、在定义中借用的概念等，先做一些梳理为好呢？于是，本篇的结构，也就在对这些观念符号有事先的铺垫说明之后，再来编译哥德尔的前十四个定义。如果说明的东西太多，对定义的理解又得后延。不过，这数码文字的体味不就如同在做一个一个游戏，事先的计划总要随着你消化文本的效率来定。而这个效率，好像总是个未知数。
对14个定义统计的结果，定义了这样几类观念，另加上定义外的argmin。
1）算术运算：定义1除法（以下略掉定义二字，概念前数字为哥德尔定义序号）
2）与素数相关的三个定义；2素数Pime，3素数因子prFactor，5第n个素数nthPrime，
3）与自然数相关的三个定义：6数的项term或者item，7数长度length，9数序列sequence
4）有关阶乘的一个概念：4阶乘factorial
5）三个逻辑符号：8连接joining together，13否定not，14析取or，
6）有关Var的两个概念：11第n个类型的变元Type（n,x)，12变元Var，
7）括号化操作符号：10相关左括号（和右括号）的符号操作Ex或者parenthesizine。
除了这些被定义概念之外，在被定义概念之中，还有一个值得关注的观念，在1962译本中是希腊字母符号ε，在2000年译本中是argmin。于是，前述定义的概念中就有第八个观念。
8)哥德尔解释过的符号ε，在后译本翻译为argmin，在上述定义中多次出现。

二、两个英译本的定义1-7和8-14的表达式比较表

这定义的东西做了简略统计之后，又产生一个念头。干脆把两个版本的原始定义做一个比较表格，从这个比较中来确认你阅读文本的感受。由此，录下来两个文本的14个定义。序号是哥德尔文本中定义序号，对照表分为两个。

这个定义1-14比较的表格终于做完，很是辛苦，颇有点做python代码的味道。一个代码出错，那文件就执行不了。而一个符号出错，理解这个定义就非常困难。这数码的游戏真不是可以轻松玩耍的。但人就应该这样，决心做一件事，就得有做一件事的交代。

三、给出原著文本编译

哥德尔给出的45个定义，全部属于递归定义。
函数x+y，x*y，xy等，还有关系x<y,x=y都发现是递归的，它们开始于这样一些观念，我们现在就来定义这些观念，这些观念是一些函数和关系。我给出1-45个定义，来构成一个定义系列。这个定义系列中的每一个定义，都借助命题1到4所称呼的运算从在前的定义中获得。这个过程，一般而言，是把许多个定义步骤放在一起，而这些定义步骤又是经命题1-4所允许的。这些定义1-45中的每一个函数或者关系含有，例如这样一些概念“公式”，“公理”，和“直接后承”，他们因此而是递归的。

定义1.**x/y≡z(z ≤ x ∧ x = y * z)
这里是x被y整除的除法定义。除法可以定义为：存在一个数z，这个z小于或者等于x，并且，那个除数x等于被除数y和结果z的乘积。
凡涉及到量词（全称，特称，最小）符号的定义，x值域就是有限度的。这个限度只是用来保证所定义概念的递归性质（也就是命题4所规定的性质）。另外，所定义概念的定义域，则常常因为在理解不受影响的情况下而被省略。定义1中的星号*为乘法符号。

定义2.Prim(x)≡～((z)(z ≤ x )∧(z≠1)∧(z≠x)∧(x/z))∧(x > 1)
这个定义，定义了素数，比欧几里得的定义要复杂。欧几里得定义素数为：仅能被1整除的数。而按照哥德尔的定义，一个数x为素数至少有二个大条件。
1）它要大于1，即x > 1；
2）不存在一个称作z的数，即～((z)(z ≤ x )∧(z≠1)∧(z≠x)∧(x/z))。
这个称为z的数又需满足4个条件。
2.1）z≤ x，z小于等于x；2.2）z≠1，z不是1；
2.3)(z≠x),z不是x； 2.4)x/z，z能被x整除。
不存在这样4个条件的z，这定义够复杂的。先想象一下这个z，可能会是什么样的自然数。假设素数为13，13这个素数中是否不存在以上所说的那个z呢？好在13之下的数字不多，逐一查验，真还不存在满足上述4个条件的z，所以，13符合素数的定义。
而任一不是素数的自然数，则一定存在一个数z，满足上述条件之一。
欧几里得的素数定义那么简单直白，哥德尔这样定义有必要么？这问题有点费思量，不过，哥德尔一上来给出定义，就给个使用否定词的定义模式，这倒是和他的否定式证明风格有点相匹配。

定义3. Pr( 0,x) ≡ 0
Pr (n+1,x) ≡arg min y(y≤x ∧ Prim(y)∧x/y ∧y > n Pr x))
这个定义中的argmin，我的哥德尔原本英译本上是希腊字母ε，在前面命题4中也有出现。哥德尔把εxF(x)解释为：最小的数x，对于这个x，F(x)成立，并且，如果没有这个数x存在，这个数即为0。（哥德尔文本第43页）
这就是说，哥德尔使用的这个εxF(x)也就是今天的函数符号argmin的含义。如今计算机语言中的常用函数argmin，就是使得它后面携带的函数F(x)中的x取最小值，因此，这个argmin就表示取函数定义域最小值的集合，和哥德尔的含义同。
由此，我们可以把这个定义3作以下解释。
定义0 Pr (0,x) ≡ 0中的左式0 Pr(0, x)，pr表示素因子，如2000年译本中的prFactor，x自然是任意整数的一个变元，n则表示这个整数x中按大小排列的第n个素因子（factor）。如果n=0，则素因子就等价于0。这里的素因子，显然全都是素数，所以哥德尔用pr来表示，与定义2的Prim以示区别。
定义3之后的一串字符，完成了定义3的递归定义。
Pr( n+1,x) ≡arg min y(y≤x ∧ Prim(y)∧x/y ∧y > Pr(n,x))

当素数因子为第n+1个位置的时候，该位置的素因子y取什么值呢？那就是满足以下4个条件的最小数y。
1)y≤x，素因子y比整数x小，除非x也是素因子，它们才会相等；
2)prime(y),素因子y是素数；
3)x/y，素因子y可被整数x整除，即x是y的倍数；
4)y > pr(n,x)，y比x中的第n个素因子大。
举个简单的例子吧，210这个整数，按照数字大小顺序，有2，3，5，7一共四个素因子。当n=0的时候，自然是0。当n=2的时候，素因子就是3。整数x的n+1=3位置的素因子由此是5。这四个式子按照哥德尔的表述分别是：(1)Pr(210)=2；(2)Pr(210)=3,（3）Pr（210）= 5；（4）Pr（210）= 7。
哥德尔在这个符号串之后，还有一段注释，也是对这个符号串的解释，他说:
符号pr(n,x)是在x中含有的第n个素数，按数量大小排序。

定义4.0！≡ 1
（n+1）！= (n+1).n!
阶乘为法国数学家基斯顿.卡曼（Christian Kramp，1760～1826）1808年发明的运算符号，英语为factorial，这是给以下与素因子阶乘相关定义准备的基础性定义。

定义5.Pr(0)≡0
Pr(n+1)≡argmin(y)(y≤{Pr(n)}!+1∧Prim(y)∧y>Pr(n))
Pr(n)是第n个素数因子（按数字大小排序）。
这个定义与定义3，4似乎完全是同一的定义结构，先有数字为0时，这个函数的对应值0，然后就出现数字n+1。该定义与阶乘有关联，我们仿定义3作简略说明。
当素数因子为第n+1个位置的时候，该位置的素因子y取什么值呢？那就是满足以下3个条件的最小值y。
1)y≤{Pr(n)}!，即素因子y小于等于（素因子位置为n的阶乘+1）；
2)Prim(y)，即y是一个素数；
3)y>Pr(n)，即y大于第n个素因子。
阶乘好像是高中生学习的数学课程，把阶乘与素数，进而与递归联系起来，有点意思。但接下来的定义，仍然把关注点放在素数上，不过，加进了一个新元素：词项。

定义6.term(n, x )≡ argmin(y)（y ≤ x∧x/Pr(n,x)y,∧～(x/Pr(n,x)y+1)
这个定义6，是关于词项term的定义。德文字符GI是英文term的含义，修订版改为term，以下简称为项。n term (n,x)表示：指派给数字x的数字序列中的第n个项（n>0，并且n不大于这个数字序列的长度）。
当指派给数字x的数字序列中第n个项的时候，该项的素因子y取什么值呢？那就是满足以下3个条件的最小值y。
1)y≤x，即数字y小于等于x；
2)x/(nPrx)y，即x可整除作为x第n个素因子的y次方的那个数。
3)～(x/Pr(n,x)y+1),即x不可整除作为x第n个素因子的y+1次方的那个数。

这个定义依然是相关于素数的一个观念，但被定义项不是指称的素数，而是素因子。素因子先出现在条件2）的那个除法公式。该公式的被除数指称了一个素因子的y次方，即整数x指派的数字序列中的第n个素因子的y次方。在条件3）中则以否定形式出现，同样素因子的幂变成y+1次方。

定义7.len(x)≡argmin(y)(y≤x ∧ yPrx > 0 ∧(y+1)Prx=0)
这个定义7，是给指派给变元x的所有数字构成序列，len表示该数字序列的长度。这个len(x)长度就是函数argmin，表示取函数定义域最小数的集合。这个最小数y，由此就需满足以下三个条件。
1)y≤x，即数字y小于等于x；
2)yPrx > 0 ，即整数x的第y个位置的素因子大于0；
3)(y+1)Prx=0，即整数x第y+1个素因子等于0。

定义8.x ○ y≡argmin(z)(z≤(Pr(len(x)+len(y))x+y∧
(n)(n≤len(x)→((term(n,z)=term(n,x))∧
(n)(0≤len(y)→((term(n+len(x),z)=term(n,y))

其中的x ○ y表示：两个有限数字序列连接在一起，相当于加在一起，有算术加和与逻辑合取的味道。1962译本使用号，但星号已经作为乘法符号，使用2000年译本的○是恰当的。

定义9.seq(x)≡ 2x。

这个定义中的R(x)仅仅对应于由大于1的数字变元x构成的数字序列，这个序列的英文为sequence。所以用2000年译本的seq定位比使用R应该更为合适。

定义10.paren(x)≡seq(11) ○ x ○ seq(13)。

这个定义中的(x)对应于“括号”字符的运算，数字11和13分别指派基本符号左括号“（”和右括号“）”。所以，2000年译本用paren更加合适一些。

定义11*Type(n,x) ≡ (z)((13 <z≤x)) ∧ Prim(z) ∧ x=(z)n))∧ (n≠0)
这个定义11中的变元x是第n个类型的变元，我依2000年译本也用Type来表达这个定义。这个第n个类型变元x会是某个素数z，而且大于13，其n次方就是x。有点费解，慢慢琢磨吧。

定义12.Var(x)≡ (n)((n≤x) ∧ Type(n,x))
这个定义中的x是变元。说x是一个变元，那在表明存在数字n，该数字n满足以下两个条件。
1)n≤x， n小于等于x
2)nTypex, x是第n型变元。

定义13.not(x) ≡ seq(5)。
这个定义中，not(x)是x的否定。

定义14.**or(x,y)≡paren(x)○seq(7)○paren(y)
这是x与y的析取，定义时与括号相关，有什么特别的蕴意，且待对于全部定义的梳理。