Proof theory for admissible rules

Citations of this article
Mendeley users who have this article in their library.


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. © 2009 Elsevier B.V. All rights reserved.




Iemhoff, R., & Metcalfe, G. (2009). Proof theory for admissible rules. Annals of Pure and Applied Logic, 159(1–2), 171–186.

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free