Proof theory for admissible rules
type: Item
instance of: scholarly article
title: Proof theory for admissible rules
zbMATH Open document ID: 1174.03024
author: Rosalie Iemhoff
author: George Metcalfe
published in: Annals of Pure and Applied Logic
publication date: 2009-06-10T00:00:00Z
full work available at URL: https://dspace.library.uu.nl/handle/1874/26742
review text: 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.
reviewed by: Emil Jeřábek
Mathematics Subject Classification ID: 03F07
Mathematics Subject Classification ID: 03B20
Mathematics Subject Classification ID: 03B45
zbMATH DE Number: 5563898
zbMATH Keywords: admissible rules
zbMATH Keywords: analytic proof system
zbMATH Keywords: modal logic
zbMATH Keywords: intuitionistic logic
MaRDI profile type: Publication
OpenAlex ID: W2170146694
cites work: Q4789450
cites work: Q3338239
cites work: One hundred and two problems in mathematical logic
cites work: Unification in intuitionistic logic
cites work: Best solving modal equations
cites work: A Resolution/Tableaux Algorithm for Projective Approximations in IPC
cites work: Tableau methods for modal and temporal logics
cites work: On the admissible rules of intuitionistic propositional logic
cites work: Preservativity logic: An analogue of interpretability logic for constructive theories
cites work: Computer Science Logic
cites work: Intermediate logics and Visser's rules
cites work: Hypersequent Systems for the Admissible Rules of Modal and Intermediate Logics
cites work: Admissible Rules of Modal Logics
cites work: Complexity of admissible rules
cites work: Admissibility of logical inference rules
cites work: Q4499084
cites work: Substitutions of \(\Sigma_1^0\)-sentences: Explorations between intuitionistic propositional logic and intuitionistic arithmetic
DOI: 10.1016/J.APAL.2008.10.011
description: scientific article; zbMATH DE number 5563898