# zbMATH — the first resource for mathematics

Derivability of admissible rules. (Russian) Zbl 0358.02031
We consider intuitionistic propositional calculus IPC in the language $$\&,\lor,\supset,\lnot, \mathrm{t(ruth)}$$ and its fragments defined by a subset of this set. It is proved that any rule defined in a fragment which does not contain one of $$\lor$$, $$\supset$$ and admissible in IPC is also derivable in IPC. Only rules closed under substitution are considered. Example $$(a \supset p)\supset (a\lor b)\vdash ((a \supset p) \supset a) \lor ((a\supset p) \supset b)$$ shows that further restriction of fragments is impossible.

##### MSC:
 03B20 Subsystems of classical logic (including intuitionistic logic)