2024 王浩 - 从数学到哲学

9 数学与计算机

总的来说，形式化或使模糊程序变精确，对于拓广计算机的应用范围具有实际价值。这也许是逻辑与计算机之间的最基本的联系。正是在这个方向上，长远看有可能实现大规模的数学革命。随着越来越多的数学证明被机械化，人对数学活动的贡献将不得不少一些程式化的方面，而多一些富有想象力和创造性的内容。

自动化证明的最初尝试和有限成功源自如下认识：数理逻辑在形式化方面已经达到了相当先进的水平。进一步的努力揭示了，逻辑作为对数学的一种形式的和系统化的处理，其成就有它的局限性。十分粗略地说，我们需要的不是数学教材原则上的形式化，而是数学活动实践上的形式化。目标是要丰富逻辑(或数学)，使计算机可以辅助纯数学家，至少与它们现在辅助应用科学家一样多。这需要彼此相关的两个方面的机械化:形式化已发现的证明;抽象出一般的方法，为寻找新定理的证明提供指导。似乎有必要发展一种“逻辑数学”，此想法必定会引起纯数学家的反感，他们会觉得这是数学家与图书馆员的混合。事实很可能是，较之于“数学语言学”与机器翻译之间的关系，这样一门学科与自动化证明之间的关系要紧密得多。不仅如此，它甚至可能是一条最有前景的途径，将带动“人工智能”之潜力和局限性研究的全面进步。

形式化显然对计算机的所有应用都很重要。计算机的存在依赖于一个基本的事实，即我们有进行数值计算的精确规则。借助类比论证，我们或许可以认为，计算机在心智活动方面的深刻应用将首先在数学证明机械化领域实现。与博活动相比，这个领域更丰富，对所有智力工作也更重要。

数学推理是机械的这个论题有多重蕴意。它不只意味着数学证明可以形式化;它要求证明方法的机械化，而不只是将给定的非形式证明形式化为一种可机械地检查的形式。这个论题的一个歧义之处，在于如下两种解释间的差别:一是仅仅要求能以某种方式机械地做数学，二是要求机械化我们做数学的实际过程，后者更强一些。例如，根据第二种解释，这个论题会要求我们将以下这些过程机械化:个体数学家如何寻找证明，数学是怎样被教授的，数学共同体如何就是否接受某些结果(为真)这个问题达成共识。如果人们的兴趣是确定这个论题是否能以一种可想象的方式为真，采取第二种解释是有优势的。但如果人们只是想用计算机做尽可能多的数学，那么合理的做法就是不要为忠实于人类实际如何做数学而操心。这里我们得到了人工智能与仿真做对比的一个例子。

在形式化方面，现代逻辑有两个主要的成就。第一是彻底确立了如下结论:全部数学都可以还原为公理集合论;并且只要不嫌麻烦，可以在该系统中完全形式化地--在机械可检验的意义上--再现数284学证明。第二是司寇伦和艾尔布朗的结果，根据这些结果，通过把数学定理理解为谓词演算中的假言定理(相关公理蕴涵该定理)，我们能够以(原则上)机械的方式搜索每一个数学证明，以确定一个相关的艾尔布朗展开是否包含矛盾。尽管这些结果令人赞叹，而且对于数学证明机械化工程大有鼓舞作用，它们仍然只是一些理论结果，而无法确立数学推理(甚或其主要部分)在本质上是机械的这个更强的论题。

这个尚未被确立的强论题令人兴奋之处在于，我们所面对的是个全新类型的问题，它呼唤一门全新的学科，这门学科对心灵与机器这个历久弥新的问题会产生广泛影响。它要求我们以系统的方式处理数学活动。虽然这并不是要我们实现机械仿真，但它确实要求对我们做数学的过程进行一番仔细的研究，以便确定非形式方法如何可由机械化程序替代，以及计算机的速度优势如何能用来弥补其不灵活性。这是一个结局仍很不确定的领域，而好事多，于它也不例外。但我们的确对它所要求的这种心理学、逻辑学、数学和技术的新奇结合充满期待，渴望从中得到惊喜。

一般来说，还原论者会被某些模式的力量或美打动，并希望在它们的基础上构建一切。上述两个对立的极端，似乎在实践上--如若不是在理论上--共享了这种还原论的执迷。依我看，应该对与料，亦即已有的数学证明和证明方法，进行更多的反思性考察。的确，对人来说自然的东西，对机器来说不一定是自然或方便的。因此，盲目模仿人类不会太有成效。但尽管如此，已有数学却包含了丰富的材料，构成了我们对数学推理之理解的主要源泉。合理的做法是从这一宝库中提炼一切可机械化的东西。换言之，我们应当力求还原与反思间的互动，由于缺少更合适的名字，姑且可称之为辩证法。

反思主义者更严肃地对待已有人类知识所提供的材料，并且常常不能给出一概而论的答案。在其极端形式中，我们会到达现象学，它是严肃的哲学，但与技术进步几乎没有直接关系。例如，一些非结论性的论证被提出来以支持这样一种观点:某些心智任务，如清晰地分类，容许模糊性，区分本质和偶性，以及那些对初级意识有依赖的活动，本质上都不可能由计算机来执行。尽管这些讨论有助于使人们聚焦一些长期问题，我们目前还没有足够严格的、关于可实现计算机和可行算法的概念，以证明甚或推测这类不可能性结果。

尽管这些极端立场前途未卜，在自动化证明领域将还原(综合)和反思(分析)方法协同起来却是十分可取的。特别地，在目前阶段，人们对艾尔布朗定理的沉溺，在我看来反映出了一种还原主义倾向，应该用对与料(已有数学)的更多反思加以调和。例如，在数论中，我们显然应该使用最小的反例，而不仅仅是反例。在数学的每个分支中，除了所有分支共有的普遍特征，我们还应该引入该特定分支独有的那些特征。此外，我们对节省公理不再感兴趣，而是更倚重导出规则(元定理)。随着我们逐渐进步，每个阶段的已有知识需要被更仔细地消化和组织，以便使机械复现变得可行。更具体地说，我认为对大量的已有证明进行广泛而系统的考察在目前阶段是有价值的。

与单纯的游戏相比，数学的一个显著特征是其应用。人们并不只用或主要用可应用性来为纯数学的研究做辩护。数学在其高等阶段有它自己的生命和追求。例如，美和优雅以及深刻性，都是数学工作评价的常用标准。

只有当相关数学共同体接受了一个定理，并且有人理解了它的证明，这个定理才能说是得到了确立。实际执行对数学来说很重要，不过不是在展示"的第十亿位数字这种狭隘的意义上，而是在一种更广泛的意义上，即被某个人类心灵实际地理解(一种心智活动)。关注数学的这个方面甚至可以帮助我们解决一个根深蒂固的争论，即应用对数学而言究竟有多么重要。追求优雅是数学的一个核心，其原因可能是，作为一项心智活动，数学必须是清晰的、一目了然的。而优雅一般能拓宽我们所能控制的复杂性范围。

工程学主要研究如何制造东西，而数学更关心证明某些事情在某些一般条件下能不能完成。证明某些事情不可完成，有特别的吸引力，因为这样的结果以否定的方式涉及一个给定的方法的所有可用资源。例如，在平分一个角时，我们只用到尺规作图方法的一小部分资源;而在证明三等分任意的角不可能时，我们需要对能以尺规做出的所有可能的构造有一个清晰的概念。正是在这一证明不可解性的领域，对理想化机器的抽象研究产生了最具数学趣味的结果。特别地逻辑和计算机理论之间的互动尤为引人注目。

对机械化的兴趣意味着形式逻辑的重新定位，它要更追求效率，特别地，这意味着，对公理和初始概念节俭性的要求需补充以对大量概念和规则的准确阐述，这些概念和规则构成普通数学家的工具库。

10 心灵与机器

今天，生物学家们普遍接受的一个信念是，所有生命形式最终都可以由支配无生命物质的自然法则来解释。这一信念经常被称为机械论或唯物主义。根据这种观点，生命科学的终极目的是通过物理学的原理来说明生命(和心灵)的起源和性质。心理学可还原为生理学(大脑的机制)，生理学(和生物学)可还原为化学和物理学(生命的机制)，化学可还原为物理学。生命(和心灵)现象的复杂性来源于其所涉大量对象的复杂组织，而非支配基本对象的基本法则本身的复杂性。