The decidability of admissibility problems for modal logics S4.2 and S4.2Grz and superintuitionistic logic KC (Q1317616)

In studies dealing with intuitionistic logic the following question arises: Is the admissibility problem for the logic Int decidable? (the Kuznetsov-Friedman problem). In a paper of \textit{V. V. Rybakov} [Algebra Logika 20, 440-464 (1981; Zbl 0489.03005)], it was noted that a rule \(\alpha/\beta\) is admissible in a superintuitionistic logic \(\lambda\supseteq\text{Int}\) if and only if the rule \(T(\alpha)/T(\beta)\) is admissible in \(\sigma(\lambda)\) -- the greatest modal companion of \(\lambda\) -- where \(T(\alpha)\) is the Gödel translation of the formula \(\alpha\). In another paper of Rybakov [ibid. 23, No. 5, 546-572 (1984; Zbl 0598.03013)], the Kuznetsov-Friedman problem was solved positively, using this fact and the decidability of the admissibility problem for modal logic S4, the modal companion of Int. Of special interest among superintuitionistic logics is the logic KC with the Weak Law of Excluded Middle. The greatest modal companion of KC is the logic S4.2Grz. In the present paper we obtain algorithms to verify whether the inference rules in the modal logics S4.2Grz are admissible. As a consequence, it is proved that the admissibility problem for KC is decidable.