Proof theory for admissible rules (Q1023055): Difference between revisions
From MaRDI portal
Added link to MaRDI item. |
Set profile property. |
||
Property / MaRDI profile type | |||
Property / MaRDI profile type: MaRDI publication profile / rank | |||
Normal rank |
Revision as of 01:56, 5 March 2024
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | Proof theory for admissible rules |
scientific article |
Statements
Proof theory for admissible rules (English)
0 references
10 June 2009
0 references
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.
0 references
admissible rules
0 references
analytic proof system
0 references
modal logic
0 references
intuitionistic logic
0 references