初基演算

中国逻辑学家沈有鼎建立的一种命题演算，它可以作为极小命题演算和刘易斯模态命题演算S4的共同基础。初基演算以∧，∨，，为初始联结词，并使用下列公理模式和推理规则：

R1． 从A和AB可推出B，

R2． 从A和B可推出A∧B。

将公理模式A换成公理模式B(AB)，就得到极小命题演算；另一方面，如果在初基演算中附加下列两个公理模式：

那么就得到刘易斯模态命题演算S4。同时进行这两件事情，就可得到通常的二值命题演算。初基演算有两个重要性质：①从A可推出B当且仅当AB是该演算的定理；更进一步有，从A和B可推出C当且仅当A∧BC是该演算的定理；类似地，对3个和3个以上的前提而言，从A、…A(n≥3)可推出C当且仅当A∧…∧C是该演算的定理。②在AB和BA的假定之下，A与B可以互相代替。这意思是说：令F(X)同于G(X，C，D，…)，而G是纯由∧、∨、、4个联结词一层一层构成的，那末从F(A)、AB和BA可推出F(B)。从初基演算中去掉3个公理模式A24、A33和A34所得到的命题演算仍具有上述两个性质。