一类命题逻辑的一般弱框架择类语义，本文主要内容关键词为：语义论文,命题论文,框架论文,逻辑论文,一般弱论文，此文献不代表本站观点，内容供学术参考，文章仅供参考阅读下载。
中图分类号：B81 文献标识码：A 文章编号：1674-3202(2011)-02-0020-15
一、一类B、C、K、W正命题逻辑
1.公理：
·公理A1：A→A
·公理A2：A∧B→A
·公理A3：A∧B→B
·公理A4：A→A∨B
·公理A5：B→A∨B
·公理A6：A∧(B∨C)→(A∧B)∨(A∧C)
2.变形规则：
·规则R1(分离规则)：由A和A→B可推出B。
·规则R2(附加规则)：由A和B可推出A∧B。
·规则R3(传递规则)：由A→B和B→C可推出A→C。
·规则R4(后件合取规则)：由A→B和A→C可推出A→B∧C。
·规则R5(前件析取规则)：由A→C和B→C可推出A∨B→C。
极小正命题逻辑
是研究一般弱框架择类语义的基础。
在结构推理的研究中，重要的内涵结构规则有：结合规则(简记为“B”)、强交换规则(简记为“C”)、弱化规则(简记为“K”)和强收缩规则(简记为“W”)([7]，p.26)。这些规则分别对应于如下的蕴涵公理([7]，p.86)：
·公理B(结合公理)：(A→B)→((C→A)→(C→B))；
·公理C(强交换公理)：(A→(B→C))→(B→(A→C))；
·公理K(弱化公理)：A→(B→A)；
·公理W(强收缩公理)：(A→(A→B))→(A→B)
(4)条件⑤的直观意义是：∏中的两个命题X、Y在每一个逻辑世界中都满足蕴涵关系的充分必要条件是：若X为真，则Y为真。这是蕴涵关系具有保真性的体现。
特性P1-P7分别对应于公理B、C、K、W、A7、A8、A9。观测特性与公理的对应关系，不难发现，只须对公理B、C、K、W、A7、A8、A9作如下的改写，即为相对应的特性P1-P7：
(1)将公式A、B、C分别改写为X、Y、Z；
(2)将逻辑联结词∧、∨分别改写为∩、∪；
(3)若逻辑联结词→不是主算子，则改写为
；
(4)若逻辑联结词→是主算子，则改写为
。
三、可靠性和完全性
限于篇幅，本文只给出了诸系统的可靠性和完全性证明的概要。某些证明细节，可参照文献[10]§2.3和§3.2，不难补齐。
注释：
②满足B、C是线性逻辑([2，4])的特征。
③满足B、C、K是BCK逻辑([4,6])的特征。
⑤满足B、C、K、W是直觉主义命题逻辑的特征。
⑥公理A7、A8来自相干基本(basic)系统B([3])。
⑦公理A9来自直觉主义命题逻辑([9])。
⑧这一定义及其后的一系列定义，在表述方式上借鉴了相干邻域语义的文献[5]和[8]。
⑨采用规则R6的否定称为“简单否定(simple negation)”([7]，p.77)。
⑩采用公理A10的否定称为“内涵否定(intentional negation)”([7]，p.77)。
(12)采用公理A10、A12且拒斥公理A11的否定是“直觉主义否定(intuitionistic negation)”。IP与[9]的同名系统等价。