简明数理逻辑

写作结构清晰，层次分明，突出重点，文字简洁易懂，注重与其他学科的关联

《简明数理逻辑》首先简要介绍了数理逻辑的发展、形式系统及一些预备知识，然后介绍了集合论，详细讲解了命题演算、谓词演算、可计算性理论和哥德尔不完全性定理，*后介绍了模型论的基础知识和方法。《简明数理逻辑》重点突出，论证详细，各部分内容配有典型的例子和习题，以便读者更好地理解、掌握相关知识。

写作结构清晰，层次分明，突出重点，文字简洁易懂，注重与其他学科的关联

目录
丛书序
前言
第1章 绪论 1
1.1 数理逻辑发展简介 1
1.2 数学定义、证明与定理 5
1.3 证明方法 7
第2章 集合论 10
2.1 集合 10
2.1.1 对象及其名称 10
2.1.2 集合的定义 11
2.1.3 集合的表示 11
2.1.4 罗素悖论 12
2.1.5 公理化方法 13
2.1.6 外延公理和空集公理 13
2.1.7 子集 14
2.1.8 分离公理 14
2.1.9 无序对和单点集 15
2.1.10 交集 16
2.1.11 并集 16
2.1.12 集合的差 18
2.1.13 幂集 19
2.1.14 广义并 20
2.1.15 广义交 20
2.2 关系 21
2.2.1 有序对 21
2.2.2 笛卡儿积 22
2.2.3 二元关系 23
2.2.4 关系的运算 24
2.2.5 像与原像 25
2.2.6 等价关系 26
2.2.7 偏序关系 27
2.2.8 良序关系 29
2.2.9 多元关系 30
2.3 映射 31
2.3.1 映射的定义 31
2.3.2 单射、满射和双射 34
2.3.3 序同态与序同构 36
2.3.4 集族 37
2.3.5 广义笛卡儿积 37
2.3.6 选择公理 38
2.3.7 多元映射 38
2.4 归纳证明与归纳定义 39
2.4.1 自然数的定义 39
2.4.2 数学归纳法 40
2.4.3 归纳定义 43
2.5 有穷集合和无穷集合 47
2.5.1 等势集合 47
2.5.2 康托尔-伯恩斯坦定理 49
2.5.3 有穷集合 51
2.5.4 可数集合 52
2.5.5 无穷集合 53
2.5.6 不可数集合 54
2.6 序数与基数 56
2.6.1 序数 56
2.6.2 超穷归纳法 59
2.6.3 可数序数 61
2.6.4 基数 62
2.6.5 基数算术 64
第3章 命题演算 66
3.1 命题演算的形式语言 66
3.1.1 命题演算的形式符号 66
3.1.2 形成规则 67
3.2 命题演算的语义 68
3.2.1 赋值、真值表、重言式 69
3.2.2 代入 72
3.2.3 语义后承 73
3.2.4 紧致性定理 73
3.2.5 等价与替换 75
3.2.6 联结词的个数 76
3.3 命题演算的公理及推理规则 77
3.4 形式证明及形式定理 78
3.5 形式推演 78
3.6 推演定理 82
3.7 导出规则及辅助推演规则 84
3.8 斜式推演 85
3.9 可靠性定理 90
3.10 范式与完全性定理 91
3.11 联结词完全性 96
第4章 谓词演算 97
4.1 一阶谓词逻辑的形式语言 97
4.1.1 符号系统 97
4.1.2 形成规则 98
4.1.3 自由变元与约束变元 99
4.2 谓词演算的语义 100
4.2.1 一阶语言的结构 100
4.2.2 指派与项的取值 101
4.2.3 满足关系 103
4.2.4 语义后承 107
4.3 谓词演算的公理系统及推理规则 108
4.3.1 谓词演算的形式证明 109
4.3.2 形式推演 109
4.4 谓词演算的可靠性定理 110
4.5 推演定理 112
4.5.1 依赖性与变化性 113
4.5.2 谓词演算的推演定理 115
4.6 谓词演算的推演规则 118
4.7 斜式推演 121
4.8 具有特殊句法结构的公式 123
4.8.1 前束范式 123
4.8.2 公式分层 125
4.8.3 斯科伦范式 126
4.9 完全性定理与紧致性定理 127
第5章 可计算性理论 129
5.1 部分递归 129
5.1.1 原始递归函数 130
5.1.2 部分递归函数 132
5.1.3 递归函数 133
5.1.4 递归关系 135
5.2 图灵可计算函数 137
5.2.1 单带确定图灵机 137
5.2.2 多带图灵机 141
5.3 图灵计算的算术化 145
5.3.1 图灵机的编码 145
5.3.2 计算的算术化 147
5.4 丘奇-图灵论题 150
5.5 通用图灵机 151
5.5.1 通用函数 152
5.5.2 s-m-n定理 153
5.5.3 通用函数的应用 155
5.6 不可判定性 158
5.7 部分可判定性 162
5.7.1 部分可判定谓词 162
5.7.2 递归可枚举集 166
5.7.3 集合间的多一归约 169
5.8 图灵计算的逻辑刻画 172
5.9 递归定理 175
5.10 神谕图灵机 181
5.10.1 神谕图灵机的配置 181
5.10.2 神谕图灵机的编码 183
5.10.3 相对于A的递归集与r.e.集 184
5.10.4 图灵归约与图灵度 185
第6章 哥德尔不完全性定理 188
6.1 皮亚诺算术系统PA 188
6.1.1 皮亚诺算术系统 188
6.1.2 PA的语义 190
6.2 序关系 191
6.3 可表示性 193
6.4 哥德尔编码 196
6.5 元数学的算术化 197
6.6 哥德尔不完全性定理的证明 200
第7章 模型论 207
7.1 结构之间的关系 208
7.1.1 子结构 208
7.1.2 初等子结构 210
7.1.3 同态与同构 210
7.1.4 嵌入与初等嵌入 211
7.1.5 初等等价 212
7.1.6 膨胀与收缩 212
7.1.7 图像与初等图像 213
7.2 完全性定理与紧致性定理的详细证明 213
7.2.1 完全性定理 213
7.2.2 斯科伦化 218
7.2.3 紧致性定理 220
7.2.4 全称型理论的模型论刻画 223
7.3 完全理论与模型完全理论 223
7.4 部分同构 230
7.4.1 部分同构与有穷同构 230
7.4.2 Fra*ssé定理 232
7.5 量词消去 235
7.6 内插定理 238
7.6.1 命题逻辑的内插定理 238
7.6.2 谓词逻辑的内插定理 238
7.6.3 Beth可定义性定理 241
7.7 Ⅱ2-理论的模型论性质 242
7.8 型省略定理 245
7.8.1 相对于结构的型 245
7.8.2 相对于理论的型 248
参考文献 250
索引 251

第1章 绪论
　　现在，人们对逻辑的理解已经很宽泛了。一般而言，逻辑学是研究推理的有效性(或称可靠性)的学问。通俗地讲，推理就是连续使用推理规则的过程，而推理规则就是从前提直接得出结论的原则。一个有效的推理规则是指，如果前提是真的，则由该规则得出的结论必然是真的。经典的逻辑学就是要研究哪些推理规则是有效的，而数理逻辑则是研究数学的可靠性的学问。
　　1.1 数理逻辑发展简介
　　对逻辑推理的形式化处理可以追溯到亚里士多德(Aristotle)。早在公元前350年，亚里士多德通过对各种推理模式的分析，提出了三段论。例如，下面两个都是有效的三段论规则：
　　两千多年来，可以说，三段论在人类教育、文化、科学研究中起着至关重要的作用，曾一度被认为是推理的唯一逻辑范式。即使是现在，它也是逻辑的重要组成部分。亚里士多德的贡献还在于：可以把推理看成对符号的操作。
　　德国数学家、哲学家莱布尼茨(G. W. Leibniz)是数理逻辑的先驱。亚里士多德的思想(如把概念分解成固定的“范畴”、把推理简化为形式规则)极大地唤起了莱布尼茨的数学才能和激情。莱布尼茨青年时期，全世界的数学研究迅速发展，处理代数表达式的方法已经系统化。笛卡儿和费马的工作表明，通过引入直角坐标系，可以把几何还原为代数。特别是莱布尼茨(或牛顿)创立了微积分，并成功引入微积分运算符号，使得人们容易理解微积分。这些都说明了一个数学理论实际上就是一个符号系统，数学运算就是对符号表达式的操作。同时，这些成功范例激发了莱布尼茨建立通用语言的信念：建立一个可以表达人类思想的符号系统，其中每个符号都以一种自然的方式表示一个确定的概念，进而发展出一种语言及操纵这些符号的工具，使得仅凭符号演算，就可以确定用这种语言写成的哪些句子为真。这就是著名的“莱布尼茨之梦”。
　　莱布尼茨之后，数理逻辑研究处于不活跃的停顿时期。这段时间逻辑学家[如哈密尔顿(W. Hamilton)、德 摩根(A. de Morgan)]大都致力于传统逻辑的修补工作。直到1847年，英国数学家布尔(G. Boole)发表了《逻辑的数学分析》，他把逻辑中的合取与析取看成数值运算，进而创建了能表示逻辑演算的代数系统(称为逻辑代数、命题代数或命题函数代数)。布尔明确指出，凡是能用传统逻辑处理的问题，用命题代数也能处理。他还举出很多问题，并指出用传统逻辑来处理这些问题非常困难，但用命题代数处理却很容易。布尔的贡献在于：第一，布尔的工作表明逻辑可以成为数学的一个分支;第二，布尔的命题体系包含了亚里士多德的逻辑;第三，布尔的命题代数部分实现了莱布尼茨梦想的通用语言。然而，布尔的命题代数距离莱布尼茨的梦想还十分遥远，比如，布尔逻辑不能处理诸如“所有的猫或是白色的或是黑色的”这样的命题。
　　数理逻辑的发展主要有两个动力：一是上面谈到的，人们认识到传统逻辑的不足，需要加以改进；二是数学基础的研究产生了大量与逻辑有关的问题。历史上，数学曾经发生了两次大危机：第一次是古希腊时期“无理数”的发现，这次危机导致了欧氏几何的兴起；第二次则是17、18世纪关于微积分基础的争论。不管是(欧氏或非欧)几何学还是微积分理论，它们的基础都依赖于实数理论的协调性(即无矛盾性)。19世纪中期，康托尔(G. Cantor)创立了集合论。戴德金(R. Dedekind)和康托尔利用集合论来定义实数。根据这个定义，可以纯逻辑地推出极限理论，也可以推出整个微积分学，从而整个数学基础就建立在集合论之上了。因此集合论的协调性就占有至关重要的地位。那么集合论的基础是什么呢？到了19世纪，数学基础的研究越来越受到关注。
　　莱布尼茨梦想建立一种通用语言，使之能够表达所有真理。这说明莱布尼茨把逻辑看成包含一切科学所依据的观念。弗雷格(G. Frege)认为逻辑是数学的基础，一切数学都可以建立在逻辑的基础之上。即数学的概念须用逻辑概念来定义，而数学真理可以由逻辑原则推导出来。这就是逻辑主义的观点。为此，弗雷格试图找到一个包含数学实践中的所有推理的逻辑系统。布尔的工作表明逻辑可以成为一个数学分支。在弗雷格看来，这是用逻辑来发展逻辑，产生了循环。因此，弗雷格认为，他的逻辑系统是不能用逻辑来发展的，而是要采用精确的语法规则或句法规则把他的概念文字发展成一种人工语言，进而把逻辑推理表示为机械的符号演算，这就是所谓的形式系统。1879年，弗雷格出版了他的小册子《概念文字》(Begriffsschrift)，副标题就是“一种模仿算术语言的纯思维的形式语言”，其中完善地发展了一阶逻辑系统(通常记作 FOL)。FOL 揭示了演绎推理过程是连续执行某些简单推理规则的过程。我们只需注意规则的执行，而无须理解各种符号的含义。哥德尔(K. G.del)1930年的博士论文证明了弗雷格的规则是完全的。这就表明，弗雷格是第一次给出了能够解释所有演绎推理的形式系统。不过，从数理逻辑的发展历史看，完全严格的逻辑演算系统是由希尔伯特(D. Hilbert)和阿克曼(W. Ackermann)在其合著的《数理逻辑基础》中给出的。1885年，皮尔斯(C.S. Peirce)也独立地引进了量词。后来他的工作由施罗德(E. Schr.der)继承并发展，*后集中在《逻辑代数讲义》一书中。皮尔斯的工作影响较大。但是，即使是在《逻辑代数讲义》一书中，其谓词演算仍然没有弗雷格的那样完善。
　　弗雷格认为一阶逻辑只是朝着他的目标迈进的第一步。在19世纪，他已经把数学基础研究归结到了为自然数理论提供基础。弗雷格希望为自然数理论提出一种纯逻辑的理论，进而证明算术、实数理论、微积分乃至整个数学都可以被看作逻辑的分支。这就是被后人称之为“逻辑主义”的观点。弗雷格关于算术基础的著作阐述了如何利用他所提出的逻辑发展算术理论。弗雷格的思想是把自然数看成集合的“集合”，例如，“3”这个数等同于所有恰含有“3”个元素的集合的“集合”。然而，1902年，正当弗雷格的《算术基础(第二卷)》即将出版时，他收到了英国哲学家罗素(B. Russell)的信，信中指出了弗雷格的系统是矛盾的。这就是著名的罗素悖论。这对弗雷格来说是一个沉重的打击，可他不得不接受这个现实。直到1925年去世，他都认为自己的工作毫无结果。更不幸的是，弗雷格的工作当时也不为同事们所认同。虽然如此，弗雷格的工作还是产生了深远的影响。他的《概念文字》被后人誉为“也许是自古以来*重要的逻辑学著作”，后来的皮亚诺(G. Peano)算术系统被认为是算术理论的形式化，集合论公理系统(如 Zermelo-Fraenkel 系统)被认为是数学的基础。
　　弗雷格的书一开始根本没有受到人们的关注，他的学说一直没人理睬。直到罗素完成了自己的研究以后，才看懂了弗雷格的书，发现两人竟然不谋而合。经罗素的宣扬，弗雷格的工作才受到人们的关注。可见，罗素是弗雷格的坚定支持者。为了避免弗雷格系统中的矛盾，罗素把对象分成0-型，1-型，2-型， 并规定 i-型对象可以是(i+1)-型对象的元素，但反之不然，进而罗素发展了他的类型论，并在类型论中定义数学概念，证明数学定理。罗素和怀特黑德(A.N. Whitehead)合著的《数学原理》(三卷，1910—1913年)是当时数理逻辑成果的总汇。
　　罗素的工作表明，许多数学定理的确可以由几个简单的公理出发逻辑地推导出来。但是，逻辑主义却遭到了多方面的批判。首先，罗素把某些集合论原则看成逻辑原则的思想不被人们所接受。其次，逻辑主义把所有自然数的全体看成具体存在(即无穷公理)，这遭到了以布劳威尔(L.E.J. Brouwer)、外尔(H. Weyl)为代表的直觉主义者的严厉批判。还有，逻辑主义者难以成功的根源在于，没有意识到如何证明他们的系统包含了整个数学。
　　希尔伯特不赞同逻辑主义的某些观点，更不能容忍直觉主义者把无穷对象完全驱逐出去。希尔伯特继承了逻辑主义的形式系统的思想，他认为应该建立数学和逻辑的形式系统。与逻辑主义不一样的是，希尔伯特区分了逻辑公理和数学公理，但认为应对二者予以统一处理。和直觉主义一样，希尔伯特认为构造性数学才是*可靠的，而包含无穷对象的数学的可靠性是值得怀疑的。但和直觉主义不同的是，他认为不能把所有无穷对象从数学中驱逐出去。
　　希尔伯特于1920年提出了著名的“建立数学基础”的计划。首先建立逻辑和数学的形式系统(通常试图作为某一理论的形式化)。希尔伯特特别强调要把整个形式系统作为研究对象。例如，我们*关心的问题有：该系统会不会导出矛盾，是不是足够丰富(即是不是具有完全性：被形式化的理论中的真理是不是在形式系统中可证)。
　　研究整个形式系统的理论称作“元数学”(或叫“元理论”)。当处理一个具体的形式系统时，该形式系统本身也是一套理论体系，我们称之为“对象理论”。值得注意的是，我们必须把形式系统内的符号和元数学符号严格区分开来，同时也要把形式系统内的概念与元数学概念区分开来。问题是，我们所用的元数学可靠吗？我们的元数学是不是协调的(会不会推出矛盾)?如果元数学不协调，或者我们无从知道元数学是否协调，那么我们如何保证关于形式系统的结论的可靠性呢？这样我们就得研究元数学的可靠性。要研究元数学的可靠性，我们又需要“元元数学”。那么，元元数学的可靠性又如何得到保证呢？如此下去，我们就会陷入无穷回归的泥潭而不能自拔。为了解决这个问题，希尔伯特主张用有穷性方法来建立和研究形式系统。所谓有穷性，是指形式系统的建立必须是构造性的，即我们应该有一套机械的方法，利用它可以在有穷步骤内判定：
　　(1)一符号是否是形式系统的符号；
　　(2)一符号串是否是一个合法的公式；
　　(3)一个公式是否是公理；
　　(4)一公式是否由另一组公式通过某一规则直接导出。
　　我们称这样的形式系统为“递归系统”。如果希尔伯特计划得以实现，那么用冯 诺伊曼(J. Von Neumann)的话说，“在直觉主义的基础上把数学建立起来了”。历史上人们把希尔伯特的这种观点称之为“形式主义”。正当希尔伯特、冯 诺伊曼、伯奈斯(P. Bernays)、根岑(G. Gentzen)等致力于证明皮亚诺算术系统的完全性时，哥德尔却宣布：任何包含皮亚诺算术系统的递归系统如果是无矛盾的，则它是不完全的。哥德尔不完全性定理宣告了希尔伯特计划的破产。但是，希尔伯特的思想，连同他在1900年国际数学家大会上提出的23个问题中的第1个和第10个问题及他提出的希尔伯特判定问题，深刻地影响着数理逻辑的发展。到20世纪50年代，数理逻辑形成了四个主要分支。
　　(1)公理集合论：研究数学命题(如连续统假设、选择公理等)的可证性、相对协调性和相对独立性等。
　　(2)递归论：研究什么是算法、什么是计算、计算机的局限性及数学问题的可判定性等。递归论亦称“可计算性理论”。
　　(3)模型论：研究形式系统与数学结构之间的联系。
　　(4)证明论：研究数学证明的形式化及数学证明的结构。
　　数理逻辑的理论与方法广泛应用于数学、计算机科学等学科，并衍生出新的学科分支(如非标准分析、计算复杂性等)。然而，数理逻辑的研究早已超出了有穷性方法，例如，模型论中研究不可数模型，完全性定理、紧致性定理都是选择公理的弱形式。选择公理只是保证某种对象的抽象存在性。好在我们所使用的元数学到目前为止并没有发现存在什么矛盾。
　　1.2 数学定义、证明与定理
　　麻省理工学院西普塞(M. Sipser)说：定义是数学的精神，定理与证明是数学的灵魂，它们是任何数学分支的主体。当然，元数学是关于形式系统的定义、定理与证明。
　　数学定义就是利用初始对象和初始概念或已经定义的对象和概念来描述更复杂的对象或概念。比如，利用自然数，我们可以定义整数，进而定义有理数。在构建形式系统的过程中，我们先给定初始符号，进而定义合式公式、公理、推理规则等。精确性是数学定义的本质。换言之，数学定义