极小命题演算

一种非经典命题演算，记作P。P的初始符号包括5个基本联结词：否定，合取，析取，蕴涵和等值，除等值以外的各联结词不能互相定义。P的公理(模式)有下面的13条。

Ⅰ．蕴涵公理

　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→B∨A

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

Ⅳ．等值公理

　10．(AB)→(A→B)

　11．(AB)→(B→A)

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

V．否定公理

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

P的推理规则是分离规则。

极小演算的特点是，不仅同直觉主义命题演算一样，不承认经典命题演算的某些逻辑规律，如排中律(A∨A)，双重否定律(A→A)等，而且也不承认直觉主义命题演算所承认的A→(A→B)(否定前件律)，从而也不承认直觉主义命题演算中证明时需要用到否定前件律的那些逻辑规律。由此产生的结果是，直觉主义者不承认好些经典逻辑规律，如排中律，但不否认它们，即认为它们不假，而在极小演算中，则连它们不假也不承认。把P的公理(13)换为

　14．(A→A)→A(特殊归谬律)

　15．A→(A→B)(否定前件律)

所得的系统就是直觉主义命题演算P。极小命题演算就是因拒绝15而提出的。