Admissibility of rules of inference, and logical equations, in modal logics axiomatizing provability

This paper examines the modal logics of Gödel-Löb (GL) and Solovay (S) – the smallest and the largest modal representations of arithmetic theories. The problem of recognizing the admissibility of inference rules with parameters (and, in particular, without parameters) in GL and S is shown to be decidable; that is, a positive solution is obtained to analogues of a problem of Friedman. The analogue of a problem of Kuznetsov on finite bases of admissible rules for S and GL is solved in the negative sense. Algorithms are found for recognizing the solvability in GL and S of logical equations and for constructing solutions for them.