Proof theory for admissible rules

R. Iemhoff, G. Metcalfe

Research output: Contribution to journalArticleAcademicpeer-review

1 Downloads (Pure)


Admissible rules of a logic are those rules under which the set of theorems of the logic is closed. In this paper, a Gentzen-style framework is introduced for analytic proof systems that derive admissible rules of non-classical logics. While Gentzen systems for derivability treat sequents as basic objects, for admissibility, the basic objects are sequent rules. Proof systems are defined here for admissible rules of classes of modal logics, including K4, S4, and GL, and also Intuitionistic Logic IPC. With minor restrictions, proof search in these systems terminates, giving decision procedures for admissibility in the logics.
Original languageEnglish
Pages (from-to)171-186
Number of pages16
JournalAnnals of Pure and Applied Logic
Issue number159 (1-2)
Publication statusPublished - 2009


  • Admissible Rules
  • Proof Theory
  • Intuitionistic Logic
  • Modal Logic


Dive into the research topics of 'Proof theory for admissible rules'. Together they form a unique fingerprint.

Cite this