| 系统R system R 相干命题逻辑中的一个系统。由安德森和贝尔纳普于20世纪60年代建立。它的初始符号中有逻辑联结词→(相干蕴涵)、(否定)和∧(合取)，整个系统可用如下公理和推理规则来表述(A、B、C是R中任意的公式)： 公理1：A→A， 公理2：(A→B)→((B→C)→(A→C))， 公理3：(A→(A→B))→(A→B)， 公理4：A→((A→B)→B)， 公理5：(A∧B)→A， 公理6：(A∧B)→B， 公理7：((A→B)∧(A→C))→(A→B∧C)， 公理8：A→(A∨B)， 公理9：B→(A∨B)， 公理10：((A→C)∧(B→C))→((A∨B)→C)， 公理11：(A∧(B∨C))→((A∧B)∨C)， 公理12：(A→A)→A， 公理13：(A→B)→(B→A)， 公理14：A→A。 分离规则：若A和A→B都是定理，则可推知B是定理。 合取规则：若A和B都是定理，则可推知A∧B是定理。 在R中∨(析取)通过和∧来定义：(A∨B)=df(A∧B)。R是经典命题逻辑的一个真子系统，一切蕴涵怪论在R中都可以避免，即不会成为R中的定理。系统R有着多种形式的语义，其中较重要的有卢特雷(R. Routley)和梅尔(R. Meyer)1972年提出的克里普克语义。在语义模型的基础上可证明R具有完全性和可靠性。80年代，尤尔奎哈特(A. Urqiuhart)进一步证明系统R是不可判定的。 |