Geodesic
Cut Elimination for Extended Sequent Calculi
Bulletin of the Section of Logic, Tome 52 (2023) no. 4, pp. 459-495.

Voir la notice de l'article provenant de la source Library of Science

We present a syntactical cut-elimination proof for an extended sequent calculus covering the classical modal logics in the 𝖪, 𝖣, 𝖳, 𝖪4, 𝖣4 and 𝖲4 spectrum. We design the systems uniformly since they all share the same set of rules. Different logics are obtained by “tuning” a single parameter, namely a constraint on the applicability of the cut rule and on the (left and right, respectively) rules for and . Starting points for this research are 2-sequents and indexed-based calculi (sequents and tableaux). By extending and modifying existing proposals, we show how to achieve a syntactical proof of the cut-elimination theorem that is as close as possible to the one for first-order classical logic. In doing this, we implicitly show how small is the proof-theoretical distance between classical logic and the systems under consideration.
Keywords: proof theory, sequent calculus, cut elimination, modal logic, 2-sequents 
@article{BSL_2023_52_4_a2,
     author = {Martini, Simone and Masini, Andrea and Zorzi, Margherita},
     title = {Cut {Elimination} for {Extended} {Sequent} {Calculi}},
     journal = {Bulletin of the Section of Logic},
     pages = {459--495},
     publisher = {mathdoc},
     volume = {52},
     number = {4},
     year = {2023},
     language = {en},
     url = {http://geodesic.mathdoc.fr/item/BSL_2023_52_4_a2/}
}
TY  - JOUR
AU  - Martini, Simone
AU  - Masini, Andrea
AU  - Zorzi, Margherita
TI  - Cut Elimination for Extended Sequent Calculi
JO  - Bulletin of the Section of Logic
PY  - 2023
SP  - 459
EP  - 495
VL  - 52
IS  - 4
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/item/BSL_2023_52_4_a2/
LA  - en
ID  - BSL_2023_52_4_a2
ER  - 
%0 Journal Article
%A Martini, Simone
%A Masini, Andrea
%A Zorzi, Margherita
%T Cut Elimination for Extended Sequent Calculi
%J Bulletin of the Section of Logic
%D 2023
%P 459-495
%V 52
%N 4
%I mathdoc
%U http://geodesic.mathdoc.fr/item/BSL_2023_52_4_a2/
%G en
%F BSL_2023_52_4_a2
Martini, Simone; Masini, Andrea; Zorzi, Margherita. Cut Elimination for Extended Sequent Calculi. Bulletin of the Section of Logic, Tome 52 (2023) no. 4, pp. 459-495. http://geodesic.mathdoc.fr/item/BSL_2023_52_4_a2/

[1] A. Avron, The method of hypersequents in the proof theory of propositional non-classical logics, [in:] W. Hodges, M. Hyland, C. Steinhorn, J. Truss (eds.), Logic: From Foundations to Applications, Oxford Science Publications, Clarendon Press, New York (1996), pp. 1–32.

[2] J. L. Bell, M. Machover, A course in mathematical logic, North Holland, Amsterdam (1977).

[3] S. Burns, R. Zach, Cut-free completeness for modular hypersequent calculi for modal Logics K, T, and D, Review of Symbolic Logic, vol. 14(4) (2021), pp. 910–929 | DOI

[4] C. Cerrato, Cut-free modal sequents for normal modal logics, Notre Dame Journal of Formal Logic, vol. 34(4) (1993), pp. 564–582 | DOI

[5] C. Cerrato, Modal tree-sequents, Mathematical Logic Quarterly, vol. 42(2) (1996), pp. 197–210 | DOI

[6] A. Ciabattoni, R. Ramanayake, H. Wansing, Hypersequent and display calculi—a unified perspective, Studia Logica, vol. 102(6) (2014), pp. 1245–1294 | DOI

[7] M. Fitting, Tableau methods of proof for modal logics, Notre Dame Journal of Formal Logic, vol. 13(2) (1972), pp. 237–247 | DOI

[8] M. Fitting, Proof methods for modal and intuitionistic logics, Springer–Verlag (1983).

[9] M. Fitting, Prefixed tableaus and nested sequents, Annals of Pure and Applied Logic, vol. 163(3) (2012), pp. 291–313 | DOI

[10] D. M. Gabbay, R. J. G. B. de Queiroz, Extending the Curry-Howard interpretation to linear, relevant and other resource logics, Journal of Symbolic Logic, vol. 57(4) (1992), pp. 1319–1365 | DOI

[11] J.-Y. Girard, Proof theory and logical complexity, vol. 1, Bibliopolis, Naples (1987).

[12] S. Guerrini, S. Martini, A. Masini, An analysis of (linear) exponentials based on extended sequents, Logic Journal of the IGPL, vol. 6(5) (1998), pp. 735–753 | DOI

[13] B. Lellmann, Linear nested sequents, 2-sequents and hypersequents, [in:] H. de Nivelle (ed.), Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX 2015, vol. 9323 of Lecture Notes in Computer Science, Springer (2015), pp. 135–150 | DOI

[14] B. Lellmann, D. Pattinson, Constructing cut free sequent systems with context restrictions based on classical or intuitionistic logic, [in:] K. Lodaya (ed.), Logic and Its Applications, 5th Indian Conference, ICLA 2013, vol. 7750 of Lecture Notes in Computer Science, Springer (2013), pp. 148–160 | DOI

[15] B. Lellmann, E. Pimentel, Modularisation of sequent calculi for normal and non-normal modalities, ACM Transactions on Compututational Logic, vol. 20(2) (2019), pp. 7:1–7:46 | DOI

[16] S. Martini, A. Masini, On the fine structure of the exponential rule, [in:] J.-Y. Girard, Y. Lafont, L. Regnier (eds.), Advances in Linear Logic, Cambridge University Press (1993), pp. 197–210.

[17] S. Martini, A. Masini, A Computational Interpretation of Modal Proofs, [in:] H. Wansing (ed.), Proof Theory of Modal Logics, Kluwer (1994), pp. 213–241.

[18] S. Martini, A. Masini, M. Zorzi, From 2-sequents and linear nested sequents to natural eduction for normal modal logics, ACM Transactions on Compututational Logic, vol. 22(3) (2021), pp. 19:1–19:29 | DOI

[19] A. Masini, 2-Sequent calculus: A proof theory of modalities, Annals of Pure and Applied Logic, vol. 58(3) (1992), pp. 229–246 | DOI

[20] A. Masini, 2-Sequent calculus: intuitionism and natural deduction, Journal of Logic and Computation, vol. 3(5) (1993), pp. 533–562 | DOI

[21] A. Masini, L. Vigan`o, M. Volpe, Labelled natural deduction for a bundled branching temporal logic, Journal of Logic and Computation, vol. 21(6) (2011), pp. 1093–1163 | DOI

[22] G. Mints, Indexed systems of sequents and cut-elimination, Journal of Philosophical Logic, vol. 26(6) (1997), pp. 671–696 | DOI

[23] S. Negri, Proof theory for modal logic, Philosophy Compass, vol. 6(8) (2011), pp. 523–538 | DOI

[24] A. Simpson, The proof theory and semantics of intuitionistic modal logic, Ph.D. thesis, University of Edinburgh, UK (1993).

[25] G. Takeuti, Proof theory, 2nd ed., vol. 81 of Studies in Logic and the Foundations of Mathematics, North-Holland Publishing Co., Amsterdam (1987).

[26] L. Vigan`o, Labelled non-classical logics, Kluwer Academic Publishers, Dordrecht (2000).

[27] H. Wansing, Sequent calculi for normal modal propositional logics, Journal of Logic and Computation, vol. 4(2) (1994), pp. 125–142 | DOI

[28] H. Wansing, Predicate logics on display, Studia Logica, vol. 62(1) (1999), pp. 49–75 | DOI