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

Restrictive Function Analysis of a Propositional Calculus System on the Applicable Scope of the Law of Excluded Middle

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

It is a logic postulate that a proposition is equivalent to the affirmation of the same proposition, based on which affirmation signs can be omitted at will in any case; therefore, there is no need to introduce affirmation signs to the construction of apropositional calculus. However, it is notable that the above-mentioned postulate has never been proved beforehand. In view of the above, this paper constructs a sound and complete propositional calculus PC5 to which level 0 proposition variables and affirmation signs are introduced on condition that the applicable scope of the above-mentioned postulate is restricted. In PC5, the law of noncontradiction is valid for any pair of contrary propositions formed by the affirmation and negation of the same level n(n∈N, n≥0)proposition; besides, the law of excluded middle is valid for level n(n∈N, n≥1) proposition, but invalid for level 0 proposition.Therefore, on the basis of PC5, the law of indirect proof applies to the argument of the affirmation and negation of the level n(n∈N, n≥1) proposition, but not that of the level 0 proposition.