# zbMATH — the first resource for mathematics

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.

##### MSC:
 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: