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

相关逻辑 (5) - 形式化公理系统

程京德 

自20世纪50年代起至今，相关逻辑(Relevant/Relevance Logic)已经发展成为哲学逻辑中一个非常重要的分支。笔者主张，相关逻辑必将成为支撑智能科学及人工智能技术的统一理论之逻辑基础。本系列文章将全面介绍相关逻辑及其应用。

    如同笔者在前面文章中阐述过的，“从解决条件句/蕴涵关系表达以及蕴涵悖论的观点来看，使得相关逻辑区别于其它形形色色的形式逻辑系统的本质特征为：相关逻辑是唯一的一族形式逻辑系统，其创建动机在于试图要解决条件句/蕴涵关系之前件与后件之间的相关性问题，其每个成员都从逻辑定理中完全排除了（经典数理逻辑的）实质蕴涵悖论和（刘易斯模态逻辑的）严格蕴涵悖论。”[5] 而创建相关逻辑的开创性工作就是阿克曼“提出了用一个初始内涵逻辑联结词“Strengen Implikation (Rigorous Implication，严密蕴涵)”来表达和刻画条件句概念/蕴涵关系的划时代重要思想，并提出了一个公理化逻辑系统（第一个完整的相关逻辑系统）π’来刻画“严密蕴涵”（以及其它逻辑联结词）的性质/行为，π’从其逻辑定理中成功地完全排除了（经典数理逻辑的）实质蕴涵悖论和（刘易斯模态逻辑的）严格蕴涵悖论。”[4]

刻画初始内涵联结词“必然归约/相关蕴涵”的公理模式

    刻画各个相关逻辑系统中表达条件句概念/蕴涵关系的初始逻辑联结词（本文用符号“=>”来表达）应该满足的性质的各个公理模式如下：

刻画外延联结词“联言/合取”及“选言/析取”的公理模式

    刻画各个相关逻辑系统中逻辑联结词“联言/合取”及“选言/析取”（两者任取其一作为初始联结词即可）应该满足的性质的各个公理模式如下：

刻画初始外延联结词“否定”的公理模式 

    刻画各个相关逻辑系统中初始逻辑联结词“否定”应该满足的性质的各个公理模式如下：

刻画“必然”模态算子的公理模式 

    如同笔者在前面文章中已经说明过的，“与刘易斯在经典数理逻辑（外延真值函数逻辑）的形式语言中引入模态算子来定义“严格蕴涵”的方法不同，阿克曼没有在形式语言中引入模态算子，而是直接引入一个内涵逻辑联结词作为初始联结词（这里我们用“=>”表示）来表达条件句/蕴涵关系。为了让 E 的模态性质更明晰地显示出来，安德森和贝尔纳普在 E 中是用条件句/蕴涵式来定义必然性模态算子的：LA =_df(A => A) => A (where L is the necessity operator)。” [5] 

    刻画相关逻辑系统中“必然”模态算子应该满足的性质的各个公理模式如下：

刻画个体量化的公理模式 

    刻画各个相关逻辑系统中个体量词应该满足的性质的各个公理模式如下：

推理规则 

    各个相关逻辑系统中的推理规则如下：

各个相关逻辑形式化公理系统 

参考文献 

[1] A. R. Anderson and N. D. Belnap Jr., “Entailment: The Logic of Relevance and Necessity,” Vol. I, Princeton University Press, Princeton, 1975. 

[2] A. R. Anderson， N. D. Belnap Jr., and J. M. Dunn, “Entailment: The Logic of Relevance and Necessity,” Vol. II, Princeton University Press, Princeton, 1992.

[3] 程京德，“相关逻辑(1) – 背景与前史”，微信公众号“数理逻辑与哲学逻辑”，科学网博客，2024年5月28日。

[4] 程京德，“相关逻辑(2) – 创建”，微信公众号“数理逻辑与哲学逻辑”，科学网博客，2024年6月9日。

[5] 程京德，“相关逻辑(3) – 特征”，微信公众号“数理逻辑与哲学逻辑”，科学网博客，2024年6月18日。

[6] 程京德，“相关逻辑(4) – 形式语言”，微信公众号“数理逻辑与哲学逻辑”，科学网博客，2024年6月25日。

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