高级逻辑学笔记

这学期选了「高级逻辑学」这门课。课程所用的教材是王元元主编的计算机科学中的现代逻辑学。本文是课程的学习笔记，分为两部分：第一部分介绍书中对现代逻辑、形式化的定义，第二部分介绍一些有趣的形式系统。

现代逻辑

先引用一段书中对现代逻辑的定义：

书名中的“现代逻辑”一词指数理逻辑(mathematical logic)，或者符号逻辑(symbol logic)。对“现代逻辑”的理解通常有两种，一种是狭义的理解，它指“数理逻辑基础”，即所谓两个演算（命题演算与一阶谓词演算）以及其他一些相关的逻辑系统；另一种是广义的理解，它指数学的一个分支，包括数理逻辑基础及建于其上的“公理化集合论”(axiomatical set theory)、“证明论”(prof theory)、“递归论”(recursive theory，也称可计算理论)、“模型论”(model theory)。

这本书讨论的主要是狭义的定义，全书以一阶谓词演算为核心展开。

• 第一章介绍了形式化、形式系统概念
• 第二章介绍了命题演算系统
• 第三到十章从两方面对一阶谓词演算进行了扩张，分别是：语法扩张（引入谓词变元，函数变元，高阶量词，模态词）和语义扩张（多值逻辑）
• 第十一、十二章介绍了非单调逻辑和lambda演算

形式化和形式系统

这门课具体讨论的就是一个个形式系统。书中对形式化方法和形式系统的定义如下：

形式化实质是一种算法，即一个可机械地实现的过程，用于将概念、断言、事实、规则、推演乃至整个被描述系统表述得严密、精确而又无需任何专门的知识即可被毫无歧义地感知。

形式系统是理论或实际系统形式化的产物，在这种系统中所进行的推演均可被机械地测试，以确定它们是否是正确的。

其中，形式化这一概念的定义是任课老师极力推崇的，不仅讲了概念的内涵，也讲了概念的外延。但我看完还是没啥感觉，其实形式化是一个组合产物，它综合了符号化和公理化两个方面的抽象：

• 符号化：用一种“只作整体认读的记号(signs)”--- 符号(symbols)表示量，数及数量关系。例子：代数，UML
• 公理化：只从一些最简单的概念出发，承认一些再显然不过的事实，使用少量逻辑规则进行推演的思想。例子：欧氏几何，希尔伯特几何

关于公理化需要解释的是，上述例子中的两套理论代表了两种不同层次的公理化：

• 欧氏几何代表的是具体公理系统，虽然可以基于“两点确定一条直线”这样的公理(axioms)和三段论，假言推理这样的逻辑规则进行推理，但整个欧氏几何都没有对点，线，面这样的概念进行抽象。以至于欧氏几何的许多性质被证明在一些其他情况下也成立时，诞生了诸多非欧几何理论。
• 希尔伯特几何则是一种抽象公理系统，欧式几何可以看作其一种具体解释。为了取消欧氏几何中的直观性，希尔伯特有如下名言：

我们必须能够不用“点、线、面”，而说“桌子、椅子和啤酒杯”

综上，形式化可以理解为“符号化+抽象公理化”。

书中形式化地给形式系统下了一个定义：

一个形式系统FS由下面五个部分组成：

• 符号表Σ，称为FS的符号表(alphabet)，其元素称为符号；
• Σ上全体字的集合Σ*的一个子集Term，其元素称为FS的项(terms)，Term有子集Variable，其元素称为变元(variables)；
• Σ*的一个子集Formula，其元素称为FS的公式(formulas)，Formula有子集Atom,其元素称为原子公式(atomic formulas)。公式集与项集不相交，而项和公式常统称为表达式(expressions)；
• Formula上的一个子集Axiom,其元素称为FS的公理；
• Formula上的n元关系集合Rule，其元素称为FS的推理规则。

由此，FS可用五元组<Σ,Term,Formula,Axiom,Rule>表示。