Cut Elimination for Extended Sequent Calculi

Simone Martini; Andrea Masini; Margherita Zorzi

doi:10.18778/0138-0680.2023.22

Authors

Simone Martini Universit`a di Bologna, Dipartimento di Informatica – Scienza e Ingegneria https://orcid.org/0000-0002-9834-1940
Andrea Masini Universit`a di Verona, Dipartimento di Informatica
Margherita Zorzi Universit`a di Verona, Dipartimento di Informatica

DOI:

https://doi.org/10.18778/0138-0680.2023.22

Keywords:

proof theory, sequent calculus, cut elimination, modal logic, 2-sequents

Abstract

We present a syntactical cut-elimination proof for an extended sequent calculus covering the classical modal logics in the \(\mathsf{K}\), \(\mathsf{D}\), \(\mathsf{T}\), \(\mathsf{K4}\), \(\mathsf{D4}\) and \(\mathsf{S4}\) 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 \(\Box\) and \(\Diamond\). 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.

References

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.
Google Scholar DOI: https://doi.org/10.1093/oso/9780198538622.003.0001

J. L. Bell, M. Machover, A course in mathematical logic, North Holland, Amsterdam (1977).
Google Scholar

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: https://doi.org/10.1017/s1755020320000180
Google Scholar DOI: https://doi.org/10.1017/S1755020320000180

C. Cerrato, Cut-free modal sequents for normal modal logics, Notre Dame Journal of Formal Logic, vol. 34(4) (1993), pp. 564–582, DOI: https://doi.org/10.1305/ndjfl/1093633906
Google Scholar DOI: https://doi.org/10.1305/ndjfl/1093633906

C. Cerrato, Modal tree-sequents, Mathematical Logic Quarterly, vol. 42(2) (1996), pp. 197–210, DOI: https://doi.org/10.1002/malq.19960420117
Google Scholar DOI: https://doi.org/10.1002/malq.19960420117

A. Ciabattoni, R. Ramanayake, H. Wansing, Hypersequent and display calculi—a unified perspective, Studia Logica, vol. 102(6) (2014), pp. 1245–1294, DOI: https://doi.org/10.1007/s11225-014-9566-z
Google Scholar DOI: https://doi.org/10.1007/s11225-014-9566-z

M. Fitting, Tableau methods of proof for modal logics, Notre Dame Journal of Formal Logic, vol. 13(2) (1972), pp. 237–247, DOI: https://doi.org/10.1305/ndjfl/1093894722
Google Scholar DOI: https://doi.org/10.1305/ndjfl/1093894722

M. Fitting, Proof methods for modal and intuitionistic logics, Springer–Verlag (1983).
Google Scholar DOI: https://doi.org/10.1007/978-94-017-2794-5

M. Fitting, Prefixed tableaus and nested sequents, Annals of Pure and Applied Logic, vol. 163(3) (2012), pp. 291–313, DOI: https://doi.org/10.1016/j.apal.2011.09.004
Google Scholar DOI: https://doi.org/10.1016/j.apal.2011.09.004

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: https://doi.org/10.2307/2275370
Google Scholar DOI: https://doi.org/10.2307/2275370

J.-Y. Girard, Proof theory and logical complexity, vol. 1, Bibliopolis, Naples (1987).
Google Scholar

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: https://doi.org/10.1093/jigpal/6.5.735
Google Scholar DOI: https://doi.org/10.1093/jigpal/6.5.735

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: https://doi.org/10.1007/978-3-319-24312-2_10
Google Scholar DOI: https://doi.org/10.1007/978-3-319-24312-2_10

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: https://doi.org/10.1007/978-3-642-36039-8_14
Google Scholar DOI: https://doi.org/10.1007/978-3-642-36039-8_14

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: https://doi.org/10.1145/3288757
Google Scholar DOI: https://doi.org/10.1145/3288757

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.
Google Scholar DOI: https://doi.org/10.1017/CBO9780511629150.010

S. Martini, A. Masini, A Computational Interpretation of Modal Proofs, [in:] H. Wansing (ed.), Proof Theory of Modal Logics, Kluwer (1994), pp. 213–241.
Google Scholar DOI: https://doi.org/10.1007/978-94-017-2798-3_12

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: https://doi.org/10.1145/3461661
Google Scholar DOI: https://doi.org/10.1145/3461661

A. Masini, 2-Sequent calculus: A proof theory of modalities, Annals of Pure and Applied Logic, vol. 58(3) (1992), pp. 229–246, DOI: https://doi.org/10.1016/0168-0072(92)90029-Y
Google Scholar DOI: https://doi.org/10.1016/0168-0072(92)90029-Y

A. Masini, 2-Sequent calculus: intuitionism and natural deduction, Journal of Logic and Computation, vol. 3(5) (1993), pp. 533–562, DOI: https://doi.org/10.1093/logcom/3.5.533
Google Scholar DOI: https://doi.org/10.1093/logcom/3.5.533

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: https://doi.org/10.1093/logcom/exq028
Google Scholar DOI: https://doi.org/10.1093/logcom/exq028

G. Mints, Indexed systems of sequents and cut-elimination, Journal of Philosophical Logic, vol. 26(6) (1997), pp. 671–696, DOI: https://doi.org/10.1023/A:1017948105274
Google Scholar DOI: https://doi.org/10.1023/A:1017948105274

S. Negri, Proof theory for modal logic, Philosophy Compass, vol. 6(8) (2011), pp. 523–538, DOI: https://doi.org/10.1111/j.1747-9991.2011.00418.x
Google Scholar DOI: https://doi.org/10.1111/j.1747-9991.2011.00418.x

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

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

L. Vigan`o, Labelled non-classical logics, Kluwer Academic Publishers, Dordrecht (2000).
Google Scholar DOI: https://doi.org/10.1007/978-1-4757-3208-5

H. Wansing, Sequent calculi for normal modal propositional logics, Journal of Logic and Computation, vol. 4(2) (1994), pp. 125–142, DOI: https://doi.org/10.1093/logcom/4.2.125
Google Scholar DOI: https://doi.org/10.1093/logcom/4.2.125

H. Wansing, Predicate logics on display, Studia Logica, vol. 62(1) (1999), pp. 49–75, DOI: https://doi.org/10.1023/A:1005125717300
Google Scholar DOI: https://doi.org/10.1023/A:1005125717300