形式主义的两个教条
现代形式主义受到两个教条的严重制约. 一个教条是, 存在着句法学 (即独立于模型概念的、基于形式证明的数学真理) 和语义学 (即基于模型的数学真理) 之间的根本分裂. 另一个教条是还原主义, 即任何数学证明都等同于基于公理和推理规则的、由指称有限对象的名词构成的逻辑构造物. 我认为这两个教条都缺乏根据. 放弃这些教条会导致的一个结果是, 正如我们稍后将看到的, 数学哲学和作为数学的数学基础论之间被认为存在的界限会变得模糊. 另一个结果是转向实用主义[1].
一般认为, 谓词逻辑为数学中证明的概念提供了形式化的定义, 阐明了数学中真假的概念与可证明的概念之间的区别. 不完备定理是关于在谓词逻辑基础上发展的算术和集合论的定理, 不完备定理的意义和重要性也是在谓词逻辑的标准理解下讨论的. 然而, 谓词逻辑的标准理解并非完全不容置疑. 如果谓词逻辑的标准理解不适用, 那么对不完备定理揭示了什么的解释也将发生重大变化.
在本章中, 我们首先在9.1节和9.2节讨论谓词逻辑的语义学和句法学之间的区别. 9.1节指出, 在语义学和句法学差异的通俗理解下, 讨论谓词逻辑的语义学和句法学之间的区别是困难的, 语义学和句法学之间的区别并非像想象的那样显而易见. 9.2节讨论了许多与数学相关的讨论可能在不知不觉中受到逻辑实证主义数学观的影响, 谓词逻辑的语义学可能也是在这种影响下发展起来的.
接下来, 从9.3节到9.6节, 我们考虑谓词逻辑中形式证明的概念与数学中朴素证明的概念之间的关系. 证明的概念与演绎的概念密切相关, 一般认为谓词逻辑中形式证明的概念是对演绎的形式化. 9.3节讨论了形式证明的概念具有被认为是发现特征的性质, 形式证明的概念不一定与演绎相对应. 此外, 9.4节通过讨论可证明性概念与命题联结词「蕴含」之间的关系, 考虑了朴素证明概念可能与形式证明概念不对应的可能性, 并指出, 在谓词逻辑中, 语义学的存在与将证明形式化的思维方式是成对出现的.
9.5节介绍了源自卡尔纳普和蒯因的同义性报告、阐明、命名这三种定义的区分, 以及这种定义区分与形式主义数学观之间的关系. 特别是, 我们讨论了构造证明、理解证明以及检验证明正确性之间的区别, 并论证了作为阐明的定义在构造证明时很重要, 而作为命名的定义在检验证明正确性时很重要. 在这个讨论的基础上, 9.6节讨论了形式证明的概念不能简单地说是对朴素证明概念的阐明.
不管最初构建谓词逻辑的目的是什么, 对于当前的数学基础论来说, 形式证明的概念是否阐明了朴素证明的概念并没有太大意义. 9.7节提出, 对于当前的数学基础论来说, 谓词逻辑与其说是一个分析数学基础相关哲学概念的框架, 不如说是一种「关系代数学」. 最后, 在9.8节中, 我们介绍了这种「关系代数学」观点在数学基础论中带来的两种实用主义, 并讨论了在认为形式证明的概念不是对朴素证明概念的阐明时, 对形式主义和不完备定理的理解的可能性.
9.1 神圣的逻辑与世俗的逻辑
与语言相关的讨论有语义学和句法学, 命题逻辑和谓词逻辑也有语义学和句法学[2]. 广义上讲, 语义学是关于语言所表达内容的讨论. 狭义上讲, 语义学是关于真假概念的讨论, 在命题逻辑中是关于真值赋值的讨论, 在谓词逻辑中是关于结构和模型的讨论. 另一方面, 句法学是关于符号串操作的讨论, 无论在命题逻辑还是谓词逻辑中, 都是关于证明和定理的讨论. 在命题逻辑和谓词逻辑中, 语义学被认为是使用集合概念的包含无限性的超越性讨论, 而句法学的特点在于是关于符号这一具体对象的有限操作的讨论.
从朴素或通俗的角度来说, 语义学是关于语言所表达内容的理论, 而句法学是关于语言的符号串表示的理论. 然而, 命题逻辑中语义学和句法学的特点并不一定与这种通俗的语义学和句法学的理解相对应. 命题逻辑中的真值计算仅仅是按照一定规则对表示真假的两种符号进行有限的符号操作, 之所以可以说这种操作与真假的概念有关, 仅仅是因为阅读真值计算的人将表示真的符号与真的概念联系起来. 另一方面, 关于命题逻辑定理和证明的讨论确实是关于有限符号操作的讨论, 但如果逻辑公理和推理规则的选择的合理性是由完备性定理给出的, 那么就很难说关于命题逻辑定理和证明的讨论与真的概念无关. 而且, 如果不参考完备性定理, 很难解释为什么所选择的逻辑公理和推理规则是必要且充分的[3].
就命题逻辑而言, 真值计算和证明构造之间最大的区别不在于它们是否涉及真的概念或是否为符号串操作, 而在于真值计算是「可判定但低效的」, 而证明构造是「高效但不可判定的」. 当然, 也可能有这样一种观点, 即这种区别正是语义学和句法学之间的区别. 但如果选择这种观点, 就必须放弃对语义学和句法学的通俗理解, 关于这种观点的合理性需要进行相当多的讨论.
与命题逻辑相比, 谓词逻辑的语义学和句法学之间的区别看起来更加明显. 谓词逻辑的模型是使用集合概念定义的, 为了表明某个逻辑式可以从谓词逻辑理论中导出, 需要参考所有这样的模型. 另一方面, 与命题逻辑的情况类似, 在谓词逻辑中, 证明也仅仅是有限的符号串. 谓词逻辑的语义学必须使用基于集合概念的超越性方法, 而谓词逻辑的句法学始终是关于符号这一具体对象的有限讨论.
然而, 这种对谓词逻辑语义学和句法学差异的理解也与语义学和句法学的通俗理解不相符. 这一点在谓词逻辑的完备性定理的证明中表现得尤为明显. 在证明无矛盾理论具有模型的过程中, 关键是构造与结构的初等图式相对应的理论. 由于可以直接从这个理论得到模型, 所以这个理论几乎等同于模型. 因此, 这个理论是与语义学相关的对象. 但是, 由于这个理论是句子的集合, 根据句法学的通俗理解, 它也可以被视为句法学对象.
无论是在命题逻辑还是谓词逻辑中, 语义学和句法学的通俗理解都不适用. 这里有三种可能性. 第一种是世界上存在两种语义学和句法学. 这种观点很明确, 但本质上只是一种逃避. 第二种可能性是, 命题逻辑和谓词逻辑的语义学和句法学本来就不应该被称为语义学和句法学. 最后一种可能性是, 我们还没有充分理解语义学和句法学之间的区别.
9.2 经验主义者的亡灵
谓词逻辑语义学和句法学之间微妙而奇特的关系典型地体现在谓词逻辑语言Ը 的结构 𝕸 上 Ը的句子 φ 为真, 即 𝕸╞ φ这一概念的数学定义中.
𝕸 是 Ը 的结构, 因此 Ը 的非逻辑符号在 𝕸 上已经被解释. 在这种解释下, φ 的意思是明确的. 如果可以使用这个明确的意思, 那么 𝕸╞ φ 是否成立就是一个无需数学定义的自明概念. 然而, 将这个概念视为自明的做法并不被视为数学上严格的论证. 在数学上严谨编写的谓词逻辑教科书中, 大多数情况下, 是先给出 𝕸 的初等图式 Th(𝕸|𝕸|) 的递归定义, 并规定当 φ ∈ Th(𝕸|𝕸|) 时, 𝕸╞ φ 成立.
初等图式Th(𝕸|𝕸|) 是作为句子集合的理论, 根据句法学的通俗理解, 它属于句法学的领域. 因此, 结构上的真这一语义概念被认为是通过初等图式这一句法概念在数学上被严格定义的.
然而, 数学的严谨性应该根据是否援引了我们的朴素常识来判断, 而与表述是否形式化基本无关. 在Th(𝕸|𝕸|) 的递归定义中, 对于原子逻辑式, 我们朴素地由援引了其在 𝕸 上的真假. 而对于例如量词 ∀ , 使用了诸如「对任意 α ∈ |𝕸| 有 φ(cα) ∈ Th(𝕸|𝕸|) 成立时, ∀xφ(x) ∈ Th(𝕸|𝕸|) 成立」这样朴素而常识性的逻辑符号解释. 因此, 引入初等图式并不意味着排除了我们朴素的常识, 没有理由认为使用初等图式会在数学上更加严谨.
源自康德的真理或判断的区分包括分析真理和综合真理. 分析真理是指「主语所指概念包含谓语所指概念」所导致的真理, 而综合真理是非分析的真理. 康德还给出了先验和后验的区分, 先验真理和后验真理分别是可以独立于经验而知道的真理和不能独立于经验而知道的真理. 粗略地说, 分析性对应先验性, 综合性对应后验性. 但康德认为这两种区分是不同的, 并论证数学是「先验且综合的」[4].
后来, 弗雷格将分析真理定义为「通过定义变形可以还原为逻辑真理的东西」, 并认为几何学是「先验且综合的」, 而算术是「先验且分析的」[5]. 如果粗暴地简化, 认为整个数学都是「先验且分析的」, 这就是继承了逻辑主义思路的逻辑实证主义[6]. 简而言之, 康德、弗雷格和简化的逻辑实证主义数学观之间的差异在于对「分析真理和综合真理」与数学关系的理解不同.
分析真理和综合真理的区分与「数学是什么」这个问题密切相关. 我们习惯于当前数学论文和教科书的风格, 即从定义出发, 然后进入定理和证明. 我们可能过于简单化了这种关系, 将分析性视为数学的定义. 然而, 蒯因断言, 分析真理和综合真理的区分是经验主义者怀有的一个毫无根据的教条[7]. 如果蒯因是正确的, 并且如果坚持使用递归定义的初等图式来定义 𝕸╞ φ 是基于对分析性的倾向, 那么这种坚持不过是一种由毫无根据的教条所带来的习惯.
与分析真理和综合真理、先验和后验类似的区分还有必然和偶然、确定和不确定等. 我们不知不觉地把数学和非数学的区分也纳入了这一系列区分之中. 进一步地, 我们可能模糊地将句法学与计算、将语义学与感觉联系起来, 从而将句法学和语义学的区分也对应到了类似的区分上.
认为使用初等图式定义结构上的真的概念在数学上是严格的, 这可能也是基于一种素朴的观念, 即初等图式是一个句法概念, 句法概念是分析的, 而分析概念是数学的. 如果我们确实在进行这样的等同, 那么通过结构上的真的概念定义的谓词逻辑语义学, 与语义学的通俗理解不相容, 可能是因为谓词逻辑语义学被要求以数学方式展开, 而「数学语义学」这个概念本身就是自相矛盾的.
然而, 真正的难点不在于区分语义学和句法学, 而在于构建语义学本身. 无论是在自然语言还是数学中, 解释词语或命题所表达的内容都不是一件容易的事. 如果一开始就存在一种明确准确地表达词语或命题所指内容的方法, 我们肯定会从一开始就使用那种表达方式作为我们的语言. 除非引入病态和极端的表达方式, 否则自然语言就是表达词语意义内容的优秀框架, 根本没有必要特意引入语义学来解释词语的意义内容. 众所周知, 自然语言的语义学是困难的. 但谓词逻辑的语义学也并非被很好地理解.
当然, 我们在这里讨论的话题与当代作为数学的数学基础论几乎没有关系, 因为后者已经失去了与哲学的联系. 对于作为数学的数学基础论来说, 真值计算是否属于语义学, 定理和证明的讨论是否属于句法学, 这并不影响它们作为重要且有用的概念的地位. 但是, 如果当代数学基础论真的与哲学无关, 那么「完备性定理是连接语义学和句法学的定理」这类解释似乎被相当随意地反复提及.
在经典命题逻辑和谓词逻辑确立之后, 出于各种目的, 人们提出了许多新的逻辑系统. 但是, 在大多数情况下, 新逻辑系统的语义学和句法学的基本框架与经典命题逻辑和谓词逻辑的语义学和句法学框架并没有根本区别[8]. 而且, 当提出了无法完全纳入谓词逻辑框架的新语义学和句法学时[9], 我们似乎倾向于根据语义学和句法学的常识或通俗理解, 轻率地批评它们「不是语义学」或「不是证明」. 这种批评实质上只是在说「与我所知道的不同」.
9.3 桌上的白色豆子
如果证明是通过推理的叠加而构成的, 那么追问「什么是证明」就等同于追问「什么是推理」. 而数学和科学中的推理常常被划分为: 将正确的前提引向正确结论的演绎, 以及从个别事例引出一般规律的归纳. 演绎被认为是数学证明中使用的推理, 是数理逻辑学一直在试图阐明的推理[10]. 另一方面, 归纳被视为科学中典型的推理, 是数理统计学中讨论的推理.
当然, 即使将话题限定在数学和科学领域, 也并非所有的推理都可以归类为这两种. 符号学理论的创始人之一皮尔士指出, 为解释观察到的事实而形成假说的推理既不是演绎也不是归纳, 并将这种推理命名为溯因[11]. 皮尔士的溯因是可以称为发现的一种具有代表性的推理, 在与人类创造性推理相关的各个领域受到关注[12].
要准确定义什么是溯因并不容易. 但是, 如果借用命题逻辑和谓词逻辑的框架, 认为为解释逻辑式φ 表示的事实而形成的假说就是满足 T ⊢ φ 的理论 T , 那么从 T 推导出 φ 的推理就是演绎, 反之从 φ 推导出 T 的推理就是溯因. 前者称为「正向推理」, 后者称为「逆向推理」. 当然, 将溯因理解为「逆向推理」也存在局限性和批评. 但是, 由于缺乏其他合适的形式化方法, 这种思路相对来说被广泛采用[13].
作为「逆向推理」的形式化, 溯因具有「不保真、可能出错、没有规则、不可判定」这四个特征. 这四个特征是通常认为的发现推理的共同特征, 或许我们应该认为具有这四个特征的推理就是发现. 但是, 这四个特征是否真正区分了演绎和发现, 需要仔细审视.
在「正向推理」和「逆向推理」中, 导出满足T ⊢ φ 的逻辑式 φ 或理论 T , 推理的结果不仅仅是得到 φ 或 T , 同时还得到了从 T 推导出 φ 的证明. 或者说, 结论为 φ 或前提为 T 只是证明需要满足的条件或规范, 推理的结果其实是证明. 如果这样考虑, 由下文的论证, 就会发现「正向推理」也具有「不保真、可出错、无规则、不可判定」这四个特征. 因此, 这四个特征并没有区分演绎和发现, 或者说, 「正向推理」并没有准确形式化演绎.
首先, 推理保真是指「如果推理的前提全都为真, 那么结论也为真」. 假设T ⊢ φ 成立, 𝕸 是其结构. 根据推理规则的可靠性, 有「 𝕸╞ T 蕴含 𝕸╞ φ」, 从这个意义上说, 「正向推理」是保真的. 另一方面, 即使 T ⊢ φ 成立, 一般来说「 𝕸╞ φ 蕴含 𝕸╞ T 」并不成立, 因此可以确定「逆向推理」不保真. 这也意味着「逆向推理」有错误的可能性, 即「 T ⊢ φ 成立且 φ 为真, 但 T 不一定为真」. 但是, 无论是正向构造证明还是逆向构造证明, 对于得到的证明, 如果从前往后读, 真理就得到保存; 如果从后往前读, 真理就不能保存, 这一点没有区别[14].
关于有错误的可能性, 还有一种错误是将没有形成证明的有限逻辑式序列误认为是证明. 从这个意义上说, 现实中的数学证明中也有很多错误的证明. 在构造形式证明的过程中, 从T 导出不满足 T ⊢ φ 的 φ 的情况也并不罕见. 总之, 就这种意义上的错误而言, 「正向推理」讨论的是「完成的证明」, 「逆向推理」讨论的是「证明的构造过程」, 只是视角不同, 统一视角后「正向推理」也与错误有关.
此外, 要成为合理的假说, 除了正确性之外, 满足「简单、抓住本质」等主观价值标准也很重要, 明确这一标准的难度也是理解发现的难度所在. 但是, 当我们将某个命题称为定理时, 即使不是作为谓词逻辑的专业术语, 而是本来意义上的定理, 也进行了某种主观价值判断, 明确这一标准同样不容易. 从这个意义上说, 「正向推理」和「逆向推理」也没有区别.
不过, 在「逆向推理」中, 从φ 出发导出满足 T ⊢ φ 的 T 确实没有规则. 但作为「逆向推理」结果得到的证明需要遵循推理规则. 从这个意义上说, 「逆向推理」也使用了规则. 另一方面, 在「正向推理」中, 构造证明时也没有关于按什么顺序对哪些逻辑式使用推理规则的规则. 因此, 「正向推理」和「逆向推理」既可以说都有规则, 也可以说都没有规则.
关于可判定和不可判定也是类似的. 在「正向推理」中, 构造证明时使用哪种推理规则也是不可判定的; 在「逆向推理」中, 如果确定了使用的推理规则和逻辑式, 那么导出的作为假设的逻辑式也是可判定的. 此外, 如果可判定的推理就是演绎, 而不可判定的推理就是发现的话, 那么如前所述, 命题逻辑的语义学是可判定的, 句法学是不可判定的, 命题逻辑的语义学和句法学的区别就成了演绎和发现的区别.
「逆向推理」也可以说是保真的. 而且, 没有规则、不可判定、可能出错, 这些跟「正向推理」也并非无关. 总之, 只是因为在「正向推理」中, 问题在于已写出的证明, 而在「逆向推理」中, 话题是证明的构造过程, 所以这四个特征在讨论「逆向推理」时总是成为问题, 而在讨论「正向推理」时却很少被提及. 当然, 这并不意味着演绎和发现没有区别. 但是, 如果演绎和发现可以用这四个特征区分, 那么演绎不一定对应「正向推理」.
在现实的数学中, 证明有时从假设出发, 有时从结论出发, 有时还会更换假设或结论, 是反复试错写成的. 数学中不存在仅由「正向推理」或仅由「逆向推理」组成的推理. 对于写形式化证明也是如此, 无论是朴素证明还是形式化证明, 在讨论证明时, 「正向推理」和「逆向推理」的区别都没有太大意义.
创作证明、理解证明和确认证明的正确性是不同的. 如果演绎和发现这两个概念与证明概念有关系, 那么创作证明可能对应发现, 确认证明的正确性可能对应演绎. 即使理解证明概念需要演绎和发现这两个概念, 演绎和证明的关系也不能用「将演绎写下来就是证明」这种简单的图式来解释.
9.4 隐藏的维度
形式定义的「证明」, 即形式证明, 是从逻辑公理和非逻辑公理出发, 通过反复应用推理规则形成的有限逻辑式序列, 而「定理」是证明的最后出现的逻辑式[15]. 「定理」和「证明」虽然都是有限的符号序列, 但本质上是完全不同种类的存在物. 实际上, 定理和证明有区别也是数学家的切身体会. 在命题逻辑和谓词逻辑中, → 和 ⊢ 都根据「定理」和「证明」的区别被明确区分, 准确把握这一区分是理解命题逻辑和谓词逻辑的第一步.
但同时, 大多数数学家并不区分「φ → ψ 可证」和「在假设 φ 的情况下 ψ 可证」, 即不区分 → 和 ⊢ . 当然, 根据演绎定理, → 和 ⊢ 的等价性已经得到证明, 所以实际上我们不需要区分 → 和 ⊢ . 但数学家并不是从演绎定理学到不需要区分→ 和 ⊢ , 而是一开始就不区分 → 和 ⊢ . 那么, 「定理和证明是不同的」这一切身体会与不区分 → 和 ⊢ 的习惯, 哪一个更合理呢?
在自然演绎的命题逻辑和谓词逻辑系统中, 当能够从假设φ 推导出 ψ 时, φ → ψ 就被定义为已证明, 因此演绎定理是不需要证明的显而易见的事实. 因此, 演绎定理不是关于 → 和 ⊢ 的基本性质的定理, 而应该被视为关于希尔伯特风格的定理和证明的形式化的定理. 如果是这样, 哪些是 → 和 ⊢ 固有的性质, 哪些是与形式化有关的性质, 可能并不总是很清楚. 而且, → 和 ⊢ 的区别本来就是模糊的, 但由于强行形式化定理和证明的概念, → 和 ⊢ 这两个概念可能被硬生生地割裂了. 如果是这样, → 和 ⊢ 的区别只是形式化定理和证明时的副产物, 数学家不区分 → 和 ⊢ 的习惯就是合理的.
但是, 如果→ 和 ⊢ 无法区分, 而且 → 对应定理, ⊢ 对应证明, 那就意味着「定理和证明没有区别」. 通常来说, 「定理和证明是不同的」这一主张似乎是无可辩驳的显而易见的事实, 但认为定理和证明是同类存在物的立场并非完全不可能. 许多年前, 一位研究证明论的朋友告诉我一位伟大的数学基础论学者曾说过[16]: 「定理是证明的省略. 也就是说, 定理和证明的关系就像标题和正文的关系, 定理和证明的区别只是表述详略程度的区别. 确实, 「读了证明才理解定理的含义」这种经历并不罕见[17]. 如果是这样的话, 定理和证明之间可能没有超出说明长短和详略程度以上的区别, 区分定理和证明的常识可能只是毫无根据的想当然.
然而, 数学家通常明确区分定理和证明. 为了尊重数学家不区分→ 和 ⊢ 但区分定理和证明的实际感受, 既不能认为「→ 和 ⊢ 是不同的」, 也不能认为「定理和证明没有区别」, 而需要第三种选择: 「 → 对应定理, ⊢ 对应证明这种说法并不成立」.
无论定理和证明是否相同, 将定理和证明的区别强行塞进→ 和 ⊢ 的区别的框架, 或者认为证明只是详细写出的定理, 都是狭隘的看法. 「→ 和 ⊢ 的区别就是定理和证明的区别」这种想法可能只是命题逻辑和谓词逻辑这个框架带来的固有观念, 从逻辑公理和非逻辑公理出发, 按照推理规则罗列逻辑式就是「证明」, 出现在「证明」最后的逻辑式就是「定理」, 这种理解是不充分的, 我们可能还没有掌握适当地表达定理和证明关系的语言.
在本章开头, 我讨论了语义学和句法学的区别. 无论语义学和句法学的区别是否明确, 确实「语义学和句法学」的二元对立是洞察数学世界的一个坐标轴[18]. 但是, 「定理和证明」的二元对立可能是解读数学世界的另一个坐标轴. 可能有一些东西要同时使用这两个坐标才能看到[19]. 例如, 同时使用这两个坐标轴, 就会发现「证明」没有语义学[20]. 命题逻辑和谓词逻辑只具备命题的语义学, 谓词逻辑中不存在「错误的证明」, 因此不需要「证明」的语义学[21]. 只要证明被定义为有限的逻辑式序列, 证明的意义就要基于逻辑式的意义来确定, 就没有证明本身语义学存在的余地. 谓词逻辑语义学的存在与证明能够用有限的逻辑式序列形式化表示这一信念是成对出现的.
证明确实有意义, 数学家讨论证明的真伪. 本来, 命题的正确性应该由证明的正确性赋予. 基于命题的正确性讨论逻辑公理和推理规则的辩护, 因果关系可能是颠倒的[22].
9.5 数学式纯真
蒯因曾论证, 在分析真理和综合真理之间存在根本鸿沟的信念只不过是教条. 在这个论证中, 他提出了将定义分为三类的观点[23]. 一类是「同义性报告」, 阐明我们模糊持有的同义性观念. 另一类是卡尔纳普所称的「阐明 (explication)」, 分析某个词语的意义或用法, 准确界定这个词语的意义, 有时还会扩展其意义. 这在哲学中有很多例子. 最后一类是作为表达简化引入新词语, 可以称为「命名」.
但是, 在「阐明」中, 被定义词语和定义条件的同义性是通过给出定义才首次意识到的. 因此, 「阐明」与「命名」具有相似性, 这两类定义与「同义性报告」有很大不同. 但是蒯因认为, 即使在「阐明」中, 也存在包含被定义词语和定义条件的语境. 在这个语境中, 被定义词语和定义条件都被赋予意义, 并通过参考这个意义, 「阐明」才作为定义被接受. 也就是说, 蒯因指出,「阐明」也跟「同义性报告」一样, 在给出定义之前就预先假定了对被定义词语意义的理解.
一般来说, 数学家认为「命名」才是定义, 而「同义性报告」和「阐明」是模糊不严谨的论证, 因此不喜欢它们. 哲学中充斥着作为「阐明」定义, 这可能是数学家不喜欢哲学的一个原因. 不过, 「阐明」本来就是试图将模糊的概念明晰化的尝试, 在「阐明」的过程中包含不明晰的部分是理所当然的. 需要区分讨论对象不明晰和讨论本身不明晰. 实际上, 在数学中作为「阐明」的定义也并不罕见, 而且「阐明」和「命名」的区别本身也不明确. 例如, 丘奇-图灵论题无疑是对可计算性概念的阐明[24], 但将到两点距离之和为常数的点集定义为「椭圆」是否属于椭圆概念的「阐明」则不甚明了[25]. 总之,「阐明」这个概念本身就不明确, 对具体的个别定义询问是「阐明」还是「命名」并没有太大意义.
「同义性报告」「阐明」「命名」这个区分可能不是定义本身的分类, 而是定义的解释或作用的分类. 而且, 一个定义在不同语境下可能有不同作用, 这三类并不互斥, 定义的解释也不一定被这三类涵盖[26]. 另外, 模糊的不是「阐明」和「命名」的区别, 而是「阐明」这个概念. 「命名」是什么相对明确, 给定的定义能否解释为「命名」可以被视为这个定义是否数学化的条件. 从这个角度看, 希尔伯特的形式主义可以说是试图明确哪些定义能解释为「命名」, 驱逐包含问题的定义, 只基于能解释为「命名」的定义重构数学世界的尝试.
然而, 所有定义都可以解释为「命名」, 与认为所有定义只是「命名」是不同的. 后者也是一种形式主义, 但与其说是形式主义, 不如称之为「数学式纯真 (mathematical innocence)」, 在不允许模糊性的意义上是一种数学上诚实的态度, 但认为描述数学对象的符号才是数学的实体, 这是狭义的形式主义或极端的唯名论, 能否导向数学的丰富性是非常值得怀疑的[27].
即使对于可以解释为「命名」的定义, 这个定义是否被期望具有「阐明」的作用, 如果被期望的话, 这种「阐明」的尝试是否成功, 这些问题不仅在哲学上需要注意, 在数学上也需要注意.
9.6 缘木求鱼
在谓词逻辑中, 「理论」被定义为称为非逻辑公理的逻辑式的集合, 「证明」被定义为从逻辑公理和「理论」中的非逻辑公理出发, 通过反复应用推理规则得到的有限逻辑式序列. 数学基础论本来就是为了阐明「什么是命题, 什么是证明」而诞生的, 因此谓词逻辑中出现的定义被期望具有「阐明」的作用. 而数学基础论中存在许多看似具有重要「阐明」作用的定义, 所以许多数学家会有「数学基础论不是数学, 而是哲学的空洞讨论」的印象.
但是, 理论本来是指像相对论和伽罗瓦理论那样, 拥有研究对象、方法论以及结果意义的价值判断标准的学术领域. 然而, 谓词逻辑中「理论」的典型例子是群或域的公理集合, 以及自然数全体或集合全体应满足的公理集合. 在这种情况下, 「理论」最多只能描述研究对象及其基本性质, 很难认为「理论」的定义成为了理论概念的「阐明」. 此外, 在谓词逻辑中, 「理论」和「公理系」这个词经常同义使用, 但日常语言中没有「公理系」这个词, 所以「公理系」的定义只能是「命名」. 因此, 「理论」的定义也应该只是「命名」[28].
无论数学基础论中出现的定义是否具有「阐明」的作用, 总之都可以解释为「命名」, 也存在认为只是「命名」的立场. 这也是数学基础论专家切身感受到「数学基础论是数学」的根据. 也有「不应从关于形式化数学得到的结果中引出关于数学本身的言论」这种观点[29]. 这种观点认为「证明」的定义只是「命名」, 或者应该对「证明」定义的「阐明」作用保持沉默. 但是, 不完备定理的素朴解释通常以「证明」的定义是「阐明」为前提, 如果「证明」的定义只是「命名」, 不完备定理的意义就会发生很大变化. 另外, 即使「证明」的定义是「阐明」, 通过这种「阐明」的尝试, 证明的概念本身也可能发生巨大变化[30].
在整个20世纪, 谓词逻辑是精确和形式化分析不限于数学领域且包括自然语言句子和概念的最标准框架. 当然, 丰富的自然语言表达能力和人类认知能力并不能完全囊括在谓词逻辑的框架中. 基于各种视角和问题意识, 人们尝试修改和扩展谓词逻辑. 但是, 这些尝试并没有取得足够的成果. 一个原因是, 这些尝试天真地假定谓词逻辑的「证明」和「理论」定义是「阐明」, 另一个原因是, 谓词逻辑本来就不是为了「阐明」人类思维和认知的全貌而构建的.
谓词逻辑原型的创造者弗雷格将自然语言和他构建的形式系统的关系比喻为肉眼和显微镜的关系, 但显微镜有优于肉眼的地方, 也有不如肉眼的地方[31]. 而谓词逻辑是为了在模型化数学公理化方法这一特殊目的中发挥最大性能, 而故意限制功能, 重新制作弗雷格设计的显微镜而成的东西. 尝试构建自然语言形式语义学的一种——情境语义学的 Barwise 这样说:「基于一阶谓词逻辑的自然语言语义学和认知分析之所以不成功, 是因为这就像缘木求鱼. 一阶谓词逻辑是为了模型化公理化方法而设计的, 并为此发挥了很好的作用[32].」
但是, 谓词逻辑在这个特殊目的上运作良好这一事实, 也不一定是简单的. 例如, 集合论家 Martin 说, 用谓词逻辑给出数学证明的严格定义是令人惊讶的[33]. 不管 Martin 的意图如何, 这个主张有两种解释. 一种是, 人类能够找到谓词逻辑这个定义数学证明的唯一正确方法是令人惊讶的, 这对应于将「证明」的定义视为「阐明」; 另一种是, 尽管谓词逻辑难以说捕捉到命题和证明的本质, 但却能用这个不完善的谓词逻辑给出证明的严格定义是令人惊讶的, 这对应于将「证明」的定义只是「命名」.
也有观点认为, 谓词逻辑采用的将句子分解为主语和谓语的框架源于欧美语言, 与日语不太合拍[34]. 因此, 谓词逻辑的句子分析方法不一定是普遍和自然的. 而且, 即使数学事实的普遍性确凿无疑, 什么是数学方法也会随时代变化, 例如公理化方法直到20世纪才在数学中普及. 如果是这样, 就很难认为存在分析证明的唯一正确的绝对方法, 也不能轻易断言「证明」的定义就是「阐明」, 或者作为「阐明」是成功的.
形式化的「证明」定义可能意在「阐明」朴素的证明概念, 这种尝试可能成功, 也可能失败而只剩下「命名」的作用. 即使成功, 通过这种「阐明」, 证明的概念也可能发生很大变化. 无论如何, 要理解「证明」这个概念, 重要的不是解决「阐明还是命名」的问题, 而是阐明「证明」定义背后有什么样的思路, 给出这个定义后, 我们对证明概念的理解发生了怎样的变化. 思考「阐明还是命名」这个问题是探讨「证明」与朴素证明概念关系的线索, 阐明这种关系应该是理解不完备定理的重要组成部分.
但是, 至少目前在数学基础论中, 「证明」与朴素证明概念的关系很少被讨论. 这首先是因为天真地相信「证明」的定义就是对朴素证明概念的「阐明」[35]; 其次是因为对这个老掉牙的话题提不起兴趣, 周围也没有讨论的人; 最重要的是, 不考虑「证明」和证明的关系也能写论文, 考虑了也写不了论文, 也就是说这是与当前数学基础论无关的问题[36].
9.7 关系代数学
纵观20世纪, 谓词逻辑一直扮演着讨论数学基础的事实上的标准框架的角色, 进入21世纪这一点也没有改变. 但是, 谓词逻辑能自然表达的公理化方法是有限的, 而且与数学漫长的历史相比, 公理化方法在数学中普及也只是最近的事[37]. 谓词逻辑成为事实上的标准框架, 仅靠形式主义数学观的普及无法解释. 数学整体是在集合论而非谓词逻辑之上形式化展开的. 在谓词逻辑这片土地上, 首先有集合论这个基础, 在这个基础之上, 数学这座大厦才拔地而起. 谓词逻辑在数学基础中的成功, 是作为形式化展开集合论的框架的成功.
然而, 用这种谓词逻辑、集合论、数学的三层结构来给数学奠基, 也不是一件简单的事. 在发现集合论中的斯科伦悖论后, 基于集合相关概念的解释依赖于模型的选择而变化这一事实, 斯科伦提出了称为集合论相对主义 (set-theoretic relativism) 的观点, 认为集合相关的各种概念并非普遍的, 并由此得出结论: 集合概念不适合作为数学的基础[38]. 也就是说, 建立在谓词逻辑这片土地上的集合论是摇摆不定的, 因此不适合作为支撑数学这个结构的基础.
从这种集合论相对主义导出的一种立场是, 将集合视为单纯的点, 把集合论看作是一个关于抽象的二元关系∈ 所确定的数学结构的公理化理论[39]. 极端地说, 这种立场不把谓词逻辑、集合论、数学的三层结构视为一个整体, 而是将集合论从数学基础的问题中分离出来, 视为与群论、域论同类的某种代数理论.
谓词逻辑在通常数学中的应用的典型例子是实代数几何. 实代数几何的关键是实闭域上的序, 与集合论中∈ 是二元关系一样, 序也是二元关系. 和、积等运算构成多项式, 与之相对地, ∈ 和序构成逻辑式, 用逻辑式可以研究实闭域的各种数学性质. 也就是说, 通常的代数学是「运算代数学」, 而谓词逻辑是「关系代数学」. 当把谓词逻辑看作「关系代数学」时, 谓词逻辑本身并不是回答「什么是命题」「什么是证明」这类哲学问题的框架. 这种将谓词逻辑视为「关系代数学」的观点, 正是将数学基础论视为数学这一思路的核心.
不过, 即使将谓词逻辑视为「关系代数学」, 形式定义的「证明」概念也不会与朴素的证明概念无关. 将谓词逻辑视为「关系代数学」, 是暂时切断常识意义上的谓词逻辑与哲学的联系, 这是为了摆脱数学思维是演绎的、演绎写出来就是证明这一固有观念, 从而重新面对「什么是命题」「什么是证明」这些哲学问题.
现在有演绎、朴素证明、形式「证明」这三个概念. 标准观点可能是, 朴素证明由演绎构成, 将这种演绎形式化就是形式「证明」. 也就是说, 这三个概念是重叠的, 朴素证明和形式「证明」并非直接相连, 而是通过演绎这个概念联系在一起. 那么, 如果朴素证明和「证明」的概念无法很好地对应, 这并非简单地因为「证明」的概念不恰当, 而可能是因为我们对演绎、朴素证明、「证明」这三个概念之间的关系理解得还不够充分.
推理是我们心智的活动. 我们可能因为将演绎和朴素证明的概念等同起来, 而扭曲了原本朴素的证明概念. 给出形式「证明」定义的谓词逻辑, 不管是否具有演绎性, 都不是理解活生生的人类推理的框架, 而是审视「写出的证明」的观测仪器. 而「写出的证明」是为了理解、信服、解释和说服而进行的言语活动, 是对于数学世界逻辑一致性的观察结果报告. 作为「关系代数学」的谓词逻辑, 支撑着这种观点.
证明与其说是人类思维的记录, 不如说更像电影或戏剧的剧本, 相当于汽车或建筑物等人工制品的设计图. 就像作家写剧本, 技术人员绘制设计图一样, 数学家创作证明, 数学家追求的不是定理, 而是证明. 我们是作为数学活动的结果发现或创造出证明的, 而不是说证明就是演绎的记录. 正如9.3节所讨论的, 如果人类认知活动中有可称为演绎和发现的东西, 那么创作证明就是发现, 确认证明的正确性就是演绎. 而理解证明是一种不同于演绎和发现的心智活动, 似乎应该称之为类似于理解小说或电影的「理解故事」[40].
津ICP备2022002164号-2 © 2016-2023 iHuaBen.com 版权保护声明 不良信息举报:jubao@ihuaben.com
京公网安备11010502036362号