蘊涵命题演算

初始符号中只有蕴涵(→)这一个命题联结词的命题演算。在蕴涵命题演算中不能定义其它的命题联结词。它的公式是命题演算中没有符号，∧，∨和出现的公式。下面陈述蕴涵命题演算的一个公理系统。用A，B，C等表示系统中的任意公式。

这个系统的公理(模式)是下面的3条：

1．A→(B→A)

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

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

　　　　　　　　　(皮尔士律)

推理规则只有一条：分离规则。从A和A→B可得B。

从上面的系统可以证明只含蕴涵词的重言式是系统中的定理。可以证明这个系统是协调的和完全的。例如，这个系统相对于A到A→a的变换(其中的a是不在A中出现的第一个命题变元)是协调的，即没有一个公式A，使得A和A→a都在系统中可证。相对于A到A→a的变换是完全的；对于系统中的每一公式B，或者B可证明，或者加上B作公理，系统就变成相对于A到A→a的变换是不协调的。

只由两个公理(模式)：A→(B→A)，(A→(B→C))→((A→B)→(A→C))和推理规则：分离规则，构成的系统，称为正蕴涵命题演算，记作P，系统P是不完全的，如重言式((A→B)→A)→A在P中是不能证明的，不是P的定理。