Decidability of admissibility in the modal system Grz and in intuitionistic logic. (English. Russian original) Zbl 0624.03009

Math. USSR, Izv. 28, 589-608 (1987); translation from Izv. Akad. Nauk SSSR, Ser. Mat. 50, No. 3, 598-616 (1986).
A criterion for admissibility of rules in the modal system Grz\(\rightleftharpoons S4+\square (\square (p\supset \square p)\supset p)\supset p\) is found. On the basis of it an algorithm is constructed that recognizes the admissibility of rules in Grz. The decidability of admissibility in Grz, proved in the paper, yields as a corollay a positive solution of the Kuznetsov-Friedman problem of algorithmic decidabiity of the admissibility problem in intuitionistic propositional logic. Algebraic analogues of the results obtained here are the decidability of the universal theories of a free pseudo-Boolean algebra and a free topo-Boolean algebra in the variety of algebras corresponding to the system Grz. The elementary theories of these free algebras are hereditarily undecidable.


03B25 Decidability of theories and sets of sentences
03B45 Modal logic (including the logic of norms)
03B20 Subsystems of classical logic (including intuitionistic logic)
Full Text: DOI