# zbMATH — the first resource for mathematics

The separation property for provability intuitionistic calculus. (Russian) Zbl 0649.03008
The provability intuitionistic calculus, denoted by $$I^{\Delta}$$, is an extension of the intuitionistic propositional calculus by adding the following axioms for the new modal operator $$\Delta$$: 1. $$(p\supset \Delta p)$$, 2. (($$\Delta$$ $$p\supset p)\supset p)$$, 3. ($$\Delta$$ $$p\supset (((q\supset p)\supset q)\supset q))$$. In the paper it is proved that the calculus $$I^{\Delta}$$ has the separation property, i.e., for any formula A deducible in $$I^{\Delta}$$ there is a deduction of A that uses no axiom which contains logical connectives different from $$\supset$$ and not occurring in A.
Reviewer: Phan Dinh Diêu
##### MSC:
 03B20 Subsystems of classical logic (including intuitionistic logic)
Full Text: