【数学与哲学翻译】Peter Smith论数学 (7-2)

我稍后会回顾最后这个问题。但让我们先从Imre说“数学家在展示他们的证明时会转向形式主义”这个说法开始。注意到，Imre在这里将形式主义描述为一种关于数学本质的说法，大约类似于是“数学只是在无意义符号间的一种游戏，看看你能从给定规则下从哪些符号串推出哪些符号串”。首先值得一提的是，至少对于那些对数学做出过严肃思考的哲学立场来说，这是一个稻草人立场：例如，伟大的希尔伯特通常被认为是典型的形式主义者；但他的立场要复杂得多。好吧，我也不是没听说过听过其他数学家描述同样的朴素的“这只是符号游戏”的说法。我此处想要指出的是，这里我们将两个事情混为一谈了，一方面是对形式主义的认可（无论是Imre的朴素形式主义还是更复杂的形式主义），另一方面是尝试追求形式化的做法。将这两者混为一谈是错误的。因为我听过其他人也犯过同样的错误，所以我认为此处值得停下来分析一下。

我们先从如下观察开始：在展示复杂的数学论证时，将我们的命题以数学+英语+符号的方式来展示是有帮助的，这种方式就是明确设计来帮助表达精确、去掉模糊性、使得逻辑结构清晰。例如，想想我们使用的量词/变量符号——比如∀ε∃δ——是如何使得一般性命题的结构变得清晰。然后我们试图将我们的命题拼凑成近似于一系列形式推导的东西。这么做有什么原因吗？因为它迫使我们诚实：我们必须记下我们引用的前提，以及我们使用的确切推理步骤。毕竟诚实是最佳策略。假设我们通过每一步推理都是显然有效的（没有隐藏的前提被偷偷引入，也没有可疑的推理步骤）从给定的前提到一些目标结论。那么通过我们的诚实劳动，我们就争取来了一种信任的权利，信任前提确实蕴含了所需结论。耶！

是的，即使是最硬核的数学文本也是用普通语言和数学符号的非正式混合写成的。证明几乎从来都不会被完完全全地被形式化地剖析，因此它们的呈现仍然不符合逻辑学家对完全形式化的理想。我们希望这种非正式地呈现的数学证明，原则上能被锐化成更接近完全形式化证明的近似。的确，我们甚至会祈祷，这些非形式证明最好能够以逻辑学家描述的严格规范的形式呈现（甚至能在计算机上实现），使得最终从我们陈述的公理开始，每一个微小的推理步骤都被完全明确地表达出来，以便一切都可以被机械地检查它们是否符合某些公认的推理规则。

但也的确，这种细枝末节的形式化努力，几乎根本不值得花费时间和墨水。在数学实践中，我们使用足够的形式化来说服自己，我们的结果不依赖于非法引入的前提或可疑的推理步骤，然后就此打住——我们的座右铭是“一天的严谨一天当就够了”（译者注：这句话是马太福音6:34后半句的改写：“所以， 不要为明天忧虑， 因为明天自有明天的忧虑； 一天的难处一天当就够了”）。看看咱们剑桥的骄傲，怀特海和罗素是如何在《数学原理》中阐述这一观点的：

大多数数学研究并不关心对完整推理过程的分析，而是关心对证明的摘要的呈现，只要这个摘要足以说服一个受过适当训练的头脑。

（“受过适当训练的头脑”大概指的就是三一学院数学牲）（译者注：原文是Trinity mathmo，第二个词就是mathematician的昵称，我这里也选择类似的昵称翻译）

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