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
03B20 Subsystems of classical logic (including intuitionistic logic)
Full Text: EuDML