Logical equations and admissible rules of inference with parameters in modal provability logics (Q805609)

The aim of this paper is to study admissible inference rules for the modal provability logics GL and S. It is proved that none of these logics has a basis for admissible rules in a finite number of variables, in particular, they do not have finite bases. It is proved that GL and S are decidable by admissibility, some algorithms are found which recognize admissibility of usual inference rules and inference rules in generalized form - inference rules with parameters (or metavariables). By using recognizability of admissibility of inference rules with parameters, we can recognize solvability of logical equations in GL and S and construct some of their solutions. Thus, the analogues of H. Friedman's problem for GL and S are affirmatively solved, the analogues of A. Kuznetsov's problem of finiteness of a basis for admissible rules for GL and S have negative solutions, and the problems of solvability of logical equations in GL and S have positive solutions.