“我们都知道数学家对逻辑的关心从未比逻辑学家对数学的关心更多。数学和逻辑学是精密科学的两只眼睛，但是数学家对逻辑视而不见，逻辑学家对数学视而不见。双方都相信自己只用一只眼比用两只眼视物更清楚。”
——德摩根
莱布尼兹曾经有两个梦想：
1. 创建一种“普遍语言”（characteristica universalis）使得任何问题都可以用这种语言表述；
2. 找到一种"判定方法"（decision method）以解决所有可以在“普遍语言”中所表述的问题。
这两个问题是上百年来数理逻辑、数学哲学和数学基础问题的核心、实质。对前一个问题的回答就是自弗雷格、罗素开始，经公理集合论运动的最终结果：以一阶谓词逻辑为语言所形式化阐述的集合论，现在已经成为数学的普遍语言，现代逻辑学、特别是将符号逻辑应用于数学领域所产生的数理逻辑，其最重要的目标就是为整个数学提供一个严格精确的语言。这是我们在学习数理逻辑时应当把握的方向。
而第二个问题则是现代哲学和计算机科学最关注的问题之一：是否可以解决用这个“普遍语言”所形式化描述的所有问题？这个问题就是所谓“可判定性问题”（Entscheidungsproblem，decision problem）。对这个问题的研究最终导致了理论计算机科学的诞生：阿隆佐·丘奇和阿兰·图灵分别以各自的方式对这个问题做出了否定的回答。他们在研究这个问题时首先对“可判定的”（decidable）这个直觉概念进行了深入研究并给出了形式化定义和解释，进一步把这个问题归结成“可计算的”（computable）问题，并最终将其定义为“可计算函数”（computable function）问题的研究。为此，丘奇和图灵分别提出了关于可计算函数的模型。图灵的模型就是著名的图灵机，它已经成为现代计算机科学的理论基础；而丘奇的模型则是lambda演算，这成为后来计算机语言Lisp和现代函数式程序语言的理论基础。其后图灵证明了这两个模型其实定义了同一类别的可计算函数。可以说，丘奇和图灵对数理逻辑的研究是从传统的解决数学基础问题出发开创了一个崭新的领域：计算科学。
与此同时，美国数理逻辑学家哈斯凯尔·克里（Haskell Curry，又称柯里）在研究怀特海/罗素的类型理论时发现了逻辑中的蕴含命题可以归结成类型问题，从而使得证明论研究可以转化为对类型理论的研究。对这个问题的更深入研究始于1969年威廉·霍华德（William Howard），他的研究表明，逻辑与类型论之间的对应关系可以从多个逻辑系统得到，从而将逻辑学的证明论与计算理论归结为同一理论的两个侧面，这就是著名的克里-霍华德同构（Curry-Howard isomorphism）。
由此来看，数理逻辑所研究的最本质主题有两个：形式系统的表述能力(the expressive power）和形式证明系统的演绎能力(the deductive power)。 对一阶谓词的语义学的研究导致了模型论的出现，而对逻辑的核心问题推理的形式化研究特别是20世纪初希尔伯特的公理化研究演化成证明论、而对自然数集合及其函数的研究催生了递归论的出现，而集合论则是所有数学分支的基础语言。从这些领域出发又可派生出和其它领域相关的子分支，例如从模型论派生出形式语义学，从证明论派生出以产生式系统为核心概念的形式句法，从递归论派生出可计算性和计算复杂性以及可计算函数的研究。从集合论出发，产生出了更抽象的范畴论，而集合论本身已经成为所有数学分支的基础语言。
因此，现代数理逻辑的学习，大致包括了两个方面：符号逻辑学基础：一阶逻辑（莱布尼兹第一问题，语言问题），逻辑应用（演绎推理问题）：数学公理化和建构性数学（constructive mathematics）、以及理论计算机科学的核心问题：可计算函数的研究以及相关的可计算问题和计算复杂性问题。
“所有科学的宏大目标都是：从最小数量的假说或公理出发通过逻辑演绎推理说明最大数量的实验事实。 ”
—— 阿尔伯特·爱因斯坦
评论 (0)