《数理逻辑手册》

此手册是逻辑和数学基础研究丛书第90卷，J．巴维斯主编，34位数理逻辑专家撰写。1977年由北荷兰出版公司出版。手册分模型论、集合论、递归论、证明论与构造性数学四大部分，共31章。每部分前都有一个简短的导言，并且第1、2章是对基本理论的介绍，其它章则是比较深奥的论题。每章后均附有参考文献目录。

模型论部分研究数学语句与数学结构之间的基本关系，特别强调一阶语句的模型论。第1章(一阶逻辑导论)介绍最基本的概念，是手册其它各章的基础。第2章(模型论基础)介绍模型论的基本概念，通过介绍构造模型的6种基本方法及其应用，给出了模型论的一些基本结果。这六种方法是：(1)初等链方法，(2)图像法，(3)紧致性定理，(4)向下勒文海姆－司寇伦定理，(5)省略型定理，(6)模型论力迫法。第3章(超积)讨论超积运算，超积与一阶逻辑的关系，以及超积在代数中的应用。第4章(模型完全性)讨论A．罗宾逊的模型完全理论在代数中肯定和否定两个方面的应用。第5章(相似集)讨论埃伦福希特－莫斯托斯基模型。这种构造不仅是模型论中的有用工具，而且应用于集合论和数学的其它分支时也非常有用。第6章(曲线和曲面的无穷小分析)是模型论在代数和集合论之外的应用，属于非标准分析。通过对无穷小在曲线和曲面几何研究中的一些基本应用分析，揭示了无穷小量在微分几何中的作用。第7章(可允许集和无穷长逻辑)讨论逻辑Lωω和它的可允许片断的模型论。第8章(范畴逻辑的学说)综述逻辑中，特别是模型论和集合论中的范畴方法。最后两章的内容不属于一阶逻辑，第1、2两章的最后一节讨论一阶逻辑的扩张，也不属于一阶逻辑，手册中与模型论密切相关的内容有递归论中的《可判定理论》和《归纳定义》两章。

集合论部分介绍一些重要的独立性和协调性结果，以及得到这些结果所用的方法。第1章(集合论公理)在对集合概念直观说明的基础上，介绍了集合论的ZF公理系统。这里对集合概念的说明不仅在说明集合论公理的正当性方面，而且在寻找新的公理和证明有关集合的定理方面都十分有用。第2章(选择公理)通过讨论选择公理AC在数学中的一些典型应用，解释了它所处的特殊地位。对一些不满足选择公理的集合论模型的讨论，揭示了哪些定理必须使用选择公理，以及选择公理各种弱的形式和它的推论的意义。还介绍了有关AC的独立性和协调性结果。第3章(组合学)讨论集合论中有广泛应用的无穷组合原则。表明了如何把AC、CH(连续统假设)和◇(詹森组合原则)看作渐强的“枚举”原理，以及何时应该使用哪一个。还讨论了拉姆齐定理和它的各种推广，以及大基数的组合性质。第4章(力迫)介绍P．J．柯恩为证明AC和CH的独立性所发明的力迫法及其应用，该方法经改进和简化已经成为获得独立性和协调性结果的重要工具。第5章(可构成性)介绍K．哥德尔在1938年引进的可构成模型L和有关的协调性结果，即选择公理和广义连续统假设的协调性，以及R．B．詹森关于L的进一步研究。第6章(马丁公理)介绍马丁公理MA的偏序形式，MA与CH之间的关系，以及MA的一些组合推论。第7章(拓扑学中的协调性结果)说明如何利用集合论中的一些假设，如马丁公理、詹森的组合原则◇来证明拓朴定理或构造反例。手册中与集合论相关的有递归论中的《描述集合论》、《不可解度》(其中第4节讨论度与公理集合论间的相互关系)和模型论中的《相似集》(其中最后一节讨论大基数与L的关系)。

递归论部分有狭义和广义之分，前4章属于狭义递归论，研究自然数上的递归或能行可计算函数类及其在数学中的应用；后4章属于广义递归论，研究任意数学结构上的递归过程。第1章(递归论基础)从可计算性的非形式概念和A·M·图灵的递归概念着手，讨论著名的丘奇论题。除介绍递归论的其它一些基本概念和基本结果外，还讨论了递归论与逻辑和可定义性之间的关系。第2章(不可解问题)应用递归函数的理论讨论了一些重要的不能能行判定的问题，包括停机问题、希尔伯特第10问题、群的字问题等。第3章(可判定理论)介绍建立一个数学理论的可判定性的三种主要方法：量词消去法、模型论方法和解释法，以及应用它们建立的各种可判定性结果；还介绍了判定程序的复杂性问题。第4章(不可解度)除介绍度的一些基本概念外，综述了有关不可解度的重要结果，并对这些结果作了一些方法论评论。第5章(α－递归论)是关于递归论在可允许序数上的推广，这里不仅介绍了α-递归论的基本概念和思想，给出了目前所探讨的重要问题和研究领域，而且还报告了该研究方向的最新进展和所使用的技术；并运用α－递归论中一个典型定理(分离定理)的证明作了具体说明。第6章(高阶型的递归论)借助归纳可定义性的一般理论介绍了它的基本概念和一些重要结果。第7章(归纳定义导论)介绍了各种形式的归纳定义，主要是单调归纳以及它在递归论的扩张中的作用，对有关非单调归纳的研究也作了介绍；还简单考查了归纳定义在基础研究中的作用。第8章(描述集合论)讨论递归论在描述集合论中的应用，分别介绍了古典的和能行的描述集合论，重点是投影集的理论；讨论了描述集合论中ZFC公理不能回答的一些有关投影集的基本问题，以及如何应用更强的集合论假设——决定性假设来回答这些问题。手册中与递归论相关的内容有模型论中的《可允许集和无穷长逻辑》、证明论中的《艾尔布朗定理和根岑的直接证明的概念》和《与数学实践相关的有穷类型论》。

最后一部分中的证明论应用现代数学工具把证明本身作为数学对象来研究，它起源于希尔伯特方案。与这个方案密切相关的是K．哥德尔的两个不完全性定理，第1章(不完全性定理)对它们作了详尽的介绍。第2章(切割法的应用)涉及当今证明论主要关心的两个问题：(1)从一个仅仅知道为真的命题到能够在一个特定理论中证明它，我们究竟获得了什么?(2)数学的和证明论的原则之间的关系。作者以古典算术为例，对这两个问题作了精辟的回答，表明G．根岑的切割法是如何能够用于对这类问题的研究。第3章(艾尔布朗定理和根岑的直接证明的概念)以等式演算为例讨论了上述第一个问题，并给出了肯定回答。第4章(与数学实践相关的有穷类型论)讨论反映数学实践的逻辑特性的各种有穷类型的形式理论，说明了在这些理论中可以展开数学；通过独立性结果研究了这些理论间的相对强度；应用各种证明论方法，如根岑的切割法、哥德尔的函数解释法获得了有关这些理论的二阶内容的精确信息。第5章(构造性数学面面观)从逻辑的作用、逻辑算子的解释、连续的量化理论的可能性、直觉主义谓词逻辑的有效性和数学假设之间的联系等方面，讨论了证明的构造性概念。第6章(拓扑斯逻辑)讨论直觉主义和范畴论的拓扑斯(topos)概念之间的关系，主要讨论高阶直觉主义逻辑的代数形式。第7章(无类型的λ－演算)在介绍古典λ－演算的基础上报告了这个研究领域中的一些新进展。最后1章(皮亚诺算术中数学不完全性一例)具体给出了有穷组合中的一个定理，尽管为真，但却不能在一阶皮亚诺算术中得到证明。