Formalized Mathematics
Formalized Mathematics
复制标题
DOI：
--
复制
发表时间：
1996
期刊：
影响因子：
--
通讯作者：
J. Harrison
中科院分区：
文献类型：
--
作者：
J. Harrison
人们普遍认为，原则上，几乎所有的现代数学都可以完全形式化。实际上这样做的可行性受到广泛怀疑，结果的价值也是如此。但在计算机时代，我们相信这种形式化是可能的，也是可取的。然而，与QED宣言相反，我们不提供支持这样一个项目的论战。我们只是试图把数学的形式化放在历史的角度，以及审视现有的实践，并确定我们认为最有趣的问题，理论和实践。1历史和哲学数学通常被认为是最优秀的精确学科。但是，数学家（在论文、专著甚至教科书中）常用的语言可能非常模糊;也许与日常用语相比不是这样，但与自然科学或哲学等其他知识学科的从业者使用的语言相比肯定是这样。Trybulec和J.W. Czkowska（1992）指出，在某种程度上，这是自然的：因为数学的基本语义通常比其他学科的语义更清晰，头脑自然地被束缚在一种精确的思维模式中，术语的精确性并不那么重要。但有时需要一个知识渊博的读者来区分修辞华丽与真实的内容，并欣赏结果被断言的背景。一些日常用语充满了特殊的意义;例如，观察“映射到X”和“映射到X”之间的关键区别，或者像“几乎所有x”这样听起来模糊的表达的精确（尽管依赖于上下文）含义。另一方面，许多作者认为显而易见或不重要的问题可能会被掩盖。布尔巴基（Bourbaki，1968）强调了“滥用语言的重要性，没有它，任何数学文本都有迂腐的风险，更不用说不可读了”，但许多惯例不仅仅是滥用语言。考虑以下例子取自早期页松村（1986年）：如果f A B是一个环同态和J是一个理想的B，那么f J是一个理想的A，我们表示这一点的A J ;如果A是一个子环的B和f是包含映射，那么这是相同的通常集理论概念的交集。一般来说，这是不正确的，但混乱不会出现。当我们说R有特征p，或者写char R p时，我们总是指p是一个素数。在关于环的定义和定理中，有时可能会发生条件A被省略的情况，即使它实际上是必要的。Trybulec和Zerwietzkowska（1992）评论说，数学文本的语言并非毫无疑问是一种自然语言;但它总是包含大量自然语言的混合物，并且具有所有通常的模糊性和不精确性。如果数学是一个小的、统一的学科，一个从业者就能轻松掌握，这可能不是问题。但恰恰相反，数学正日益朝着专业化的方向发展，指望数学物理学家，比如说，深刻理解拓扑学、微分几何、数值分析等领域的所有理论成果是不现实的。还有一个数学推理的正确性问题。数学证明在发表之前要经过同行评审，但有很多证据确凿的案例表明，发表的结果是错误的。一个值得注意的例子是Kempe（1879）对四色定理的证明;这个证明中的错误最终被Heawood（1890）在印刷品中指出，只有在阿佩尔和Haken（1976）的工作下，这个定理才最终被承认。
It is generally accepted that in principle it’s possible to formalize completely almost all of present-day mathematics. The practicability of actually doing so is widely doubted, as is the value of the result. But in the computer age we believe that such formalization is possible and desirable. In contrast to the QED Manifesto however, we do not offer polemics in support of such a project. We merely try to place the formalization of mathematics in its historical perspective, as well as looking at existing praxis and identifying what we regard as the most interesting issues, theoretical and practical. 1 History and Philosophy Mathematics is generally regarded as the exact subject par excellence. But the language commonly used by mathematicians (in papers, monographs, and even textbooks) can be remarkably vague; perhaps not when compared with everyday speech but certainly when compared with the language used by practitioners of other intellectual disciplines such as the natural sciences or philosophy. Trybulec andŚwiȩczkowska (1992) point out that in a way this is natural: since the underlying semantics of mathematics is generally clearer than that of other disciplines, the mind is naturally trammelled into a precise mode of thinking, and terminological exactness is less important. But a knowledgeable reader is sometimes needed to separate rhetorical flourish from real content, and to appreciate the context in which results are asserted. Some everyday phrases are imbued with a particular significance; observe for example the crucial distinction between a ‘mapping into X’ and a ‘mapping onto X’, or the precise (albeit context-dependent) meaning of woolly-sounding expressions like ‘for almost all x’. And on the other hand many issues that the author feels are obvious or unimportant may be glossed over. Bourbaki (1968) stresses the importance of ‘abuses of language, without which any mathematical text runs the risk of pedantry, not to say unreadability’, but many of the conventions go beyond mere abuse of language. Consider the following examples taken from the early pages of Matsumura (1986): If f A B is a ring homomorphism and J is an ideal of B, then f J is an ideal of A and we denote this by A J ; if A is a subring of B and f is the inclusion map then this is the same as the usual set-theoretic notion of intersection. In general this is not true, but confusion does not arise. When we say that R has characteristic p, or write char R p, we always mean that p is a prime number. In definitions and theorems about rings, it may sometimes happen that the condition A is omitted even when it is actually necessary. Trybulec and Świȩczkowska (1992) remark that the language of mathematical texts isn’t incontrovertibly a natural language at all; but it invariably contains a substantial admixture of natural language, and that has all the usual potential for ambiguity and imprecision. This might not be a problem if mathematics were a small, unified subject easily graspable by a single practitioner. But on the contrary mathematics is heading increasingly in the direction of specialization, and it’s not realistic to expect mathematical physicists, say, to appreciate deeply all the theoretical results in topology, differential geometry, numerical analysis and what not that they use. There is also the question of the correctness of mathematical reasoning. Mathematical proofs are subjected to peer review before publication, but there are plenty of well-documented cases where published results turned out to be faulty. A notable example is the purported proof of the 4-colour theorem by Kempe (1879); the error in this proof was eventually pointed out in print by Heawood (1890), and it is only with the work of Appel and Haken (1976) that the theorem has finally come to be ac-