数学哲学译文丨形式主义的两个教条（二） (7-4)

14. 从根本上说, 数学之所以进行演绎, 并不是因为演绎能保证保真, 而是因为通过演绎得到的结果才能确定为真. 因此, 本来应该独立于是否保真来定义是否为演绎. 这也是「演绎是否由保真这一事实得到辩护」的问题. 达米特在 [68] 中讨论了这个问题, 并在 p.276 中这样谈到归纳和演绎:「对于归纳, 原则上不可能存在辩护. 我们拥有的论证方法看起来完全没有说服力. 而且我们一个辩护的候选都没有. 对于演绎, 我们有很好的候选来为特定逻辑系统辩护, 即可靠性证明和完备性证明. 尽管存在这样的看似有说服力的论证, 但这种辩护不可能存在.」并且在 p.300 中说:「可靠性证明和完备性证明与其说是对该证明所适用的逻辑学理论的测试, 不如说是对隐藏在语义学背后的意义理论的测试.」这与标准观点完全相反, 但如果我们回顾一下为什么接受 Modus Ponens, 达米特的话似乎很有说服力.

15. 在本章中, 我将把形式化的证明写作「证明」, 把作为逻辑式 (该逻辑式附带谓词逻辑中定义的证明) 的定理写作「定理」, 以区别于朴素意义上的证明和定理.

16. 遗憾的是, 他说「忘记了是谁说的」.

17. 回顾这一点, 布劳维尔的学生海廷提出, 并由达米特展开哲学讨论的「命题的意义就是其证明」这一源自直觉主义的主张, 如果故意忽略其哲学语境, 而作为简单朴素的口号来读, 似乎具有格外强大的说服力. 关于这一点, 请参阅 Shapiro [45] pp.246-248, 金子洋之 [24] pp.201-209等. 此外, 形式主义和直觉主义的区别或许也可以这样理解: 形式主义认为命题先于证明而存在, 证明是通过罗列命题构建的; 而直觉主义认为证明先于命题而存在, 命题简洁地表达了证明所表示的意义内容.

18. 关于定义理论的坐标轴, 物理学家佐藤文隆在 [42] pp.74-75 中这样说:「理论就是人为设定简化到夸张的程度的对立轴, 并以与这个『坐标轴』的关系来描述现实. 坐标轴并不真实存在于现实中, 参照它所描述的现实始终是『坐标系依赖』的, 而不是现实本身.」即使对于自然科学来说这已经几乎是常识, 但人们很少关注谓词逻辑是否也有类似的「坐标系依赖」. 形式证明和现实证明经常被简单地等同起来.

19. 前面介绍的海廷的主张「命题的意义就是其证明」可以看作是认为这两个坐标轴相同.

20. 这只是说标准的命题逻辑和谓词逻辑框架中没有「证明」的语义学, 而不是说世界上不存在「证明」的语义学. 例如参见 Schroeder-Heister [207].

21. 当然, 如果将逻辑式的有限序列统称为「证明」, 就可以定义「错误的证明」. 但在这种情况下, 无意义的逻辑式序列和「错误的证明」无法区分. 这与能够区分假逻辑式和无意义符号串的命题语义学有很大不同. 相反, 例如奥雅博在 [18] pp.175-176 中关于维特根斯坦认为「非定理逻辑式」这一概念是无意义的观点的讨论, 构建一个不存在假逻辑式的框架也并非不可能. 实际上, 考虑根岑的 LK, 将 LK 的推理规则视为 相继式 (sequent) 的递归定义而非推理规则, 并将 → φ 形式的特殊相继式定义为定理, 就可以在不定义包含假逻辑式的一般逻辑式的情况下定义定理. 当然, 这个定义过于人为, 例如饭田隆在 [11] p.140 注4 中认为这个立场得出的结论「看起来难以忍受」, 确实不自然且反常识. 但是, 如果接受这样的定理定义, 定理和证明的关系就成为被定义物和定义的关系, 在这个定理定义下, 「命题的意义就是其证明」这个主张或许反而会变得自然且显然.

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