×

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)
PDF BibTeX XML Cite