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

在现实的数学中, 证明有时从假设出发, 有时从结论出发, 有时还会更换假设或结论, 是反复试错写成的. 数学中不存在仅由「正向推理」或仅由「逆向推理」组成的推理. 对于写形式化证明也是如此, 无论是朴素证明还是形式化证明, 在讨论证明时, 「正向推理」和「逆向推理」的区别都没有太大意义.

创作证明、理解证明和确认证明的正确性是不同的. 如果演绎和发现这两个概念与证明概念有关系, 那么创作证明可能对应发现, 确认证明的正确性可能对应演绎. 即使理解证明概念需要演绎和发现这两个概念, 演绎和证明的关系也不能用「将演绎写下来就是证明」这种简单的图式来解释.

9.4 隐藏的维度

形式定义的「证明」, 即形式证明, 是从逻辑公理和非逻辑公理出发, 通过反复应用推理规则形成的有限逻辑式序列, 而「定理」是证明的最后出现的逻辑式[15]. 「定理」和「证明」虽然都是有限的符号序列, 但本质上是完全不同种类的存在物. 实际上, 定理和证明有区别也是数学家的切身体会. 在命题逻辑和谓词逻辑中, → 和 ⊢ 都根据「定理」和「证明」的区别被明确区分, 准确把握这一区分是理解命题逻辑和谓词逻辑的第一步.

但同时, 大多数数学家并不区分「φ → ψ 可证」和「在假设 φ 的情况下 ψ 可证」, 即不区分 → 和 ⊢ . 当然, 根据演绎定理, → 和 ⊢ 的等价性已经得到证明, 所以实际上我们不需要区分 → 和 ⊢ . 但数学家并不是从演绎定理学到不需要区分→ 和 ⊢ , 而是一开始就不区分 → 和 ⊢ . 那么, 「定理和证明是不同的」这一切身体会与不区分 → 和 ⊢ 的习惯, 哪一个更合理呢?

在自然演绎的命题逻辑和谓词逻辑系统中, 当能够从假设φ 推导出 ψ 时, φ → ψ 就被定义为已证明, 因此演绎定理是不需要证明的显而易见的事实. 因此, 演绎定理不是关于 → 和 ⊢ 的基本性质的定理, 而应该被视为关于希尔伯特风格的定理和证明的形式化的定理. 如果是这样, 哪些是 → 和 ⊢ 固有的性质, 哪些是与形式化有关的性质, 可能并不总是很清楚. 而且, → 和 ⊢ 的区别本来就是模糊的, 但由于强行形式化定理和证明的概念, → 和 ⊢ 这两个概念可能被硬生生地割裂了. 如果是这样, → 和 ⊢ 的区别只是形式化定理和证明时的副产物, 数学家不区分 → 和 ⊢ 的习惯就是合理的.

但是, 如果→ 和 ⊢ 无法区分, 而且 → 对应定理, ⊢ 对应证明, 那就意味着「定理和证明没有区别」. 通常来说, 「定理和证明是不同的」这一主张似乎是无可辩驳的显而易见的事实, 但认为定理和证明是同类存在物的立场并非完全不可能. 许多年前, 一位研究证明论的朋友告诉我一位伟大的数学基础论学者曾说过[16]: 「定理是证明的省略. 也就是说, 定理和证明的关系就像标题和正文的关系, 定理和证明的区别只是表述详略程度的区别. 确实, 「读了证明才理解定理的含义」这种经历并不罕见[17]. 如果是这样的话, 定理和证明之间可能没有超出说明长短和详略程度以上的区别, 区分定理和证明的常识可能只是毫无根据的想当然.

然而, 数学家通常明确区分定理和证明. 为了尊重数学家不区分→ 和 ⊢ 但区分定理和证明的实际感受, 既不能认为「→ 和 ⊢ 是不同的」, 也不能认为「定理和证明没有区别」, 而需要第三种选择: 「 → 对应定理, ⊢ 对应证明这种说法并不成立」.

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