zzx217的个人博客分享 http://blog.sciencenet.cn/u/zzx217

博文

w一致的故事和符号世界的对应——哥德尔读后之24

已有 1680 次阅读 2021-11-8 16:50 |系统分类:科研笔记

 w一致的故事和符号世界的对应——哥德尔读后之24

 

听到来自脸书改名元宇宙的消息之后,又从一份外刊中得知,这元宇宙的概念其实由来已久。最早可以追溯到柏拉图的洞穴假说,最晚也要追溯到美国上世纪90年代的一本科幻小说《雪崩》snow crash,一本厚厚的长篇科幻小说。还没有时间来看这部几十年前的科幻长篇,但据说这个作者史蒂芬森很是了得。它的雪崩长篇,正是今日“超元城市”,即所谓虚拟实景技术的原创性构想所在。以致今天的虚拟世界,让人生有了远不同于实在世界的另一类空间。在这个空间里也有了公民,有了大使馆,有了很多超越尘俗的神奇梦想(参见史蒂芬森《雪崩》导读)。

柏拉图洞穴 洞穴简图.jpg

洞穴2.jpg

雪崩超元城

 雪崩幻想.jpg

元宇宙想象

 元宇宙.jpg

不过,我听到这元宇宙概念时,首先想到的倒不是虚拟世界,因为这个“元”字,我首先想到的是,由希尔伯特和哥德尔等数学家逻辑学家开创的元数学、元语言或者元逻辑观念。也许,这个语言中的“元”,其实不是科幻小说家的原创,而是哲学家、数学家和逻辑学家的原创。例如柏拉图,就是一个推崇数学的哲学家,而哥德尔则因为他的两条定理,影响到元数学的整个规划与哲学。所以,现在为人所知的元宇宙的“元”,雪崩设想的所谓超元城市中的那个‘’元‘’,数学家和逻辑学家早就从数学和逻辑的角度予以了探究。并且,这个探究产生了数学和逻辑学的巨大变革,如同雪崩影响到计算机的虚拟技术一样。

哥德尔的原著实在难读,但人智对于元的探求似乎总是一个动力在推你前行。从内蒙返回广州,漫看闲书,又回到原先的原著解读了,

博文880的读后之20,解读到标号(8),感觉得关注一些背景性的东西,于是停下来去理解基本观念。这一停,从880穿越到893了。自媒体的文字表述让你随心所欲,这感觉很好。你可以紧跟着原著文本,用文字来表述对于文本的理解。你也可以随时离开原著文本,用另外的阅读来强化对于原著文本的理解。文武之道,一张一弛。文字之道,似乎也有个类似的一离一即。离开原著文本一段时间,现在重回原著了,自然先要重温原著标号(8)之前的几个标号。

一、标号(5),(6)和(6.1)的回顾

先看定义(8.1),

Q(x,y)≡Ø(proofFormulac(x,subst(y,19,number(y)))

直观上,Q(x,y)它的寓意是,x对y(y) 在w一致c下不可证。那么,它为什么不是可证公式呢?我们先回到哥德尔不完全性定理证明的起点,标号(5)的定义上来。

标号(5)告诉我们,x序列在w一致c下可证的定义。那就是,一个公式x在w一致c下可证,其进行证明的符号串,必须是某个长度为n的公式序列,该序列满足以下条件:

1)它的构成项是有限的,长度为length(x);

2)构成项是在w一致c公式类下的公式;

3)构成项或者是公理,或者是依据公理和规则从在前公式导出的直接后承;

4)该序列长度n>0。

这个标号(5),是证明哥德尔第一不完全性定理的第一个标号。它所定义的‘’是一个证明序列‘,表达的是一个原始递归谓词。该谓词和标号(5)右式的符号串等价。而这个符号串,实际上是一串数字。’所以,我们对于哥德尔第一不完全性定理的证明,是从算术角度或者说数论角度来着手的。这个证明的过程看起来是公式或者公式序列,但这些公式和公式序列都被配以哥德尔数。那就是说,由逻辑符号联结的这些客体,都是一个一个的数字,而且是原始递归的。

例如:

谓词is axiom(term(n,x))表示,序列中第n个x是公理,这里的x就是处于序列第n个位置上的数字。

谓词immediConseq(term(n,x),term(p,x),term(q,x))表示,序列中的x处于序列中的第n个位置,它是在前的p和q的直接后承。所以,也可以说,x是其数字为p和q直接后承的一个数。

谓词length(x),那就更明显,表示序列x的长度,如果length(x)>0,则表示x的长度数字大于0,自然这个谓词就是一个数字。

接之标号(6)又更具体地说明,一个w一致c公式类下的可证公式,就是证明序列中的最后一个公式,这类似于定义45。这个标号中的符号串,依然也是用数字来说明。

该标号可以解读为,数字为x的公式序列是数字为y的公式的一个证明。解读得更为详细一点则是,x作为一个符号序列,它等价于一个合取式。这个合取式有两个合取支,一个是,x是一个在w一致c公式类下的证明序列;另一个是,x序列长度中的最末一项为y,y正好是序列x所要证明的公式。这个标号(6),恰好就是哥德尔定义45的一个特例,差别仅在于具有w一致c公式类条件。

现在轮到相关于哥德尔46个定义中的最后一个定义46了,这个相关于哥德尔定义46的新定义,在哥德尔第一不完全性定理证明序列中,标号为(6.1)。

标号(6.1),几乎完全等同于哥德尔定义46。它表达:x可证。也就是,x是一个可证公式的数,等价于存在一个数y,y是x的一个证明序列。在整个哥德尔46个定义中,前面45个定义的客体,都是原始递归的,唯有这最后一个定义46,不是原始递归的或者说是可判定的。

 

把这个标号(6.1)给出的可证定义,和在前46个定义中的定义46相比较,哥德尔认为标号(7)和标号(8)是显然成立的。但你似乎对哥德尔的这个‘’显然‘’,会有一点茫然的感觉。行家一看可能就是显然,但对于哥德尔的那些稀奇古怪符号仅略知一二的读者来说,想要获得显然的感觉,体验点显然的味道,可并不是一件容易事。至少,你要悟出些符号的门道,才有可能品尝出所谓‘’显然‘’的味道。

 

二、哥德尔原著英译本标号(7)和(8)显然成立么?

(一)标号(7)可以说是显然的

先看标号(7),它显然成立么?我们来解读这个标号(7)。

标号(7)

"x(provablec(x)≡x∈consequence(c))       (7)

这个公式标号为(7)

 

继续按照常规出牌,撇开量词,把定义拆分成左式和右式。

左式:provablec(x)

公式x可证。

说一个具有递归和w一致性的公式类c中的公式可证,需满足右式所描述的条件。

右式:x∈consequence(c)

只要x属于w一致c中的直接后承即可,这明显先根据标号(5)的证明序列定义。一个客体可证,首先得有一个证明序列。而要有一个成立的证明序列,至少得满足其析取中某一个选言支,而属于某个直接后承正好是其中一个要求。直接后承又是由在前两个公式,根据公理和推理规则推导而来,于是直接后承中的每一个公式,依据标号(6),就都是证明公式,这又用到标号(6)。再根据(6.1),x存在着证明公式y,就表明x可证。

这是依据在前标号定义的推演,如果再往前看原著文本,在哥德尔不完全性定理给出之前,哥德尔在文本中已经预设了c是任意公式类,并且用consequencec来表示公式的最小集合,该集合包括c的所有公式和所有公理,并在“直接后承”关系下封闭。依据这个在前的预设,标号(7)的表达式显然成立,就是好理解的了。不过标号(7)前置全称量词约束变元x,为什么要加上全称量词?大概是x中的所有变元吧?姑且存疑。

 

那么,标号(8)呢?标号(8)的显然性还真不那么显然,似乎要多花费点文字。标号(8)是个蕴涵式,蕴涵式前件的可证无下标,后件则带有下标w一致c。

我们来看标号(8):

"x(provable(x)→provablec(x))       (8)

这个公式标号为(8)。

 

这个标号(8),左式可证不带下标,右式可证带下标w一致c。这表明,前件的可证,是条件更为宽泛的可证,后件的可证则是带有特殊条件,即w一致条件的可证。这样,不带w一致条件的可证和带有w一致条件的可证,就得来点比较和分析。至少,你得对w一致有点感觉才行。好在哥德尔的思路明晰,他在给出哥德尔定理和证明之前,已经陈述了为这个定理给定的前提假定,那就是w一致,一个否定性的存在假设。

 

公式类c称作w一致,如果不存在类符号a使得

"(n)(subst(a,v,number(n)∈conseq(c)∧not(forall(v,a))∈conseq(c)

 

这段符号串先做一个简单说明:

1)a是类符号,所谓类符号,即是一元关系符号,仅有一个自由变元的公式;一般称之为描述性质的语句中的谓词。

2)v是公式a中的自由变元

3)number(n),根据哥德尔定义17,这是对于数字n的数字符号number-sign

4)conseq(c),这是哥德尔已经预设的公式类,直接后承集合或者可证公式集合;

 

在前已有多篇理解哥德尔文本的博文,对w一致已有一些讨论,行文至此,又要涉及到w一致了。再增加一点相关理解似有必要,于是有了以下几段有关w一致的新增文字。

理解w一致,常常是从w不一致开始。哥德尔研究高手斯穆里安,在解释这个w不一致观念的时候,先讲了三个故事。其中第二个故事更简单更有趣,我在这里来做一个辗转引用。斯穆里安也喜欢引用,他的第三个故事就引用了另一位数学家哈尔莫斯为w不一致构思出来的妙趣文字。很传神,却抽象了一点,还是用第二个故事为好。

设想我们都是永恒不朽的生命,但也是要体验凡尘生活的仙人,我们居住和徜徉在宇宙空间之中。这个空间,有无限多个为我们服务的银行,银行的数目似乎和我们生命的永恒一样无穷无尽。把这些银行做成一个列表,可以用自然数下标永无止境地排下去,从银行1,银行2,…银行n……,一直排到宇宙的无穷深处,没有尽头。

我们再设想,其中的某个银行i给你一张大额支票,支票上注明“在某个银行可以支取”。拿着这个大额支票,你去银行1,支取不了。银行2,还是支取不了。你一个接一个地到不同银行支取,都不能兑现。甚至你已经尝试过成万上亿个银行,都不能兑现。但你是永恒的,银行是无止境的,你可以伴随着时光,不断地寻求支票的兑现。所以,我们似乎也不能证明这张支票是无效的。因为你的永恒和银行的无限,使得你有永远也走不完的银行。也许,总有无限之中的下一个银行,可以在你生命的下一个时刻将这个支票兑现(参见斯穆里安《数理逻辑入门》第219页)。

这个故事似乎告诉我们,所谓w不一致,就如同这个故事中的支票一样,它写有“可兑现”的文字,但你却在银行里怎么也兑现不了,支票上的可兑现文字和使用支票的效果是不一致的。不过,那个银行数目的无限性假定,还有那个赋予你的生命永恒假定,似乎总在给你留存一点也许可以兑现的期待。

这个故事告诉我们,也许,正是因为这个无限和永恒,造就了某种不一致(参见斯穆里安《数理逻辑入门》第218页)

但逻辑并不等同于故事,我们还是得给w不一致一个精确的定义。

 

(二)w不一致w一致

斯穆里安是这样定义w不一致的。

假设S是其所有公式都属于皮亚诺算术的系统,S中有公式F(w),w是以自然数为变域的自由变元。再假设带有上横线的数字符号,……是指称自然数0,1,2,…n…的数字,由这些上横线的符号构成公式F(,……。

由此我们可以定义w不一致如下:

称系统S是w不一致的,如果公式F(w)使得,公式$wF(w)可证,但所有另一类的公式F(,……皆是可驳斥

有了这个w不一致,我们可以简单地说,如果系统S不是w不一致,那么它就是w一致。这也可以用斯穆里安的换句话说来表示:

换句话说,如果公式$wF(w)在S中可证,那么就至少存在一个数字n使得公式在S中不可驳。这时候,我们就可以称S是w一致。

斯穆里安的这个换句话说,其实等价于哥德尔在其原著英译本中所表达的东西:

公式类c称作w一致,如果不存在类符号a使得

 

"(n)(subst(a,v,number(n)∈conseq(c)not(forall(v,a))∈conseq(c)

 

黑体字中那长长一串中英字母符号,也可以翻译为斯穆里安的‘’换句话说‘’。我们先解读这个符号串,然后来推测它们的等价。

w一致的系统中,不存在一元关系公式a,即所谓表达性质的公式a有以下两个合取支所描述的结论。

合取支1)a中的自由变元v代入全部变域所获得的公式a=F(v),属于可证公式类。其中的number(n),是对于数n的数字表示,这个符号表示与斯穆里安用上横线表示相应数n的表示法是一样的。

合取支2)则是说,一个否定的公式表达式not(forall(v,a)),它其实就是对于a的一个全称否定公式Ø"vF(v),它不属于可证公式类,也就是,它是斯穆里安定义中的可驳公式。

把这两个合取支解读得更直白一点,哥德尔定义中的这个类符号a,既可以指包含变元v的一元公式a=F(v),也可以单就变元v而言。把哥德尔的那个有点陌生的属于符号,换成更直白的可证符号├,用大写的谓词符号A替代小写的a,则有合取支1)的转换式:

"(n)(subst(a,v,number(n)∈conseq(c) = ├A(0),├A(1),├A(2), ├….

 

合取支2)则可以转换表示为:

not(forall(v,a))∈conseq(c) = Ø"vA(v)

 

不存在一个公式a使得上述两种情形全都可证,这被哥德尔和《元数学导论》的作者克林称作w一致(参见《元数学导论》第227页)。

再来看康先生对w一致的定义:(参见《可能世界的逻辑》第10页)

系统T是w一致的,当且仅当,如果T├Φ(,…则T$xØΦ(x)

康先生的这个定义类似于哥德尔和克林的方式,又好像和斯穆里安的定义挂了钩,因为他也使用了上横线的数指称方式,用形式替身来表示数n。他的定义方式和斯穆里安的方式更为接近一些,那个不可证的公式T$xØΦ(x),其实就是斯穆里安定义w一致的后件所呈现的公式。我们继续把以上有关w一致的定义和斯穆里安定义再做点比较,以强化我们对w一致观念的理解。而且,从进一步的比较中可以感觉到,上述几种定义方式,其实和哥德尔的原创定义几乎全都一脉相承。

斯式定义,预先给定了数字对变元的代入,对任意自然数n,他用这样的上横线方式来指称n的数字,在一元公式的情形下,公式F(w)中的自由变元仅仅w。这就可以用F()来表示,那些用代入w每一处自由出现所得到的公式,如上所示的A(0),A(1),A(2)…等等,都可以用这个方式简化表述,康先生直接采用了这样的标记模式。这样的表达也就被看作是普通算术命题的形式替身。由此就有了斯穆里安w一致的定义:

若S中有一个可证公式$wF(w),则至少会有一个数n使得公式在S中不是可驳。这时候的S,就是w一致。

也就是说,我们在S中有可证公式├$wF(w),这个公式的自由变元w中至少有一个变元使得这个公式可证。如果这个条件满足的话,这就表明,在w作为自由变元的变域中,一定至少有一个数n保证公式$wF(w)可证,而给n配置的数名是,由这个数名在S中构成的公式不是可驳,这就保证了S的w一致。

由此可知,w一致性就是说,在一个算术系统中有一个表达性质的公式,这个公式的性质对于一个特定的数是可证的,但对于每一个特定的数,则并非是可驳的,也就是不是不可证的。斯穆里安编造了一个w不一致的银行支票故事,这个故事设想了无限的银行,因为无限,我们不可证支票无法兑现,但我们又认定,所有的银行中总有一个银行可兑现是可证的。把这个故事稍加改变,大概就可以是一个w一致的故事。

其实只是一个轻微的改变,设想有那么一个银行Bn,它可以兑现支票,我们把它对应数名和可兑现性质构成公式,它也有性质“可兑现”。但这个一元公式可证么?我们似乎不知道。我们顶多能够知道的,这个公式似乎既不能可证,也不是可驳。

这个解读好像还有点玄,此处再用克林关于w一致所做的一段评论,继续来理解一下它的寓意。克林在《元数学导论》中比较了两种一致,一个是简单一致,另一个就是w一致。

他说:

在上述权宜性论证中所做的假设,即如果A或者ØA假,它便不能在系统内证明,在现在的元数学论证中便应换以一个元数学的等价假说,就如果A假则A不能证而言,这个等价物就是系统的简单无矛盾性或者简单一致性。就如果ØA假则ØA不能证而言,我们需要一个更强的条件,叫做w一致性,它可定义如下:

一个形式系统称作w一致,如果没有变元x及公式A(x)使得下列各命题为真:

├A(0),├A(1),├A(2),….Ø"xA(x)

(换句话说,如果不是既Ø"xA(x),又对每个自然数n都有├A(n)),反之,如果对某个x及A(x)使得所有A(0),A(1),A(2),…以及Ø"xA(x)全是可证,则该系统称作w不一致(克林《元数学导论》第227页)。

所以,w一致是从否定角度,来思考系统中的公式客体和公式中的变元。它的一致性似乎是体现在:你不能在断定一个一个特定数字具有某个性质可证的同时,又断定所有个体数字不具有某个性质的可证。一个具有w一致的系统,没有这样的公式,也没有这样的变元,能够接受这种不一致的可证断定。这种否定式断定,颇类似同时否定了一个特称命题和全称命题的合取,自然就是w一致。

如果能够编一个通俗的故事,如同斯穆里安说明w不一致那样的银行故事,来说明w一致,那就有点意思了。我还是尝试把那个数学家哈尔莫斯编的小故事翻转过来,他编的依然是w不一致,我不揣鄙陋,想将它改为w一致的故事。但很遗憾,这个w一致的故事难编。那就依然用哈尔莫斯的w不一致的小故事,来暂停w一致的讨论吧。

Jane是一个具有w不一致的母亲,她几乎不允许她的孩子做任何事情。这些事情可以列成一个长长的没有尽头的清单,从编号1直到无穷。她对孩子说:你不可以做1,不可以做2,不可以做……这列表上无穷多事情。孩子看到这么多不可做的事情,就问母亲:难道就没有允许我做的事情么?母亲回答:有啊!有允许你做的事情啊。但不是这,也不是那,也不是……。

这还是w不一致的故事,能够有一个通俗说明w一致的故事么?我费神想了想,还是拿不出像样的文字,期待有高手把这样的故事编出来。

 

(三)标号(8)和(8.1)解读

有了以上w一致的讨论,我们来看标号(8)是否如同哥德尔所说,是显然成立的。

标号(8):

"x(provable(x)→provablec(x))       (8)

 

这个公式标号为(8)。

这个标号(8),左式可证不带下标,这就是上文提及到的,右式可证带下标w一致c。这表明,前件的可证,是另一个条件下的可证,后件的可证则是带有w一致条件的可证。这样,不带w一致条件的可证和带有w一致条件的可证之间,有一个前者导出后者的蕴涵关系。

而这个标号(8)的前件provable(x),不正好就是哥德尔定义46么?它等价于存在一个公式序列y,y是x的一个证明。而这个定义恰好就是在哥德尔的系统P中,序列y也好,可证公式x也好,都处在哥德尔的P系统中。那么,在P系统条件下的x可证,能够蕴涵在w一致条件下的可证么?这需要设想一下一个语言的两个集合,可证公式的集合和可驳公式的集合,在这两个集合的前提之下,斯穆里安鼓捣出一个正确性观念。那就是,如果一个系统中,可证公式的集合皆为真,可驳公式集合皆为假,这个系统可称之为“正确的”。这个正确性大致类似于一个系统的可靠性,而这个正确或者可靠,正是哥德尔系统P具有的元数学性质。在P的正确性性质下,再给P一个w一致,那就是在收紧系统中公式为真或者为假的范围。

由此而可以表明,正确性之下的系统P,比w一致更强。于是,我们在标号(8)中的蕴涵式,就是具有正确性的P蕴涵着增加w一致的系统P,这个标号(8),由此而就有了显然性。

有了在前的定义和标号(7)(8),现在开始定义一个二元关系了,这就是标号(8.1)。

 

Q(x,y)ØproofFormulac(x,subst(y,19,number(y)))         (8.1)

 

这个二元关系被定义为对证明序列x的一个否定,定义右式的变元x是一个公式序列,但这个公式序列x却并不是那个变元y借助代入而形成公式的一个证明,一个在w一致条件下的证明。变元y为什么不是变元x的证明序列呢?这需要依据哥德尔定义17和定义31来说明,先来解读由subst紧随的,公式序列x之后的符号串subst(y,19,number(y))。

哥德尔定义17在解读w一致时,已经多次提及过,这里再一次用到这个定义17。这个符号串number(n),就是表达数字n的数字符号number-sign,可以用上横线的符号表达。用到y上,则这个变元y的数字符号就是

哥德尔定义31则是对于sbust的定义,该定义可以用来解释公式subst(y,19,number(y))。它是这样一个公式,把公式变元y作为自由变元用y的数字符号代入后形成。括号中间的19,是变元y的哥德尔数,变元x的哥德尔数是17。变元y经过代入运算之后,依据哥德尔在前对于代入的说明,则subst(y,19,number(y)),就是将在y中出现的自由变元19代入之后获得的公式。这个代入的结果,使用哥德尔原著2000年译本的说法,实际上就是一个有自指意味的公式y(y)。由此,这个标号(8.1)给出的二元关系定义,直觉地看,就是在表示:二元关系Q(x,y)被定义为,x不是在w一致条件下y(y)的证明。

说有一种二元关系,是对于证明的否定关系,这是在放出什么信号呢?因为这个否定的二元关系来自于哥德尔定义17和定义31,而定义17和定义31所定义的关系是原始递归的,这就可以得到,Q(x,y)也是原始递归的。于是,哥德尔在前给出的可表达性定理就发挥作用了,我们的二元关系Q(x,y)似乎正对应于这个可表达性定理4,此处再重述一下这个可表达性定理4:

 

R(x1,x2,…,xn)→provable(subst(r,u1,…,un,number(x1)…number(xn)))          (3)

ØR(x1,x2,…,xn)→provable(not(subst(r,u1,…,un,number(x1)…number(xn))))     (4)

 

依据这个可表达性定理4,于是我们就有关系q,它带有自由变元17和19,构成了哥德尔不完全性定理证明中的标号(9)和标号(10)。

 

三、标号(9)和标号(10)解读

标号(9)是一个如同标号(8)那样的蕴涵表达式,前件为x与y的非证明公式关系,即Q(x,y)。由这种关系,衍生出证明和可证这两个有关证明概念间的关系。有点奇怪的是,一个悖论式公式的非证明公式关系,竟然导引出在递归w一致性c条件下肯定的可证性质。

标号(8.1)的代入,是一个自由变元的代入,标号(9)增加了一个变元。但标号(9)与(10)不是定义,而是蕴涵式。依然按照标号(8.1)的方式进行解读,先整理各个符号的常规理解。

先看标号(9):

(Ø(proofFormulac(x,subst(y,19,number(y)))

(provablec(subst(q,(17,19,number(x),number(y)))   标号(9)

 

这个公式为标号(9),它告诉读者,在Q(x,y)关系下,原始递归谓词”x不是相关条件下的证明公式”,这样的谓词该蕴涵着什么呢?

 

符号q是后件中的关系符号,它带有两个自由变元x和y,分别配以哥德尔数字17和19。而subst这个符号串,则是一个元数学的代入符号。至如那个number(x)和number(y),则是与自由变元17和19同等类型的数字符号,也可以表示为

由此,这个标号(9)的后件就可以解读为:

当我们用number(x)来代入变元17,用number(y)来代入变元19的时候,关系符号q实际上做了这样的变换。那就是,在x中出现的所有17中的自由变元,都代换为number(x)。在y中出现的所有19中的自由变元,都代换为number(y)。在这种情形下的二元关系q,其实就被标号(8.1)揭示的非证明公式关系所蕴涵。

依据什么呢,回看标号(3)和(4)的表达定理,这个结论就十分清楚。因为标号(9)的前件就是Q(x,y)的二元谓词,而在标号(3)中,当n=2的时候,不正好就是标号(9)的表达式么?所以,这个标号(9)自然就成立。原始递归关系或者谓词的条件,也就自然蕴涵着这样关系下的代入运算是可证的。哥德尔似乎在这里又在显示某种符号世界的奇妙,可表达性定理4中的标号(3)似乎绝配似的对应哥德尔证明过程中的标号(9)。

再看标号(10)

标号(10)的表达式:

 

((proofFormulac(x,subst(y,19,number(y)))

(provablec(not(subst(q,(17,19,number(x),number(y))))   标号(10)

 

这个公式为标号(10),刚才的标号(9)为否定式的前件,现在的标号(10)则为肯定式的前件,依据标号(8.1),标号(9)可以表达为Q(x,y)为前件,标号(10)则可以表达为ØQ(x,y)为前件。它们似乎是在表明,两类互为否定的证明公式proofFormula和可证概念provable之间的同一种蕴涵关系。

 

标号(10)解读

有了标号(9)的上述解读,标号(10)的解读就有了样板,但因为(10)的前件是一个否定式,在这里依然需要一些说明。

但这个解读,因为有标号(9)做铺垫,就可以简化许多。特别体现逻辑与数学中的对应特性的是,如同标号(3)对应于标号(9)一样,标号(4)似乎绝配似的对应标号(10)。标号(3)和(4)除了自身的对应,它们还分别对应了标号(9)和(10)。标号(4)的公式前件,恰好就是否定的。当其中的变元数字n=2的时候,正好表达的就是标号(10)的结果。

这篇博客,又是够长的了,从标号(10)到哥德尔不完全性定理证明的最后一个标号(16),恐怕还有一段长长的文字理解。这一次的估计应该不会错吧,从标号(11)到标号(16),不会再有什么停顿,一篇就该完成这哥德尔第一不完全性定理的阅读任务吧。

 

 

 

 

 

 

 




https://wap.sciencenet.cn/blog-3478957-1311512.html

上一篇:存在 列表框-按钮=滚动条——Python学习笔记之25:
下一篇:宇宙时空 符号世界 对应引理——哥德尔读后之25
收藏 IP: 120.230.79.*| 热度|

0

该博文允许注册用户评论 请点击登录 评论 (0 个评论)

数据加载中...

Archiver|手机版|科学网 ( 京ICP备07017567号-12 )

GMT+8, 2024-5-21 08:03

Powered by ScienceNet.cn

Copyright © 2007- 中国科学报社

返回顶部