Proof theory for admissible rules

Abstract

The admissible rules of a logic are the rules under which the set of theorems of the logic is closed. In this paper a Gentzen-style framework is introduced for defining analytic proof systems that derive the admissible rules of various non-classical logics. Just as Gentzen systems for derivability treat sequents as basic objects, for admissibility, sequent rules are basic. Proof systems are defined here for the admissible rules of classes of both modal logics, including K4, S4, and GL, and intermediate logics, including Intuitionistic logic IPC, De Morgan (or Jankov) logic KC, and logics BCn (n = 1, 2, . . .) with bounded cardinality Kripke models. With minor restrictions, proof search in these systems terminates, giving decision procedures for admissibility in the corresponding logics.