Language, Proof and Logic（语言、证明与逻辑）

引用

Barker-Plummer, D., Barwise, J., & Etchemendy, J. (2011). Language, Proof and Logic (2nd ed.). CSLI Publications.

章节概要

Language, Proof and Logic（LPL）是一本与软件配套的教材。Tarski's World 讲授一阶语言及其语义，Fitch 是构造和检查证明的自然演绎环境，Boole 处理真值表，Submit 则把练习文件提交给自动评分的在线服务 Grade Grinder。导论之后是分为三部分的19章，许多小节都明确标注为“（optional）”。书末有形式证明规则汇总、术语表，以及文件、练习和综合索引。据出版社介绍，第二版对原版作了大幅扩充和修订：扩充了数学归纳法的内容（并为皮亚诺归纳和累积值归纳增加了软件支持），改进了朴素集合论和策梅洛–弗兰克尔集合论的讲解。

导论

包括逻辑在理性探究中的特殊作用、为什么要学习一种人工语言、后承与证明等小节；随后是目录中标为“必读”的家庭作业说明，以及给教师的说明。

第一部分：命题逻辑

第1–2章：原子句、原子句的逻辑

第1章介绍个体常项、谓词符号和原子句，另有关于函数符号、集合论和算术的一阶语言以及其他记法的选读小节。第2章定义有效论证和可靠论证，介绍证明方法和形式证明，说明如何在 Fitch 中构造证明，以及如何证明不构成后承。

第3–4章：布尔联结词、布尔联结词的逻辑

第3章讲否定、合取和析取，一个用于判定语句真假的游戏，歧义与括号，同义的不同说法，以及翻译。第4章区分重言式与逻辑真理、重言等值与逻辑等值、重言后承与逻辑后承，在 Fitch 中处理重言后承，并有关于把否定内移以及合取范式和析取范式的选读小节。

第5–6章：布尔逻辑的证明方法、形式证明与布尔逻辑

先讲非形式证明：有效的推理步骤、分情况证明和反证法。第6章再给出合取、析取和否定的形式引入规则与消去规则、子证明的正确用法，以及寻找证明的策略和技巧。

第7–8章：条件句、条件句的逻辑

实质条件句和双条件句、会话含义，以及选读的真值函项完全性。第8章增加了条件句的非形式与形式证明方法、关于可靠性和完全性的选读小节，以及第一部分的复习练习。

第二部分：量词

第9–11章：量化导论、量词的逻辑、多重量词

第9章介绍变元、量词符号、合式公式与语句、量词的语义和四种亚里士多德形式，并练习翻译复杂名词短语。第10章讨论一阶有效性和后承、包括德摩根律在内的量词等值式、关于公理化方法的选读小节，以及引理。第11章处理混合量词、逐步翻译法、英语的改写、歧义与语境敏感性，以及前束范式。

第12–13章：量词的证明方法、形式证明与量词

先讲非形式方法：有效的量词步骤、存在例示、一般条件证明以及含混合量词的证明。随后是 Fitch 中全称和存在量词的形式规则、策略与技巧，以及关于可靠性和完全性的选读小节。

第14章：再论量化

数量量化及数量命题的证明，“the”“both”“neither”，在一阶逻辑中加入其他限定词，广义量词的逻辑，以及一阶逻辑表达力的局限。

第三部分：应用与元理论

第15–16章：一阶集合论、数学归纳法

第15章展开朴素集合论：空集、子集、交与并、有序对、关系和函数；选读小节包括幂集、罗素悖论和策梅洛–弗兰克尔集合论。第16章介绍归纳定义与归纳证明、自然数上的归纳以及 Fitch 中的归纳，并有关于自然数公理化和强归纳的选读小节。

第17–19章：命题逻辑高级专题、一阶逻辑高级专题、完全性与不完全性

第17章证明命题逻辑的完全性，另有关于霍恩语句和归结法的选读小节。第18章定义一阶结构，重新讨论真与满足，证明一阶逻辑的可靠性，并有关于斯科伦化、合一和归结法的选读小节。第19章用亨金构造证明完全性定理，接着讨论勒文海姆–斯科伦定理和紧致性定理，最后以哥德尔不完全性定理收尾。

核心概念

第一部分：命题逻辑

• 有效性与可靠性：当结论从前提中得出时，论证是有效的；如果前提也为真，论证就是可靠的。
• 重言后承与逻辑后承：仅凭真值函项联结词成立的后承，与更一般地凭意义成立的后承之间的区别。
• 菲奇式自然演绎：由引入规则和消去规则构成、用子证明处理临时假设的形式证明。
• 真值函项完全性：一组联结词能否表达所有真值函项。

第二部分：量词

• 一阶有效性与后承：超出重言后承、仅凭量词和同一性的意义而成立的后承。
• 翻译：把英语句子（包括复杂名词短语和混合量词）逐步改写为一阶逻辑。
• 存在例示与一般条件证明：形式量词规则所对应的非形式推理模式。
• 广义量词：诸如“most”“both”之类的限定词，以及一阶逻辑所能表达内容的界限。

第三部分：应用与元理论

• 数学归纳法：对归纳定义的集合（包括自然数）进行的证明。
• 可靠性与完全性：证明系统只证明、而且能证明全部有效后承。
• 紧致性与勒文海姆–斯科伦定理：由完全性推出的、关于无穷语句集和模型大小的结论。
• 哥德尔不完全性定理：在一个一致的形式系统中无法证明全部算术真理的限制。

评析

优点

• 软件融入学习过程。 据出版社介绍，配套程序让学生构造世界、真值表和证明，Grade Grinder 能几乎即时地为数百道上机练习评分。学生能迅速得到反馈，教师也免去了机械的批改工作。
• 先非形式，后形式。 从目录看，每个逻辑主题都先有一章讲非形式证明方法，再有一章讲形式证明（第5–6章和第12–13章）。学生既学会在形式系统中推理，也学会用普通的数学语言推理。
• 选读内容标注清楚。 选读小节在目录中有明确标注，课程可以沿着第一、二部分的核心路线推进，再选择补充内容。
• 从入门到元理论。 出版社说本书不要求任何逻辑基础，适用于入门课程和第二门课程；Openproof 网站则表示，由于第三部分讲到完全性、紧致性和哥德尔定理，本书从本科第一门逻辑课到研究生第一门逻辑课都适用。
• 重视翻译与自然语言。 书中有整节讨论翻译、英语改写、会话含义和广义量词，体现出作者不仅关注证明，也关注语言。

局限

• 与软件包绑定。 要充分利用本书，需要随软件包出售的注册码。出版社指出，注册码一经激活便不可转让，因此二手书可能无法使用网络应用和评分服务。
• 篇幅长、内容密。 全书约600页，第三部分远远超出第一门课程所需。
• 只讲一阶逻辑。 目录中没有模态逻辑、多值逻辑或其他非经典逻辑；第14章虽讨论了一阶逻辑表达力的局限，但哲学专业学生学习模态逻辑还需要另一本教材。

在课程中的定位

在这门逻辑课程中，LPL 是两本采用菲奇式自然演绎的形式逻辑入门书之一。forall x: Calgary 是一本免费、开放许可的教材，用类似的证明系统讲授真值函项逻辑和一阶逻辑；它更短，也不需要软件，适合想先轻松过一遍的学生。科皮的 Introduction to Logic 在一本书中涵盖非形式推理、三段论逻辑、符号逻辑和归纳，因此比 LPL 更适合批判性思维课程。

学完 LPL 之后，西奥多·赛德的 Logic for Philosophy 是第二门课程的教材，它更严格地处理命题逻辑和谓词逻辑，并补上 LPL 所缺的模态逻辑。布洛斯、伯吉斯和杰弗里的 Computability and Logic 展开可计算性理论和各项限制性结果的完整证明；据出版社介绍，LPL 的第19章以哥德尔定理的概要收尾，可以作为通向该书的桥梁。

如何使用本书

本书不要求任何逻辑基础。在开始做练习之前，先读导论中关于家庭作业的说明，因为软件和 Grade Grinder 本身就是练习的做法和提交方式的一部分。第一门课程通常讲授第一、二部分（第1–14章）；作者基于这套教材制作的在线课程正好用14章讲授这两部分，并建议大约每周学习一章。第一遍学习时可以跳过选读小节，除非老师另有安排。

先学非形式方法的章节，再学对应的形式章节；在进入 Fitch 证明之前，用 Tarski's World 把翻译放到具体的世界中检验。第三部分适合第二门课程，或准备进入数学、计算机科学方向的学生：讲集合论和归纳法的第15–16章是学习任何以证明为主的数学的良好准备，第17–19章则通向元理论。做练习时，可把书末的形式证明规则汇总和术语表当作参考资料。