* 第 5 章 形式系统与推理技术读者已经看到，逻辑代数的确揭示了人类思维的基本规律，例如AA （排中律） ， (A A)（矛盾律） ，A(A B) B （假言推理） ，A(BB) A（归谬推理） ，(AB) (A C)(BC) C（穷举推理）; 逻辑代数还提供了真值计算、代入、替换、对偶等演算手段，可用于对其它思维规律的探求。但是，这与数理逻辑所追求的形式化、公理化的目标相去甚远。20 世纪初，数理逻辑研究的一个重要目的在于建立一个严密的数学体系,来刻划人的思维的规律。这个体系以符号语言来表达；以若干表示最基本逻辑规律的公式（永真式）为基础，称为公理（axioms） ；以若干可对公式进行重写的规则（确保由永真式重写出永真式） ，作为系统内公式变换的依据，称为推理规则（rules of reference） 。系统内推演的全部依据是符号的形式,而不是别的任何东西，并且系统能导出且只能导出反映人们思维正确规律的永真式，进而成为人类进行逻辑推理的一个框架，它保证在前提正确的条件下，总得出正确的推理结果。这就是所谓数理逻辑的形式系统。2本章先推出一个经典简明的谓词演算形式系统 FC（first order predicate calculus formal system） ，借以介绍形式系统的相关概念。然后较完整地讨论一个相对实用的形式系统自然推理系统，也称自然演绎系统（natural deduction system）,简记为 ND。5.1 谓词演算形式系统 FC5.1.1 FC 的基本构成 谓词演算形式系统 FC 由两个部分组成：1. 谓词演算形式系统 FC 的语言部分。2. 谓词演算形式系统 FC 的理论部分。1. 谓词演算形式系统 FC 的语言部分。FC 的符号表：个体变元 x ,y ,z ,u ,v ,w , 个体常元 a ,b ,c ,d ,e, 个体间运算符号（函数符）f (n) , g (n) , h (n) ,其中 n 为任一正整数，表示函数的元数。谓词符号 P (n)，Q (n)，R (n)，S (n)，其中 n 为非负整数，表示谓词的元数。当 n = 0 时谓词符退化为一个命题常元。真值联结词 , 量词 (把 v 看作v的缩写)括号 ( ， )FC 的更高一级的语言成分有“个体项”和“公式” 。个体项(terms, 以下简称项)归纳定义如下：（1）个体变元和个体常元是项。（2）对任意正整数 n，如果 f (n)为一 n 元函数符，t 1 , ,tn 为项，那么 f (n)(t1,tn)也是项。（3）除有限次使用（1） ， （2）条款所确定的符号串外，没有别的东西是个体项。合式公式(well found formula ，以下简称公式)归纳定义如下：（1）对任意非负整数 n，如果 P (n)为一 n 元谓词符，t 1 , ,tn 为项，那么 P (0)（命题常元）和 P (n) (t1,tn)（n 0）是公式。（2）如果 A，B 为公式，v 为任一个体变元，那么(A) , (AB) , (vA) (或(vA(v)均为公式。（3）除有限次使用（1） （2）条款可确认为公式的符号串外，没有别的东西是公式。公式中括号的省略原则同前。约束变元、自由变元及辖域等概念照旧。今后，我们常用大写拉丁字母 A，B，C, ,表示任意公式，用 A(v)等表示公式 A 中含有自由变元 v；常用大写希腊字母 表示一个公式的集合， 可以是空集合；用 ；A 表示在公式集合 中添入公式 A，即 A。此外，我们还需要以下定义：定义 5.1 设 v1,vn 是公式 A 中的自由变元，那么公式v 1vnA(或v1vnA(v1,vn)称为 A 的全称封闭式（generalization clusure） 。A 不含自由变元时，A 的全称封闭式为其自身。2. 谓词演算形式系统 FC 的理论部分FC 的公理系统包括以下公理（A，B，C 为任意公式）：A1. A(BA)A2. (A(BC) (AB)(AC)A3. (A B)(BA)A4. xA(x)A(t/x)（x 为任一变元，t 为对 x 可代入的项） 。A5. x (A(x)B(x)(xA(x)x B(x)（x 为任一变元） 。A6. Ax A（A 中无自由变元 x） 。A7. 以上公式的全称封闭式都是 FC 的公理。推理规则: (分离规则) 。A1A3 为命题演算的重言式，也是谓词演算的永真式。 A4A7 是谓词演算的永真式。它们的永真性在第 3 章和第 4 章已经得到证实。5.1.2 系统内的推理：证明与演绎定义 5.2 公式序列 A1,A2,Am 称为 Am 的一个证明（proof） ，如果 Ai(1im)或者是公理，或者由 Aj1,Ajk(j1,jki)用推理规则推得。当这样的证明存在时，称 Am 为系统的定理（theorems） ，记为 *Am, ( 为所讨论的系统名),或简记为A m 。定义 5.3 设 为一公式集合。公式序列 A1,A2,Am 称为 Am 的以 为前提的演绎（diduction） ，如果 Ai(1im)或者是 中公式，或者是公理，或者由 Aj1,Ajk(j1,jki)用推理规则导出。当有这样的演绎时，A m 称为 的演绎结果，记为 *Am, ( 为所讨论的系统名)，或简记为 A m。称 和 的成员为 Am 的前提(hypothesis)。显然，证明是演绎在 为空集时的特例。注意，A m 与A m 是不同的，A m 与 Am 也是不同的，前者都是指形式系统内的推理关系（证明与演绎） ，而后者则是指公式的真值特性及真值间的逻辑关系。当然，它们之间应当是一致的，这正是我们建立形式系统所想要做到的。例 5.1、例 5.2 和例 5.3 是 FC 系统内证明和演绎的例子。例 5.1 证明： FCAA证. 其证明序列是（1）(A (AA) A) (A(AA) (AA) 公理 A2（2）A(AA) A) 公理 A1（3）(A (A A)(AA) 对(1) (2) 用分离规则（4）A(AA) 公理 A1（5）AA 对(3)(4) 用分离规则例 5.2 证明 FcB(BA)。证. 其证明序列是（1）B(AB) 公理 A1（2）(AB)(BA) 公理 A3（3）(A B)(BA)( B ( AB)(BA) 公理 A1（4）B（AB） (BA)） 对(2)(3)用分离规则（5） （B（AB） (BA) ）（B（AB） ）（B(BA)） ） 公理 A2（6） （B（AB） （B (BA) ） 对(4)(5) 用分离规则（7）B(BA) 对(1)(6)用分离规则例 5.3 在 FC 中对任意公式 A，B，C，证明：A，B(AC) FC BC证. 其演绎序列为（1）A 前提（2）B(AC) 前提（3）A(BA) 公理 A1（4）BA 对(1) (3) 用分离规则（5）(B(A C)(BA)(BC) 公理 A2（6）(BA) (BC) 对 (2) (5)用分离规则（7）BC 对 (4) (6)用分离规则5.1.3 FC 的重要性质现在我们对 FC 的重要性质作一些讨论。定理 5.1（合理性，sondness）若公式 A 是系统 FC 的定理，则 A 为永真式。若 A 是公式集 的演绎结果，那么 A 是 的逻辑结果。即若 FC A，则 A .若 FC A，则 A .本定理的证明是容易的，因为（1）易证公理 A1，A2，A3，A4，A5 ，A6 ，A7 是永真的。（2）易证分离规则是“保真”的，即当 A，A B 真时，B 亦真。从而由公理和分离规则逐步导出的公式是永真的；由 中公式、公理及分离规则导出的公式，在 中公式均真时也真。合理性定理的逆否命题可表述为若 A 不成立，则 FC A 不成立。因此，欲证 FC A 不成立，只要找出一个个体域、一种解释和一种指派，它满足 中的每一公式，但它却弄假 A。也就是说要证明一个由前提集合 推导出结论 A 的推理是无效的，只要举出一个反例（一个个体域、一种解释和一种指派） ，使得前提成立而结论不成立。作为合理性定理的自然推论我们有: 定理 5.2 FC 是一致的，即没有公式 A 使得 FC A 与 FCA 同时成立。证 若不然，据合理性定理有 A 和 A ，但这是不可能的。更深入的研究表明，FC 还是完备的。定理 5.3 （完备性，completeness ）若公式 A 永真，则 A 必为 FC 的定理；若公式 A是公式集 的逻辑结果，那么 A 必为 的演绎结果。即若 A，那么 FC A .若 A ，那么 FC A .本定理的证明是相当复杂的，略去。由于 ，是完备联结词组，并且由于全称量词 可以表示存在量词 ，因此所有永真式均可用只含联结词，和全称量词 的形式来表示，从这个意义上说，在FC 中可以推出前述系统中的一切永真式。这表明 FC 是一个成功和简化了的谓词演算形式系统。关于系统 FC 的性质还有一些重要定理，它们被称为导出规则，可以用来简化系统内的推理。定理 5.4（演绎定理）对任意公式集 和公式 A，B，AB 当且仅当；A B（当 = 时， AB 当且仅当 A B）证. 设 AB 的演绎序列是A1, A2, , An(=AB)那么可作出由 ；A 推出 B 的演绎：A1, A2, , An(=AB) ，A （前提） ，B（对 An,A 用分离规则）反之，设 ；A B，其演绎是A1, A2, , Am-1 , Am(= B)对演绎长度归纳证明 A B。 （1）若 B 为公理或 中成员，那么可作出由 导出 AB 的演绎如下：B(AB)（公理 A1） ，B , AB （对前两式用分离规则） （2）若 B