您的位置 : 首页 >> 计算机与互联网电子书

计算进化史 改变数学的命运 Les métamorphoses du calcul

下载方式

本书作者:

 Les métamorphoses du calcul

主要想讨论的是计算对证明的重要性。对“证明”这一概念的梳理比较清楚,尤其谓词逻辑和判定性问题的章节,提纲挈领,对理解语言哲学也有帮助。

以上是读后感,我的学习笔记如下

无论哪种推理,都是由一系列命题构成的,每个命题都是用先前的命题通过逻辑得出的,也就是按照“演绎推理规则”构造的。 P13

然而,即使有了这样的拓展,亚里士多德的逻辑对于表达某些数学表述来说还是太粗糙了。 P14

然而,计算却并没有从数学工作中消失——无论在哪个时代,数学家都提出了一些新算法来系统地解决某些类型的问题。 P15

对于90和21这两个数来说,欧几里得算法会在进行3次除法之后得到结果。 P16

这个定理由此拥有了它内在的价值,也就是我们今天所说的“平行线分线段成比例定理”〔4〕。 P17

计算进化史 改变数学的命运 Les métamorphoses du calcul 计算机与互联网电子书 第1张

弗雷格的逻辑弗雷格把斯多葛的一些概念又拿了出来:最突出的是在弗雷格的逻辑中,命题是由原子命题组成的,并通过“和”“或”“不是”“如果……那么……”等连词组合起来。 P26

而另一条则可以从命题“A和B”演绎出命题A。 P27

无论在数学上还是在日常生活中,这样的矛盾都是出错的信号。 P28

例如欧式几何,它先天地采用了不同于集合论的一套公理,但也可以转化为集合论。 P29

这些算法比欧几里得算法与加法算法的目标更高,因为它们可解决的命题的范围更大。 P34

这样一来,算法绝不会同时得出两个不同的结论,那么从构造上就保证了这个逻辑不会有矛盾。 P35

同样,为了解决判定性问题,丘奇和图灵就必须把计算本身变成研究对象。 P36

计算进化史 改变数学的命运 Les métamorphoses du calcul 计算机与互联网电子书 第2张这就意味着人类是自然界中最会计算的——自然界中的任何东西,动物、机器……都不会比人类算得更好了。 P41

第二个假设意味着,一个系统的状态要经过一定延迟后才能影响另一个系统的状态,而延迟的时间则与两个系统之间的距离成正比。 P42

他意识到,行星的轨迹呈椭圆形。 P43

在某些情况下,当我们对一个现象有了更深入的理解之后,它遵循某个数学定律的原因就不言自明了。 P44

这个由塔、球、测量时间的计时器、测量高度的量高器构成的物理系统,可以被视为一台计算机器。 P45

在这个“构造主义”(也称为“直觉主义”〔4〕)纲领下,数学家发现自己处于一个十分尴尬的境地:有些命题的已知证明必须依赖排中律,结果导致有人承认它们是定理,而其他人则不承认。 P52

欧几里得没能证明“平行公理”,并不意味着它就理所当然地成为公理了。 P53

这样一来,我们就明白了为什么“存在出境前的最后一站”对于认为它的意思是“我们知道出境前的最后一站是哪一站”的人而言不成立,而对于认为它说的是“应该存在出境前的最后一站,虽然不知道具体是哪一站”的人来说成立。 P54

而在使用证明检验程序时,我们会同时提出命题及其证明,程序只需要检验证明是否正确就行了。 P68

使用计算机却不能让它做加法——德布鲁因已经发现了这个矛盾,但他似乎对于在证明中使用更多的计算规则还心存疑虑。 P69

程序的长度和电路的体积都呈爆炸式增长,膨胀速度很可能还超过了数学证明。 P70

在1976年和1995年之间,这一证明正确与否仍留存一个争议:人们无法排除阿佩尔和肯普在撰写程序时会出错的可能性。 P76

我们可以考虑一下,命题的长度和证明的长度之间是不是有什么关联?对此而言,可计算性理论确实给出了一个答案,不幸的是,答案是否定的。 P77

如果这样证明的话,我们需要把乒乓球换成网球、铁砧或是独角兽,并无限次地重复这个实验。 P80

如果一套关于自然的理论不能做出可观察的预测,那它就只能是一种思辨而已,这样的理论没有理由“高人一等”。 P81

数学创造的知识与自然科学构造的知识之间有一个重要的区别。 P82

所以,数学进入工具时代,并不是让我们盲目信任使用的工具,而是让我们谨慎看待自己有时过度的自信——我们一样可能出错。 P83

一种新思想出现几年后,人们很自然地会思考它的意义,思考是否能将其放在尽可能大的框架下来表达。 P85

但迄今为止,根据这一理论提出的例子都是人为设计的——我们所知的方法还太过原始,无法证明那些真正的数学命题没有短证明,比如四色定理、黑尔斯定理等。 P87