Properties of superintuitionistic propositional calculi (Q1814378)

The aim of the paper is to study derivability of formulas which have no occurrences of some logical connectives. Before, the author has shown that the separation property can be reduced to two properties, one of which is the so-called \({\mathfrak P}_{\supset\lor\&}\)-property. This means that the set of positive formulas provable in the given calculus coincides with the set of positive formulas provable in the calculus which is obtained from the original one by removing supplementary axioms which have an occurrence of negation. In this paper, the author studies the above-mentioned property and the separation property for superintuitionistic logics with implicative axioms and some supplementary axioms. An algorithm is found which recognizes the \({\mathfrak P}_{\supset\lor\&}\)-property and the separation property among the superintuitionistic logics of the considered class.