Complexity of admissible rules (Q868660)

An inference rule is admissible in a logic \(L\) if the set of theorems of \(L\) is closed under the rule. V. Rybakov proved decidability of the problem od admissibility for many modal and superintuitionistic logics. The author provides complexity estimates for this problem which are optimal or close to optimal. Admissibility in ``typical'' extensions of K4 and superintuitionistic logics is co-NEXP-complete while derivability is P-SPACE-complete or even NP-complete. A co-NEXP decision procedure is given for admissibility in a class of logics including K4, GL, S4, S4Grz and Int. Admissibility is proved to be co-NEXP-hard in all superintuitionistic logics \(L\) such that every depth-3 tree is an \(L\)-frame and in similar normal modal extensions of K4.