数学哲学译文丨形式主义的两个教条（一） (11-9)

在整个20世纪, 谓词逻辑是精确和形式化分析不限于数学领域且包括自然语言句子和概念的最标准框架. 当然, 丰富的自然语言表达能力和人类认知能力并不能完全囊括在谓词逻辑的框架中. 基于各种视角和问题意识, 人们尝试修改和扩展谓词逻辑. 但是, 这些尝试并没有取得足够的成果. 一个原因是, 这些尝试天真地假定谓词逻辑的「证明」和「理论」定义是「阐明」, 另一个原因是, 谓词逻辑本来就不是为了「阐明」人类思维和认知的全貌而构建的.

谓词逻辑原型的创造者弗雷格将自然语言和他构建的形式系统的关系比喻为肉眼和显微镜的关系, 但显微镜有优于肉眼的地方, 也有不如肉眼的地方[31]. 而谓词逻辑是为了在模型化数学公理化方法这一特殊目的中发挥最大性能, 而故意限制功能, 重新制作弗雷格设计的显微镜而成的东西. 尝试构建自然语言形式语义学的一种——情境语义学的 Barwise 这样说:「基于一阶谓词逻辑的自然语言语义学和认知分析之所以不成功, 是因为这就像缘木求鱼. 一阶谓词逻辑是为了模型化公理化方法而设计的, 并为此发挥了很好的作用[32].」

但是, 谓词逻辑在这个特殊目的上运作良好这一事实, 也不一定是简单的. 例如, 集合论家 Martin 说, 用谓词逻辑给出数学证明的严格定义是令人惊讶的[33]. 不管 Martin 的意图如何, 这个主张有两种解释. 一种是, 人类能够找到谓词逻辑这个定义数学证明的唯一正确方法是令人惊讶的, 这对应于将「证明」的定义视为「阐明」; 另一种是, 尽管谓词逻辑难以说捕捉到命题和证明的本质, 但却能用这个不完善的谓词逻辑给出证明的严格定义是令人惊讶的, 这对应于将「证明」的定义只是「命名」.

也有观点认为, 谓词逻辑采用的将句子分解为主语和谓语的框架源于欧美语言, 与日语不太合拍[34]. 因此, 谓词逻辑的句子分析方法不一定是普遍和自然的. 而且, 即使数学事实的普遍性确凿无疑, 什么是数学方法也会随时代变化, 例如公理化方法直到20世纪才在数学中普及. 如果是这样, 就很难认为存在分析证明的唯一正确的绝对方法, 也不能轻易断言「证明」的定义就是「阐明」, 或者作为「阐明」是成功的.

形式化的「证明」定义可能意在「阐明」朴素的证明概念, 这种尝试可能成功, 也可能失败而只剩下「命名」的作用. 即使成功, 通过这种「阐明」, 证明的概念也可能发生很大变化. 无论如何, 要理解「证明」这个概念, 重要的不是解决「阐明还是命名」的问题, 而是阐明「证明」定义背后有什么样的思路, 给出这个定义后, 我们对证明概念的理解发生了怎样的变化. 思考「阐明还是命名」这个问题是探讨「证明」与朴素证明概念关系的线索, 阐明这种关系应该是理解不完备定理的重要组成部分.

但是, 至少目前在数学基础论中, 「证明」与朴素证明概念的关系很少被讨论. 这首先是因为天真地相信「证明」的定义就是对朴素证明概念的「阐明」[35]; 其次是因为对这个老掉牙的话题提不起兴趣, 周围也没有讨论的人; 最重要的是, 不考虑「证明」和证明的关系也能写论文, 考虑了也写不了论文, 也就是说这是与当前数学基础论无关的问题[36].

9.7 关系代数学

数学联邦政治世界观提示您：看后求收藏（同人小说网http://tongren.me），接着再看更方便。