前言

前言 数学踏上新的征程

人们常说,刚刚过去的一个世纪是数学真正的黄金时代。数学在 20 世纪的进步比先前所有的世纪加起来还要大。然而,刚刚开始的这个世纪也可能同样是数学发展的好时候。或许,数学在这个世纪的变迁会和 20 世纪一样巨大,甚至更为惊人。引发这种想法的信号之一是一场渐变:自 20 世纪 70 年代开始,数学方法的基石——证明的概念逐渐发生演变,让一个古老却有些被人忽视的数学概念重新回到了舞台中央,这就是“计算”。

计算能成为引发革命的导火索,这看起来有点不合常理。算法,比如做加法和做乘法的算法,常常被视为数学知识中最基础的一部分,做计算也经常被看成是缺乏创造性的枯燥工作。数学家们自己对计算也颇有成见,勒内·托姆就曾说过:“我的论述中很大一部分属于纯粹的猜想,大家基本上可以把它们看成是梦话。我接受这种定性……如今,世界上到处有这么多学者在做计算,难道有人做梦不是件好事吗?”用计算来做梦,大概还真有点难度啊……

不幸的是,对计算的偏见恰恰根植于“数学证明”这一概念的定义里。确实,欧几里得以降,“证明”的定义就是利用公理和演绎规则构建的一套推理 。然而,要解决一个数学问题,仅仅需要构建一套推理吗?数学的实践难道没有告诉我们,解决问题需要把推理的步骤和计算的步骤巧妙地融合起来吗?公理化方法若局限在推理中,它所展现的数学视野恐怕也会十分狭隘。正是因为人们对约束过多的公理化方法多有批评,才让计算有机会重新出现在数学的舞台上。现在,已有一些研究工作(它们之间未必有关联)渐渐开始质疑推理高于计算的优势地位,并倡导一种更为平衡的观点,让两者互为补充。

这场革命让我们重新考量推理和计算之间的关系,同时也促使我们重新审视数学与物理学、生物学等自然科学之间的对话,特别是数学为何能在这些学科中发挥难以理解的强大作用这一古老问题,以及自然理论的逻辑形式这一全新问题。此外,这场革命给“分析判断”和“综合判断”等哲学概念带来了新的火花。它还让我们反思数学与计算机科学之间的关系,而且数学似乎是唯一一门不需要借助机器的科学,它为什么如此独特?

最后,最振奋人心的是,这场革命让我们隐约看到了一些解决数学问题的新方式,它摆脱了过去的技术强加给证明长度的枷锁——数学也许正踏上新的征程,去探索从未涉足的全新领域。

诚然,公理化方法的危机并不是凭空出现的。从 20 世纪上半叶起就有许多先兆,特别是两种理论——可计算性理论和构造性理论的出现。这两种理论本身虽然没有质疑公理化方法,却重新确立了计算在数学大厦中的地位。在讨论公理化危机之前,我们会简要回顾这两个概念的历史。不过,还是让我们先上溯远古,探寻计算这一概念的起源,看看古希腊人对数学的“发明”过程吧。

目录

  • 版权声明
  • 译者序
  • 致辞
  • 前言
  • 第一篇 古老的起源
  • 第 1 章 从史前数学到希腊数学
  • 第 2 章 计算两千年
  • 第二篇 古典时代
  • 第 3 章 谓词逻辑
  • 第 4 章 判定性问题与丘奇定理
  • 第 5 章 丘奇论题
  • 第 6 章 为计算树立数学地位的尝试——λ 演算
  • 第 7 章 构造性
  • 第 8 章 构造性证明与算法
  • 第三篇 公理化危机
  • 第 9 章 直觉主义类型论
  • 第 10 章 自动化证明
  • 第 11 章 证明检验
  • 第 12 章 学界新进展
  • 第 13 章 工具
  • 第 14 章 公理的终结?
  • 结语 旅程的尾声
  • 附录一 人物简介
  • 附录二 参考文献