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

从牛年之初，就被哥德尔原著英译本缠上。导论的阅读，覆盖了牛年的春天。正文浏览之际，又碰上广州的荔湾疫情。

春日已过，入夏时分，阅读之余，游兴萌生。思绪迁移到了疫情阻断的旅行，念想着到塞外风情的内蒙旧地重游，追怀那客逝他乡的苦命之人。想到就做，于是机票定好了，车也预定好了。可人算不如天算，恰好就是起飞前的一天，北京和内蒙地区挂起了暴风雨的橙色预警。可能就是预警吧，不会影响行程的。我好像有一种对媒体的天然不信任感，包括最有科学依据的天气预报，也受这个感觉的牵连，被放进了不信任列表名单之中。所以，依然将所有的行装都准备停当，管他什么预报，我只按原定计划出发。

谁知，清晨起来，真的是人算不如天算，短信已经传来了多项取消航程的消息。凡预定北京的当天行程，所有的航班一律停飞。我们的那个航班还更为决绝，干脆就取消，连改期的程序也免了。一次准备充分的旅行，就这么成为了泡影。这让我想到了一些精致利己主义的哲学家，讨论的什么实体概念，有些所谓物欲论者的什么论和什么公理，一副自信满满，人定胜天的气概，只觉得有些可笑。这个哲学感觉，以后有机会再谈，此处暂且打住。

挂起橙色预警

一、灾祸连连的盛夏七月

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

加拿大的极端高温

美国的山火连连

西欧洪水滔天

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

亚马逊森林

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

已读过哥德尔定义的1-30，我们继续前行，读他的定义31-46吧。

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

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

定义31-38比较图5

定义39-46比较图6

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

定义31：代换概念

定义32：蕴涵 合取 析取 存在

1962年译本                            2000年译本

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

定义33：类型提升

这个定义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)))ⁿ

定义34：皮亚诺公理

1962年译本   

Z-Ax(x)≡(x=z₁ ∨ x=z₂ ∨ x=z₃)                        

2000年译本

peanoAxiom(x)(x= pa₁∨x=pa₂∨ x=pa₃)

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

peanoAxiom(x)≡(x= pa₁∨x=pa₂∨ x=pa₃)

定义35：从命题逻辑公理序列得到的公式

1962年译本                            

A₁-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) ≡ A₁-Ax(x) ∨ A₂-Ax(x)∨ A₃-Ax(x) ∨ A₄-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的定义

这个定义38依然与谓词逻辑公理1相关，其中的x是基于公理模式Ⅲ中的公理1通过代换而获得的公式。这样的公式表达为定义38的左式，定义38右式则表明，该左式可以理解为四个符号v,y,z,n的存在，但这些符号的存在需同时满足六个条件。

所以这个定义可以表述为：

L₁-Ax(x) ≡ ($v,y,z,n)(((v,y,z,n≤x) &(Var(n,v)) & (Type_n{z)) & (Form(y)) & (Q(z,y,v)) &(x=Imp(forall(v,y),()))。

定义39：有关量词逻辑公理2的定义

1962年译本

L₂-Ax(x) ≡ (Ev,q,p){v,q,p≤x & Var(v) & Form(p) & 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(p)∧Ø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的存在，但这些符号的存在需同时满足六个条件。

所以这个定义可以表述为：

L₂-Ax(x) ≡ ($v,q,p)(({v,q,p≤x) & (Var(v)) & (Form(p)) & (Free(v,p) & (Form(q)) &(x=Imp[(forall(v,or(p,q)),or(p,forall(v,q)))。

定义40：有关公理模式Ⅴ中公理1的定义

定义40是有关外延公理的，该公理陈述了一个类，是由其元素来判定的。这个定义中的x，是基于公理模式Ⅴ中公理1,通过代换而获得的公式。这样的公式表达为定义40的左式，定义40右式则表明，该左式可以理解为四个符号u,v,y,n的存在，但这些符号的存在需同时满足六个条件。

所以这个定义可以表述为：

L₃-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 z₄]

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，z₄））

定义42：谓词“x是公理”的定义

1962年译本

Ax(x)≡Z-Ax(x)∨A-Ax(x)∨L₁-Ax(x)∨L₂-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)∨L₁Axiom(x)∨L₂Axiom(x)∨L₃Axiom(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是一个形式证明的定义

定义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，但这个结果怎么出现的，有一条什么样的线索在导致思路的循环。还需要花功夫对着字符发呆。

落笔至此吧，且待下篇。