×

zbMATH — the first resource for mathematics

Proof theory for admissible rules. (English) Zbl 1174.03024
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 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 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 E. Jeřábek [J. Log. Comput. 15, No. 4, 411–431 (2005; Zbl 1077.03011)], drawing on the work of 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.

MSC:
03F07 Structure of proofs
03B20 Subsystems of classical logic (including intuitionistic logic)
03B45 Modal logic (including the logic of norms)
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] N. Bezhanishvili, Lattices of intermediate and cylindric modal logics, Ph.D. Thesis, ILLC, University of Amsterdam, 2006
[2] Chagrov, A.; Zakharyaschev, M., Modal logic, (1996), Oxford University Press · Zbl 1003.03516
[3] de Jongh, D., Formulas in one propositional variable, (), 51-64
[4] Friedman, H.M., One hundred and two problems in mathematical logic, Journal of symbolic logic, 40, 2, 113-129, (1975) · Zbl 0318.02002
[5] Ghilardi, S., Unification in intuitionistic logic, Journal of symbolic logic, 64, 2, 859-880, (1999) · Zbl 0930.03009
[6] Ghilardi, S., Best solving modal equations, Annals of pure and applied logic, 102, 3, 184-198, (2000) · Zbl 0949.03010
[7] Ghilardi, S., A resolution/tableaux algorithm for projective approximations in IPC, Logic journal of the IGPL, 10, 3, 227-241, (2002) · Zbl 1005.03504
[8] Goré, R., Tableau methods for modal and temporal logics, (), 297-396 · Zbl 0972.03529
[9] Iemhoff, R., On the admissible rules of intuitionistic propositional logic, Journal of symbolic logic, 66, 1, 281-294, (2001) · Zbl 0986.03013
[10] Iemhoff, R., Preservativity logic (an analogue of interpretability logic for constructive theories), Mathematical logic quarterly, 49, 3, 1-21, (2003) · Zbl 1024.03061
[11] Iemhoff, R., Towards a proof system for admissibility, (), 255-270 · Zbl 1116.03304
[12] Iemhoff, R., Intermediate logics and visser’s rules, Notre dame journal of formal logic, 46, 1, 65-81, (2005) · Zbl 1102.03032
[13] Iemhoff, R.; Metcalfe, G., Hypersequent systems for the admissible rules of modal and intermediate logics, (), 230-245 · Zbl 1211.03037
[14] Jeřábek, E., Admissible rules of modal logics, Journal of logic and computation, 15, 411-431, (2005) · Zbl 1077.03011
[15] Jeřábek, E., Complexity of admissible rules, Archive for mathematical logic, 46, 2, 73-92, (2007) · Zbl 1115.03010
[16] P. Rozière, Regles Admissibles en calcul propositionnel intuitionniste, Ph.D. Thesis, Université Paris VII, 1992
[17] Rybakov, V., Admissibility of logical inference rules, (1997), Elsevier · Zbl 0872.03002
[18] Troelstra, A.S.; Schwichtenberg, H., Basic proof theory, (2000), Cambridge University Press · Zbl 0957.03053
[19] Visser, A., Substitutions of \(\Sigma\)-sentences: explorations between intuitionistic propositional logic and intuitionistic arithmetic, Annals of pure and applied logic, 114, 1-3, 227-271, (2002) · Zbl 1009.03029
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.