Proof theory for admissible rules (Q1023055): Difference between revisions

The paper is a contribution to the study of admissible rules of nonclassical propositional logics. A rule (closed under substitution) is admissible in a logic if the set of its theorems is closed under the rule. Admissibility was shown to be decidable in a variety of normal modal and superintuitionistic logics by \textit{V. V. Rybakov} [Admissibility of logical inference rules. Amsterdam: Elsevier (1997; Zbl 0872.03002)]. Explicit bases of admisible rules were constructed for some superintuitionistic logics by \textit{R. Iemhoff} [J. Symb. Log. 66, No. 1, 281--294 (2001; Zbl 0986.03013); Notre Dame J. Formal Logic 46, No. 1, 65--81 (2005; Zbl 1102.03032)] and for some modal logics by \textit{E. Jeřábek} [J. Log. Comput. 15, No. 4, 411--431 (2005; Zbl 1077.03011)], drawing on the work of \textit{S. Ghilardi} [J. Symb. Log. 64, No. 2, 859--880 (1999; Zbl 0930.03009); Ann. Pure Appl. Logic 102, No. 3, 183--198 (2000; Zbl 0949.03010)] on projective formulas. In the paper under review, the authors present a proof-theoretic treatment of admissible rules. They introduce certain analytic calculi operating with multiple-conclusion rules consisting of Gentzen-style sequents of formulas, and show their completeness for admissibility in a class of modal logics and in intuitionistic logic.