天灾经典定义31-46译本对照——哥德尔读后之十五

从牛年之初，就被哥德尔原著英译本缠上。导论的阅读，覆盖了牛年的春天。正文浏览之际，又碰上广州的荔湾疫情。
春日已过，入夏时分，阅读之余，游兴萌生。思绪迁移到了疫情阻断的旅行，念想着到塞外风情的内蒙旧地重游，追怀那客逝他乡的苦命之人。想到就做，于是机票定好了，车也预定好了。可人算不如天算，恰好就是起飞前的一天，北京和内蒙地区挂起了暴风雨的橙色预警。可能就是预警吧，不会影响行程的。我好像有一种对媒体的天然不信任感，包括最有科学依据的天气预报，也受这个感觉的牵连，被放进了不信任列表名单之中。所以，依然将所有的行装都准备停当，管他什么预报，我只按原定计划出发。
谁知，清晨起来，真的是人算不如天算，短信已经传来了多项取消航程的消息。凡预定北京的当天行程，所有的航班一律停飞。我们的那个航班还更为决绝，干脆就取消，连改期的程序也免了。一次准备充分的旅行，就这么成为了泡影。这让我想到了一些精致利己主义的哲学家，讨论的什么实体概念，有些所谓物欲论者的什么论和什么公理，一副自信满满，人定胜天的气概，只觉得有些可笑。这个哲学感觉，以后有机会再谈，此处暂且打住。
挂起橙色预警

一、灾祸连连的盛夏七月

时令进入下半年的首月七月，整个世界除了疫情，好像到处都麻烦多多。素来寒凉的北美洲山火不断，极端气温甚至到达50度，这个气温，连昔日中国的三大火炉都没有达到过，竟然能够在处于寒带的北美加拿大出现。近几日更是惊天奇闻，素来无洪灾的西欧地区，洪灾连连，洪水竟然可以淹没屋顶，导致欧洲数百人命丧洪灾之中。欧洲200多年未见的洪水滔天，就发生在本年度的盛夏七月。
加拿大的极端高温

美国的山火连连

西欧洪水滔天

还有巴西的亚马逊热带森林，这个昔日的地球之肺，被七月美国太阳报的一个新闻报导为，如今已经成为地球的负担，不但没有减轻碳排放，反倒成了碳排放之源。
亚马逊森林

这个世界怎么啦？过分悲观那是多余，但自信满满，傲视自然和人文，则肯定是如同天灾一样虐害这个世界的人祸。不过还有真的科学在，读经典体味经典，大概还能够让人们在惊恐之余，找到一些敬畏，找到一些解决自然和人文问题的方法。这读书可能无用，但至少它也无害，何况是在读那些有关科学的经典文献。
已读过哥德尔定义的1-30，我们继续前行，读他的定义31-46吧。

二、定义（31-46）–1962年译本与2000年译本对比

延续前面博文的编写程序，先把两个译本版本的定义31-46做一个列表对比，然后在第三部分，对哥德尔的这十六个定义做一个粗浅的解析。

定义31-38比较图5

定义39-46比较图6

三、定义31-46的粗浅解析

定义31：代换概念
1962年译本：Sb()≡SbA(v,x)()
2000年译本：subst(x,v,y)=subst’(nFreePlace(v,x),x,v,y)
这个定义31，哥德尔紧随其后，有个简短的说明。说那个被定义的左项公式是这样一个公式的概念（这里的概念简而言之，恐怕就是将公式普遍化的含义），该公式由以下符号构成：
Subst()
即该公式中的a代表一个公式，v代表一个变元，b则是一个与v同样类型的符号，那个subst则如哥德尔所言是一个元数学符号，表示代换。也就是把a中的所有自由变元v用b代换后获得的公式。
所以，这个定义31翻译最好修改为：
Sb()≡Sbv(v,，x)()。

定义32：蕴涵合取析取存在
1962年译本 2000年译本
x Imp y ≡ [Neg(x)]Dis y
x Con y ≡ Neg{[Neg(x)] Dis [Neg(y)]}
x Aeq y ≡ (x Imp y) Con (y Imp x)
x Ex y ≡ Neg {vGen[Neg(y)]} imp(x,y) = or(not(x),y)
and(x,y) = not(or(not(x), not(y)))
equiv(x,y) = and(imp(x,y), imp(y,x))
exist(v,y) = not(forall(v, not(y)))

这是四个纯粹的逻辑符号定义，逻辑是什么，数学是什么？大概这些逻辑符号就可以给你答案。

定义33：类型提升
1962年译本 2000年译本
n Th x ≡ εy{y≤ &
(k)[≤l(x)→(k Gl x ≤ 13
& k Gl y = k Gl x)∨(k Glx > 13
& k Gl y = k Gl x.[1 Pr(k Glx)]n)]} typelift(n,x) = argmin y≤ .k≤
length(x).item(k,x)≤13∧item(k,y)=
item=(k,x)∨item(k,x)> 13∧item(k,y)
=item(k,x).prFactor(1,item(k,x))n

这个定义33，是当x和第n个类型的x是公式的时候，第n个x就是x的第n个类型的提升，即type-lift。
所以这个定义最好是以下表达式：

typelift(n,x) = argmin y(((y≤ ∧k((k≤length(x)→(item(k,x)≤13))∧(item(k,y)=
item=(k,x))∨(item(k,x)> 13))∧(item(k,y)=item(k,x)∧prFactor(1,item(k,x)))n

定义34：皮亚诺公理
1962年译本
Z-Ax(x)≡(x=z1 ∨ x=z2 ∨ x=z3)
2000年译本
peanoAxiom(x)(x= pa1∨x=pa2∨ x=pa3)

对应于皮亚诺公理模式Ⅰ中1-3，恰好有三个判定数，可以用pa1,pa2和pa3来指称。这当然用定义模式来说明为好。
peanoAxiom(x)≡(x= pa1∨x=pa2∨ x=pa3)

定义35：从命题逻辑公理序列得到的公式
1962年译本
A1-Ax(x)≡(Ey)[y≤x & Form(y)& x =(y Dis y) Imp y]
2000年译本
prop1 Axiom(x)y≤x. isFm(y)∧x=imp(or(y,y),y)
公理模式Ⅱ有四个公理，定义35是说，x是一个公式，这个公式用公理模式Ⅱ中的公理1通过代换而得到，可以表述为A1-A(x)。类似地，如果x是通过逻辑公理模式中的某个公理代换而得,那也可以分别表述为A2-A(x),A3-A(x),A4-A(x).
由此，这个定义35表述为以下公式为好：
mlogic1 Axiom(x)≡y((y≤x∧isForm(y)∧x=imp(or(y,y),y))

定义36：依然是有关逻辑公理的定义
1962年译本
A-Ax(x) ≡ A1-Ax(x) ∨ A2-Ax(x)∨ A3-Ax(x) ∨ A4-Ax(x)
2000年译本
propAxiom(x)prop1Axiom(x)∨prop2Axiom(x)∨prop3Axiom(x)∨prop4Axiom(x)

这个定义依然是有关逻辑公理模式的，它用析取的方式来定义。其中的x是这样的公式，它通过在逻辑公理模式中代换而导出，所以一定是四种逻辑公理中的一种代换式。
由此，这个定义36可表述如下：
mlogicAxiom(x)≡mlogic1Axiom(x)∨mlogic2Axiom(x)∨mlogic3Axiom(x)∨mlogic4Axiom(x)。

定义37：有关量词逻辑公理1的定义
1962年译本
Q(z,y,u)≡(En,m,w)[n≤l(y) & m≤l(z) &w≤z &w=m Glx & w Geb n,y & v Fr n,y]
2000年译本
quator1AxiomCondition(z,y,v)n≤length(y),m≤length(z),w≤z.w=item(m,z)∧bound((w,n,y)∧free(v,n,y)

这个定义37是有关谓词逻辑量词的定义，涉及到自由与约束，实际上也涉及到谓词逻辑的公理模式。该定义中的字符z在y中不含约束变元，而y处在这样的位置，它中间的v是自由变元。所以，整个定义告诉我们的是：它相关于谓词逻辑公理模式Ⅲ中的公理1，该公理可应用的条件要求，如果z要代换y中的自由出现，那么就得保证不能出现约束z的变元。这个定义该修改为哪一种表达式为好，还真有点拿不准，暂且搁置。

定义38：依然是有关量词逻辑公理1的定义
1962年译本 2000年译本
L1-Ax(x) ≡ (Ev,y,z,n){v,y,z,n≤x &n Var v & Typn{z) & Form(y) & Q(z,y,v) &x=(v Gen y)Imp[]} quantor1Axiom(x)v,y,z,n≤x.vtype(n,v)∧stype(n,z)∧isFm(y)∧quartor1AxiomCondition(z,y,v) ∧ x=imp(forall(v,y),subst(y,v,z))

这个定义38依然与谓词逻辑公理1相关，其中的x是基于公理模式Ⅲ中的公理1通过代换而获得的公式。这样的公式表达为定义38的左式，定义38右式则表明，该左式可以理解为四个符号v,y,z,n的存在，但这些符号的存在需同时满足六个条件。
所以这个定义可以表述为：
L1-Ax(x) ≡ (v,y,z,n)(((v,y,z,n≤x) &(Var(n,v)) & (Typen{z)) & (Form(y)) & (Q(z,y,v)) &(x=Imp(forall(v,y),()))。

定义39：有关量词逻辑公理2的定义
1962年译本
L2-Ax(x) ≡ (Ev,q,p){v,q,p≤x & Var(v) & Form§ & v Frp &Form(q) &x=[v Gen (p Dis q)Imp[p Dis(v Gen q)]}

2000年译本
quantor2Axiom(x)v,q,p≤x.isVar(v)∧isFm§∧Free(v,p)∧isFm(q) ∧ x=imp(forall(v,or(p,q)),or(p,forall(v,z)))

这个定义39与谓词逻辑公理2相关，其中的x是基于公理模式Ⅲ中的公理2通过代换而获得的公式。这样的公式表达为定义39的左式，定义39右式则表明，该左式可以理解为三个符号v,q,p的存在，但这些符号的存在需同时满足六个条件。
所以这个定义可以表述为：
L2-Ax(x) ≡ (v,q,p)(({v,q,p≤x) & (Var(v)) & (Form§) & (Free(v,p) & (Form(q)) &(x=Imp[(forall(v,or(p,q)),or(p,forall(v,q)))。

定义40：有关公理模式Ⅴ中公理1的定义
1962年译本 2000年译本
R-Ax(x) ≡ (Eu,v,y,n)[u,v,y,n≤x & n Var v & (n+1)Var u & u Fr y & Form(y) & x=u Ex{v Gen [[R(u) * E(R(v))]Aeq y]}] reduAxiom(x)u,v,y,n≤x.vtype(n,v)∧vtype(n+1,u)∧free(u,y)∧isFm(y) ∧ x=exists(u,forall(v,equiv(seq(u))○paren(seq(v)),y)))

定义40是有关外延公理的，该公理陈述了一个类，是由其元素来判定的。这个定义中的x，是基于公理模式Ⅴ中公理1,通过代换而获得的公式。这样的公式表达为定义40的左式，定义40右式则表明，该左式可以理解为四个符号u,v,y,n的存在，但这些符号的存在需同时满足六个条件。
所以这个定义可以表述为：
L3-Ax(x) ≡ (u,v,y,n)((u,v,y,n≤x) & (Var(n,v) & Var(n+1),u) & (Free(u,y) &( Form(y) & (x=exist(u,forall{v equiv(seq(u) ○ paren(seq(v)),y)))。

定义41：有关公理模式Ⅴ中公理1对应的另一个定义
1962年译本
M-Ax(x) ≡ (En)[n≤x∧x=n Th z4]
2000年译本
setAxiom(x)n≤x.x=typeLift(n,sa)
对应于公理模式Ⅴ中公理1，还有一个定义41，和这个公理相对应的是一个判定数字z4，由此我们就有定义41。而这里的所谓判定数字，其实就是这个公理的哥德尔数。这个公理是集合公理，定义41中的x，也是依据公理模式通过代换而获得的。定义中的左式，起首的M即表述的这个公理，定义右式则表明，该左式可以理解为存在一个数字n，该数字n的存在需要满足两个条件，一个条件是n≤x，另一个条件是n相关于集合公理而得到类型提升。
由此，它最好是表述为：
Set-Ax(x) ≡ (n)（（n≤x）∧（x=typelift（n，z4））

定义42：谓词“x是公理”的定义
1962年译本
Ax(x)≡Z-Ax(x)∨A-Ax(x)∨L1-Ax(x)∨L2-Ax(x)∨R-Ax(x)∨M-Ax(x)
2000年译本
isAxiom(x)peanoAxiom(x)∨propAxiom(x)∨quantor1Axiom(x)∨quantor2Axiom(x)∨reduAxiom(x)∨setAxiom(x)
定义42中的x是公理，x何以是公理呢？则是由定义右式中的析取式所表达。
这个析取式定义可以表述如下：
isAxiom(x)≡peanoAxiom(x)∨mlogicAxiom(x)∨L1Axiom(x)∨L2Axiom(x)∨L3Axiom(x)∨setAxiom(x)。

定义43：二元谓词x是y和z的直接推论的定义
1962年译本
Fl(x,y,z)≡y=z Imp x ∨(Ev)[v≤x &Var(v) & x=v Gen y]
2000年译本
Immconseq(x,y,z)y=imp(z,x)∨v≤x.isVar(v)∧x=forall(v,y)
定义43给出了直接后承的定义，其中的x被看作是符号y与z的一个直接推论，这是对于二元谓词的一个定义。该定义左式是一个二元谓词，右式则是该谓词成立的条件，是一个满足析取的条件。
这个定义可以这样表述：
Isconsequence(x,y,z)≡(y=imp(z,x))∨v(v≤x)∧isVar(v)∧x=forall(v,y))。
定义44：谓词x是一个形式证明的定义
1962年译本 2000年译本
Bw(x)≡(n){0<n≤l(x)→Ax(n Gl x)∨(Ep,q)[0<p,q<n &Fl(n Gl x, pGlx, q Gl x)]}&l(x)>0 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

定义44又是一个谓词定义，表述“是一个形式证明”应该满足的条件，Bw为德文证明的缩写。这个定义右式告诉我们，一个形式证明是一个有限长度的公式序列，其中的每一个或者是公理，或者两个在前公式推出的直接推论。
于是定义44就可以描述为：
isproof(x)≡（(n){0<n≤llength(x))∧isAxiom(item(n,x)∨((p,q)(0<(p,q)<n )&consequence(item(n, x),item( p,x),item(q, x)&length(x)>0）。

定义45：x是对于y的证明的定义
1962年译本
x By≡Bw(x) & [l(x)] Gl x=y
2000年译本
proveForFn(x,y)isProofFigure(x)∧item(length(x),x)=y。

定义接近尾声了，称作原始递归函数的，这应该是最后一个定义了。这将近全部定义的列出，似乎在哥德尔的字符中看到一点曙光，好像有点接近他的思路了。这个定义实际上也是一个谓词，说一个公式x是另一个公式y的证明得满足两个条件，似乎重复了定义44。但定义44没有讲那个x是那个客体的证明，定义45则明显强调了客体y。所以满足这个二元谓词的定义，首先自然得是一个形式证明，此外，这个形式证明长度中有一项,，其实就是最后一项恰好就是y。
于是我们就有这样的定义45：
prove(x,y)≡(isproof(x))∧(item(length(x),x)=y))。

定义46：唯一不是原始递归的最后一个定义-可证定义
1962年译本
Bew(x)=(Ey) y B x
2000年译本
provable(x)y.proofFor(y,x)
这篇博文终于如愿完成，弄到了哥德尔定义的最后一个，得暂且歇息一下了。
说x是一个可证公式，那是什么含义呢？那就是说存在某个y，它对于x是可证的。
这可以定义为：
Isprove able(x)≡y(proof(y,x)。
这个定义的给出，让人品尝到一点自指悖论的味道了。说x根据y可证，结果掉头又回到了x，但这个结果怎么出现的，有一条什么样的线索在导致思路的循环。还需要花功夫对着字符发呆。
落笔至此吧，且待下篇。