正命题演算

初始符号中没有命题联结词否定()和没有关于命题联结词否定的公理的部分命题演算，记作P。P的初始联结词是蕴涵，合取，析取和等值。它的推理规则是分离规则。P的公理(模式)有以下的12条：

Ⅰ．蕴涵公理

1．A→(B→A)

2．(A→(A→B))→(A→B)

3．(A→B)→((B→C)→(A→C))

Ⅱ．合取公理

4．A∧B→A

5．A∧B→B

6．(A→B)→((A→C)→(A→B∧C))

Ⅲ．析取公理

7．A→A∨B

8．B→A∨B

9．(A→C)→((B→C)→(A∨B→C))

Ⅳ．等值公理

10．(AB)→(A→B)

11．(AB)→(B→A)

12．(A→B)→((B→A)→(AB))

建立系统P的目的是具体表现命题演算中在某种意义上独立于联结词否定的部分。加上否定作初始联结词并增加关于否定的公理，系统P就可以扩展为全的命题演算(full proposinal propositional calculus)。如加上关于否定的公理(模式)：

13．(A→B)→(B→A)

14．A→A

15．A→A

所得的系统称为希尔伯特－贝奈斯系统，是D．希尔伯特和P．贝奈斯在《数学基础》一书中给出的。这个系统的特点是把5个基本联结词的一些重要特征用公理表示出来。每一组公理刻划一个联结词的特征。

正命题演算和希尔伯特－贝奈斯系统都具有各组公理自足的性质，即：在证明系统中的定理时，除了Ⅰ组公理外，只需用到所要证明的公式中出现的联结词有关的公理。例如，证明A∧B→B∧A是定理，除蕴涵公理外，只用到合取的公理。