数学哲学（五）

5.3 计算

直到最近，计算主题在数学哲学中还没有受到太多关注。这可能部分是由于在数论的希尔伯特式公理化中，计算被简化为皮亚诺算术中的证明。但这种情况近年来发生了变化。看来，随着计算在数学实践中重要性的增加，对计算概念的哲学反思将在未来几年的数学哲学中占据更加突出的地位。

丘奇的论文在可计算性理论中占据着核心地位。它说自然数上的每个算法可计算函数都可以由图灵机计算。

作为一项原则，丘奇的论文具有某种奇怪的地位。这似乎是一个基本原则。一方面，这一原则几乎被普遍认为是正确的。另一方面，很难看出如何从数学上证明它。原因是它的前件包含一个非正式的概念（算法可计算性），而它的后件包含一个纯粹的数学概念（图灵机可计算性）。数学证明只能连接纯粹的数学概念——或者看起来是这样。人们普遍接受的观点是，我们丘奇论文的证据是准经验的。为丘奇论文寻找令人信服的反例的尝试已经失败。独立地，已经提出了各种建议来以数学方式捕获自然数上的算法可计算函数。人们提出了一般递归性、赫布兰德-哥德尔可计算性、lambda 可定义性等概念，而不是图灵机可计算性。但这些数学概念都被证明是等价的。因此，用哥德尔的术语来说，我们已经积累了丘奇论文真实性的外在证据。

Kreisel很早之前就指出，即使一个论点无法被正式证明，仍然有可能通过对直觉概念进行严格但非正式的分析来获得其内在证据（Kreisel 1967）。克赖塞尔称这些练习为非正式的严格练习。 Sieg 的详细学术研究表明，这篇开创性的文章（Turing 1936）构成了对算法可计算性直观概念（Sieg 1994）的这种分析的一个绝妙例子。

目前，基础和计算哲学领域最活跃的研究主题如下。首先，人们投入精力发展自然数以外的结构的算法计算理论。特别是，人们已经努力获得丘奇论文的类似物，以进行各种结构的算法计算。在这种背景下，近几十年来在开发实数有效计算理论方面取得了实质性进展（Pour-El 1999）。其次，人类已经尝试解释除算法可计算性之外的可计算性概念。这里特别令人感兴趣的一个领域是量子计算领域（Deutsch et al. 2000）。

5.4 数学证明

我们非常了解形式证明和形式可证明性的概念、它们与算法可计算性的联系以及这些概念的管理原则。例如，我们知道，形式系统的证明是可计算可枚举的，并且健全（足够强）的形式系统中的可证明性受到哥德尔不完备定理的约束。但是，您在数学期刊中找到的数学证明并不是逻辑学家意义上的形式证明：它是（严格的）非正式证明（Myhill 1960、Detlefsen 1992、Antonutti 2010）。

首先，虽然在正式系统中可证明的句子集合总是可计算可枚举的，但我们对非正式可证明性概念的扩展知之甚少。卢卡斯 (Lucas 1961) 和后来的彭罗斯 (Penrose 1989, 1994) 都认为，非正式的数学可证明性超过了任何给定的正式系统中的可证明性。但他们的论点被广泛认为缺乏说服力。贝纳塞拉夫反对卢卡斯和彭罗斯，认为不能排除存在正式系统

时间

�

事实上，数学可证明性与可证明性在外延上是一致的

时间

�

，尽管我们不知道它确实如此（Benacerraf 1967）。其他人则认为，非正式数学可证明性的概念对于其扩展是否可计算可枚举的问题来说还不够清晰，无法有明确的答案（Horsten & Welch 2016）。

其次，对于一个论证是否符合数学证明的标准，尚未达成一致。根据所谓的公认观点，一个陈述的数学论证

p

�

如果论证允许有能力的数学家将其转化为正式的推论，则构成非正式的数学证明

p

�

来自普遍接受的数学公理 (Avigad 2021)。然后，可以将非正式的数学证明视为推导指标

p

�

（阿佐尼 2004）。但近年来，人们对数学证明标准的普遍看法受到了攻击。例如，有人认为，在达到逻辑上正确且非椭圆的一阶导数之前，非正式数学证明中原因的插值可能是一个无限的过程（Rav 1999，p.14-15）。其他人则对收到的观点进行了辩护，因此目前对这些问题进行了热烈的辩论（Tatton-Brown即将到来，Di Toffoli 2021）。

过去的几十年见证了数学证据的首次发生，其中计算机似乎起着重要的作用。四色定理就是一个例子。它说，对于每张地图，只需要四种颜色才能以一种具有共同边界的国家使用相同颜色的方式为国家着色。该定理在1976年证明（Appel等，1977）。但是证明区分了许多通过计算机验证的情况。这些计算机验证太长了，无法通过人类进行仔细检查。四种颜色定理的证明引起了关于这个问题的辩论。

收到的观点表明，数学证明会产生先验知识。但是，当我们依靠计算机生成一部分证明时，我们似乎依靠计算机硬件的正确功能以及计算机程序的正确性。这些似乎是经验因素。因此，人们可以得出结论，计算机证明会产生准经验知识（Tymoczko 1979）。换句话说，通过计算机证明的出现，证明的概念纯粹失去了先验性的角色。相比之下，Burge认为，由于我们接受计算机证明的经验因素在论证中并未作为前提出现，因此计算机证明毕竟可以产生先验知识（Burge 1998）。 （Burge后来撤回了此主张：请参见（Burge 2013，第31页）。

6. 未来

在20世纪，数学哲学的研究主要围绕数学对象的本质，控制它们的基本定律以及我们如何获得数学知识。这些是与传统的形而上学和认识论问题密切相关的基本问题。

在20世纪下半叶，科学哲学的研究在很大程度上摆脱了基本关注。取而代之的是，与科学知识和科学理解的增长有关的哲学问题变得更加核心。早在1970年代，就有声音认为，数学哲学应该发生类似的关注。拉卡托斯开始了数学概念进化的哲学研究（Lakatos 1976）。他认为，数学概念的内容大致以以下方式演变。数学家提出了一个深刻的猜想，但无法证明这一点。然后发现针对猜想的反例。作为回应，对猜想中一个或多个中心概念的定义被更改以至少消除反例的方式。仍然无法证明如此修订的猜想，并逐渐出现了新的反例。修改一个或多个中心概念的定义的过程将一次又一次地应用，直到找到猜想的证明为止。 Lakatos称此过程概念伸展。近几十年来，Lakatos的数学概念变化模型进行了修订和完善（Mormann 2002）。

几十年来，数学哲学应采取历史和社会学转变的观点仍然仅限于数学哲学中的某种边缘思维学校。但是，近年来，一方面，这种数学实践的新运动与另一方面的“主流”哲学之间的反对是柔和的。与数学实践，数学理论的演变以及数学解释和理解有关的哲学问题变得更加突出，并且与数学哲学的更传统主题有关（Mancosu 2008）。在未来的几年中，这种趋势无疑会持续下去。

例如，让我们简要介绍计算机证明的主题（请参阅第5.3节）。数学家面对计算机证明时所经历的不适的根源似乎是以下内容。 “好”数学证明应该做的不仅仅是说服我们某个陈述是正确的。它还应该解释为什么所讨论的陈述。这是通过谈到经常将不同数学领域联系起来的深层数学概念之间的深层关系来完成的（Manders 1989）。到目前为止，计算机证明通常仅采用相当低的数学概念。众所周知，他们自行发展深厚的概念，并且在将不同的数学领域的概念联系起来时遇到困难。所有这些使我们提出了一个哲学问题，该问题现在正开始受到应有的关注：什么是数学理解？

数学联邦政治世界观提示您：看后求收藏（笔尖小说网http://www.bjxsw.cc），接着再看更方便。