一个限制排中律适用范围的命题演算系统

“一个命题与肯定该命题而形成的命题是等值的”只是逻辑学的一个公设，基于这一公设，肯定词在任何情况下都可以随意消除，人们在构造命题演算系统时根本无需引入肯定词。然而，值得提出的是，上述公设从未得到过系统外的预先证明。命题演算系统PC5在限制上述公设适用范围的基础上引入了0级命题变项和肯定词符号。PC5具有可靠性和完全性。在PC5中，对于任意的肯定和否定同一个n（n∈N且n≥0）级命题而形成的两个相反命题而言，不矛盾律都成立；对于任意的肯定和否定同一个n（n∈N且n≥1）级命题而形成的两个相反命题而言，排中律成立，但对于任意的肯定和否定同一个0级命题而形成的两个相反命题而言，排中律不成立。以PC5为逻辑基础，反证法适用于论证n（n∈N且n≥1）级命题的肯定或否定命题，但不适用于论证0级命题的肯定或否定命题。