[敬请读者注意] 本人保留本文的全部著作权利。如果哪位读者使用本文所描述内容，请务必如实引用并明白注明本文出处。如果本人发现任何人擅自使用本文任何部分内容而不明白注明出处，恕本人在网上广泛公布侵权者姓名。敬请各位读者注意，谢谢！

形式逻辑系统中逻辑归结关系的形式化定义方法

程京德

[注：本文最初于2023年2月1日发表在笔者微信公众号“数理逻辑与哲学逻辑”，今日才发现不知何故当时未在科学网博客同步发表，故今日在此补充发表。]

一个形式逻辑系统由其形式语言（formal language，由该逻辑系统的符号表中的符号构成的合乎文法的逻辑式的集合，用来表达逻辑命题）和逻辑归结关系（logical consequence relation，定义在该逻辑系统的语言上的、从语言的幂集到语言的二元关系，用来表达从前提得出有效结论）这两个部分构成。那么，形式逻辑系统的逻辑归结关系是怎样被严格地形式化地定义的呢？本文来简单（亦即，非形式化）地说明这个问题。

对一个形式逻辑系统可以从两个侧面去研究，语义的（或也称模型论的、逻辑的）(semantical/model-theoretical/logical) 侧面和语构的（或也称证明论的、演绎的）(syntactical/proof-theoretical/deductive) 侧面。一般来说，语义的侧面更为本质。

每个形式逻辑系统对其逻辑式都严格地定义了一个语义解释方法，使得每个逻辑式经过解释都获得一个真值(truth-value)。无论是两值逻辑还是多值逻辑，逻辑式的真值都是其本质的逻辑性质。

命题逻辑系统通常以从命题变量符号集合到真值集合的赋值映射来对每个命题变量赋予一个真值，对由逻辑联结词联结而成的复合逻辑式则按照逻辑联结词的逻辑语义来定义其真值。一阶（高阶的情形比较复杂，就不在此科普文章中介绍了）谓词逻辑系统通常把个体常数符号及个体变量符号映射到对象领域里的实体个体，把函数符号及谓词符号映射到对象领域上实体个体间的关系，而根据每个n元原子逻辑式是否的确为对象领域上的n元关系来确定其真值。对由逻辑联结词联结而成的复合逻辑式则按照逻辑联结词的逻辑语义来定义其真值，对于有（全称或存在）量词限定的复合逻辑式则按照量词的限定个体变量的（全部或某个）实例的存在来确定其真值。所以，如果每个逻辑联结词是一个外延真值函数，那么每个逻辑式本质上都是一个真值函数。

请读者注意一个重要事实。因为一个形式逻辑系统通常允许有无穷多（可数、可枚举）个变量符号，所以可以有无穷多个解释。

对于一个给定的形式逻辑系统，如果一个逻辑式在某个解释之下被解释为真，则称该解释为此逻辑式的一个模型(model)，如果一组逻辑式在某个解释之下每个逻辑式都被解释为真，则称该解释为此组逻辑式的一个模型。

基于上述概念，我们就可以从语义的（模型论的、逻辑的）侧面定义一个经典的形式逻辑系统的语义的（模型论的、逻辑的）逻辑归结关系为：对于作为前提给定的一组逻辑式P 和作为结论给定的一个逻辑式 c ，如果 P 的每个模型也都是 c 的模型，亦即，使得 P 的每个逻辑式解释为真的模型也将 c 解释为真，则称 P 与 c 之间存在着语义的（模型论的、逻辑的）逻辑归结关系。显然，当一组前提P 和一个结论 c 之间存在有语义的（模型论的、逻辑的）逻辑归结关系时，如果所有前提都为真的话，那么结论不可能为假。

请读者注意一个重要事实。尽管一个形式逻辑系统通常可以有无穷多个解释，但是这种“无穷性”并未在定义语义的（模型论的、逻辑的）逻辑归结关系时有所考虑。

科学研究中的基础主义方法论(the foundationalism methodology)，寻求在基础知识以及知识扩展过程的坚实基础上建立所有的人类知识；通常，基础知识应该是毋庸置疑的，知识扩展过程也应该是无可争议的。形式逻辑系统的形式化演绎机制，就是基础主义方法论在逻辑学中的体现。

从语构的（证明论的、演绎的）侧面去研究一个形式逻辑系统，就是要给出一个该逻辑系统的形式化演绎机制：设定该逻辑系统的出发点（逻辑公理，其正确性应该是由逻辑系统的语义/模型理论所保证的）以及推演规则（从特定的前提推演出特定的结论，其正确性也应该是由逻辑系统的语义/模型理论所保证的）。一个形式逻辑系统的形式化演绎机制必须保证：（1）健全性(soundness)；从该系统的逻辑公理出发推演出的所有结论都是该系统的逻辑定理（亦即，从语义/模型理论来说都是恒真的逻辑式）；（2）完全/充分性(complteness/adequacy)：该系统的所有逻辑定理都能够被从逻辑公理推演出来。通常，我们把一个形式逻辑系统的所有恒真逻辑式称为其逻辑定理，把该形式逻辑系统通过演绎机制推演出的所有逻辑式称为其形式定理。健全性和完全性合起来就是要求，一个形式逻辑系统的逻辑定理集合和形式定理集合是等同的。

从语构的（证明论的、演绎的）侧面定义一个形式逻辑系统的语构的（证明论的、演绎的）逻辑归结关系为：对于作为前提给定的一组逻辑式P 和作为结论给定的一个逻辑式 c ，如果从该逻辑系统的逻辑公理及P 出发，以有穷步骤（！）不断地应用推演规则，最终推演出 c ，则称 P 与 c 之间存在着语构的（证明论的、演绎的）逻辑归结关系。这个有穷步骤的推演过程被称为从前提P 到结论 c 的一个形式演绎(formal deduction)；仅从公理出发的形式演绎也称为形式定理的一个形式证明(formal proof)。

请读者注意一个重要事实。在定义语构的（证明论的、演绎的）逻辑归结关系时要求推演必须是在有穷步骤内完成的,这是形式逻辑系统的语构/证明理论中一个本质上非常重要的要求。在要求有穷性这一点上，语构/证明理论与语义/模型理论完全不同。

最后举两个实例。目前在硬件及软件形式验证中使用的模型检查技术之逻辑理论基础便是上面定义的语义的（模型论的、逻辑的）逻辑归结关系。哥德尔证明的关于数论形式理论的不完全性定理，其本质困难就在于上面定义的形式演绎中的有穷性要求。

微信公众号“数理逻辑与哲学逻辑”