在经典命题演算中，不矛盾律和排中律都普遍有效。直觉主义断然否定排中律的普遍有效性，在直觉主义命题演算中，不矛盾律普遍有效，排中律无效。直觉主义的创始人布劳维(L.E.J.Brouwer)认为：排中律是从有限事物中概括出来的，任何一个涉及有限事物全体的命题，总是可以通过对这些事物逐一地加以验证，来判明该命题的真伪，这时排中律是有效的。但是如果忘记了排中律的有限来源，把排中律视为先于和高于数学的某种普遍适用的法则，并将它运用于无限的场合，就会犯错误。这是因为对于无限的事物，往往不可能(哪怕是原则上)对它们一一加以鉴别。[1] 49 然而，经典命题演算认排中律为普遍有效式，这固然与直观相违;直觉主义命题演算认排中律为无效式，亦与直观不尽相符。从直观上看，正如布劳维所认为的那样，排中律对且只对有限事物有效;但无论是经典命题演算，还是直觉主义命题演算，都没有框定排中律的适用范围。鉴于此，本文拟对经典命题演算做适当改动，构造一个限制排中律适用范围的命题演算系统PC5。
命题演算系统PC5 及其可靠性、完全性
(一)PC5的语法和语义
初始符号：甲、p1，p2，p3，，pm，，m 为自然数;乙、┌ ，┐，丙、(，)。
在陈述形成规则以前，我们先引进一些语法语言的符号并作如下说明：
(1)Q、R、S 代表任一甲类符号。
(2)X、Y、Z 代表任一符号序列。
(3)A、B、C、D、E 代表任一合式公式。
(4)语法符号┠写在任一公式之前，它表示紧接在后面的公式是本系统所要肯定的。
形成规则：
(1)若X 是甲类符号，则┌X、┐X 是合式公式。
(2)若X 是合式公式，则┌X、┐X 是合式公式。
(3)若X 和Y 都是合式公式，则(XY)是合式公式。
(4)只有适合以上三条的符号序列是合式公式。
定义：
(甲)(AB)定义为(┐AB)。
(乙)(AB)定义为┐(┐A┐B)。
(丙)(AB)定义为((AB)(BA))。
括号省略规则：
(甲)最外面的一对括号可以省略。
(乙)真值联结词的结合力依下列次序而递增：，，，┌，┐。
公理：
公理1：┠AA;
公理2：┠AB;
公理3：┠AB
公理4：┠(BC)BC);
公理5：┠┌A
公理6：┠ ┐(┌Q┐Q)。
变形规则：
(1)分离规则，从┠A 和┠ ┐AB 可得┠B。
(2)定义置换规则，定义的左右两方可相互替换。设原公式为A，替换后所得公式为B，则从┠A 可
得┠B。
公式的级的递归定义：
(1)若X 是甲类符号，则┌ X 和┐X 均为原子公式，原子公式是1 级公式。
(2)若X 是m 级公式，则┌ X 和┐X 均为m+1 级公式。
(3)若X 是m 级公式，Y 是n 级公式，且mn，则XY、YX、XY、YX、XY、YX、XY、
YX 均为m 级公式。
对引入0 级命题变项和肯定词符号的一点说明
如前文所述，0 级命题变项代表任意的0 级命题。0 级命题就是不包含肯定词或否定词的命题。这里有一点需要说明，逻辑学界有一种普遍流行的观点，这种观点认为任何命题都肯定了自身。按照这种观点，人们必须承认：第一，任何命题都隐含着肯定词;第二，一个命题与肯定该命题而形成的命题是等值的。这样一来，也就不存在0 级命题了。
笔者认为，上述普遍流行的观点颇值得商榷。首先，没有任何理由可以证明任何命题都肯定了自身。
其次，有些命题很难说肯定了自身。例如，命题甲圆周率 的小数表达式3.1415926中有七个连续出现的5就很难说肯定了自身。 是一个无理数，即无限的不循环的小数。到目前为止，我们还没有发现(或证明) 的小数展开式中有七个连续出现的5，因而不能肯定命题甲;我们也无法论证 一定没有这样一个特性，因而也不能否定命题甲[1] 49~50。如果命题甲肯定了自身，那么只要提出命题甲，就提出了对命题甲的肯定。这与命题甲虽已提出来但到目前为止还未被肯定这一事实显然不符。再次，一个命题与肯定该命题而形成的命题是等值的只是逻辑学的一个公设，基于这一公设，肯定词在任何情况下都可以随意消除，人们在构造命题演算系统时根本无需引入肯定词，这就造成了在现代逻辑中对肯定词和否定词的研究极为不平衡的奇特现象：人们建立了多种多样的命题演算系统来刻画否定词的逻辑意义，区分了不同种类的否定(如经典否定、直觉主义否定、弗协调否定等)[3] 476~477;但人们对肯定词的逻辑意义却极少关注。然而，值得提出的是，上述公设从未得到过系统外的预先证明。鉴于此，本文所建构的形式系统在限制上述公设适用范围的基础上引入了0 级命题变项和肯定词符号。