Decidability of admissibility in the modal system $\mathrm{Grz}$ and in intuitionistic logic

A criterion for admissibility of rules in the modal system $\mathrm{Grz}\rightleftharpoons\mathrm S4+\Box(\Box(p\supset\Box p)\supset p)\supset p$ is found. On the basis of it an algorithm is constructed that recognizes the admissibility of rules in $\mathrm{Grz}$. The decidability of admissibility in $\mathrm{Grz}$, proved in the paper, yields as a corollary a positive solution of the Kuznetsov–Friedman problem of algorithmic decidability 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 $\mathrm{Grz}$. The elementary theories of these free algebras are hereditarily undecidable.
Bibliography: 15 titles.