数据词典：数理逻辑（Mathematical Logic）

赵老师

数理逻辑（Mathematical Logic）是指用数学方法研究的逻辑，又称符号逻辑。所谓数学方法是指数学采用的一般方法，包括使用符号和公式，使用已有的数学成果和方法，特别是使用形式的公理方法。其思想可以追溯到17世纪的G. W. Leibniz，他试图建立一种精确的、普遍的符号语言，并寻求一种推理演算，以便用演算来解决推理的问题。数理逻辑是由一些数理逻辑的先驱者沿着Leibniz的思想进行了实质性的工作以后，而逐步完善和发展起来的。

公理方法是数学中广泛使用的一种方法。数理逻辑采用了完全形式化的公理系统，即形式系统。形式系统由它的语言、公理和推理规则三部分构成。

形式系统的语言一般采用人工语言, 又称为形式语言。建立一种形式语言, 首先要规定语言的符号。由这些符号根据某些确定的形式规则而得到的符号的有穷序列, 称为公式。这些形式规则就是公式的形成规则。事实上, 公式是人们希望经过解释有意义的形式语言中的有穷序列。

形式系统的公理是需要系统加以肯定的论断的公式，并称这样的公式为有效公式。例如, 命题演算的有效公式是重言式，谓词演算的有效公式是逻辑有效式，群论的有效公式是在每个群中都解释为真命题的公式。当然, 有效公式很多，只取其中一部分作为公理, 为了推出其余的有效公式，需要引进推理规则。推理规则说明，如何由某些公式(称为该规则的前提) 获得一个公式( 称为该规则的结论)。公理和推理规则一旦给定，形式系统的全部定理就完全确定了。形式系统的定理归纳定义如下: ① 每个公理都是定理；② 若推理规则的前提都是定理，则其结论是定理；③ 每个定理都可通过有穷次应用①和②获得。如果推理规则有有穷多个前提，则称该规则是有穷的。例如，分离规则是有穷的，因为它只有两个前提。命题演算和谓词演算的推理规则也都是有穷的。在大多数情况下，只使用有穷规则。但有时需要非有穷规则，例如在无穷长语言逻辑中。

如果公理集是递归集，每条推理规则对应的判定问题是可判定的，即可以能行地确定是否可用该规则由一组公式得到一个公式，则定理集是递归可枚举集。称定理集是递归集的形式系统为可判定的，称定理集是递归可枚举集的形式系统为半可判定的。例如，命题演算是可判定的，谓词演算是半可判定的。

一个形式系统由它的符号集、公式的形成规则、公理集和推理规则集完全确定。形式系统本身是一个纯语法对象。形式系统的解释或意义称为语义。通常，形式系统都有逻辑推理系统或数学公理系统作为它的背景。

形式系统的协调性、独立性、可靠性和完全性是数理逻辑中经常研究的元理论性质。协调性和独立性给出了形式系统的语法性质。如果至少有一个公式不是形式系统的定理，则称该系统是协调的。如果形式系统没有多余的公理和推理规则，即只要去掉任何一个公理或推理规则，系统的定理就会减少，则称该系统是独立的。例如, 命题演算和谓词演算都是协调的。可靠性和完全性给出了形式系统的语法性质和语义性质之间的关系。如果形式系统的定理都是有效的公式，则称该系统是可靠的。反之，如果有效的公式都是形式系统的定理，则称该系统是完全的。建立可靠且完全的形式系统常常是逻辑学家向往的目标，但并非总是能够如愿以偿。例如，对于高阶逻辑就不存在可靠且完全的形式系统。

用形式化方法处理逻辑推理(特别是数学中所用的推理) 的思想是数理逻辑最初的思想。20 世纪，由于数学奠基问题的研究而形成了四个数理逻辑分支，即模型论、公理集合论、递归论和证明论，它们构成了现代数理逻辑的主要内容。

模型论是研究形式语言和对它的解释(结构)之间的关系的理论。一个形式语言的解释称为此语言的一个结构(模型)。这是一个具有若干运算、关系及特指元素的非空集合，也称为泛代数。所以模型论又被形容为“泛代数+逻辑”。

如果在研究模型论时关心的预定模型是集合论，那就进入了公理集合论的范围。不能把公理集合论看作模型论的一个分支。各门数学中的概念、定义、定理和证明都可以用集合论语言来表达。因此，奠定数学基础就成为奠定集合论基础，归结成为公理集合论的研究。G .Cantor 于19 世纪70 年代创立了集合论。B .Rus sell 于1902 年发现了罗素悖论。为了排除罗素悖论以及其它悖论，E .Zermolo于1908 年提出了集合论的第一个公理系统。后经过A .Fr aenkel 的改进成为ZF系统。另一个广泛应用的集合论公理系统是J .von Neumann、P .Bernays和K .Godel 提出的GB系统。到目前为止, 在公理集合论中还没有发现悖论。

证明论也称元数学。它是以数学证明作为研究对象的数学。20 世纪20 年代初, D .Hilbe rt 提出了一个论证数论、集合论或者数学分析的协调性的方案。他提出首先将这些理论形式化，然后按照有穷方法证明这些形式系统是协调的。1931 年Godel发表了不完全性定理。该定理指出，一个半可判定的协调的数学理论, 只要包括初等数论，那么这个理论就是不完全的，即总有闭公式A 使得A 和A 都不是该理论的定理。哥德尔第二不完全性定理还说，如果一个包含初等数论的数学理论是协调的，则其协调性不能在该理论中证明。这说明了希尔伯特方案是行不通的，使证明论的内容发生了变化。哥德尔不完全性定理揭示了形式化方法的局限性，对数学、计算机科学和其它科学的发展都产生了深远的影响。

递归论也称算法论，是研究算法、可计算性和不可计算性的数学。它研究算法的一般规律，研究数学的问题类是否存在着算法解。一类问题存在算法解就是这类问题都是可解决的； 一类问题不存在算法解，就是这类问题不都是可解决的。研究问题类的可解决性和不可解决性就是数理逻辑中的判定问题，这是关系到全部数理逻辑的问题。递归论与构造性数学不可分，是构造性数学的理论基础。

从最广义的角度上看，数理逻辑除包括以上内容外, 还包括归纳逻辑、模态逻辑、多值逻辑、时态逻辑等，它仍然是用数学方法研究的逻辑。所以，数理逻辑包括了演绎逻辑与归纳逻辑、单调逻辑与非单调逻辑、二值逻辑与多值逻辑、一阶逻辑与高阶逻辑等在经典与非经典意义上的逻辑。演绎逻辑是研究演绎推理的逻辑，如谓词逻辑。归纳逻辑是研究归纳推理的逻辑，对于单调逻辑，增加公理或推理规则不会使推得的定理减少。对于非单调推理，增加公理或推理规则可能会使原来可以推出的定理不再能推出。多值逻辑研究多于二值的逻辑演算，即三值以至更多值的逻辑演算。对于一阶逻辑演算中的一阶谓词和一阶函词进行量化，这样就有由一阶逻辑演算扩充成为高于一阶的二阶逻辑演算了。类似地，对于任何正整数n，可以有n 阶逻辑。

在进入20 世纪70 年代后，由于科学技术的发展，在各研究领域中都涉及了思维逻辑规律的问题。数理逻辑及其应用正迅速地发展。例如，用于数学的无穷长语言逻辑、高阶逻辑、具有广义量词的逻辑；用于哲学和社会科学的道义逻辑、存在逻辑、断定逻辑；用于物理学的量子逻辑等。值得指出的是，数理逻辑与计算机科学有着十分密切的关系，它是反映现代数理逻辑基本特点的重要方面。

在Leibniz的思想中，数理逻辑、数学和计算机三者均出于一个统一的目的，即思维过程的演算化、计算化以至在计算机上实现。早在20 世纪30 年代，数理逻辑将推理化为一些简单机械的动作，提出了图灵机这一计算机的抽象模型，并证明了存在通用图灵机，这正是40 年代出现的存储程序计算机(即冯·诺伊曼计算机) 的理论原型。

推理与计算是相通的，数理逻辑的研究成果许多都可用于计算机科学。例如, 原则上数理逻辑已给出了哪些思维过程可以借计算机实现。同时，计算机科学的深入研究推动了数理逻辑的发展。例如，一阶逻辑中没有时间的概念，而关于程序的推理是涉及过程的，因此需要增加程序算子或其它包含时间概念的算子，以便适用于过程的推理。

数理逻辑倡导的形式化方法已广泛渗入到计算机科学的各个领域中，如软件规范、形式语义学、程序变换、程序正确性证明、硬件综合和验证等。程序逻辑、算法逻辑、动态逻辑、时态逻辑在形式化方法中有许多应用。在人工智能科学中，人们用数学方法研究非单调推理， 以便用计算机模拟人的思维，例如非单调逻辑等。相信在科学技术的数学化的发展中, 数理逻辑将会不断地起着关键的作用。

【出处】张效祥. 计算机科学技术百科全书,清华大学出版社,2018年5月第3版.