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 Author https://orcid.org/0000-0002-9834-1940
Andrea Masini Universit`a di Verona, Dipartimento di Informatica Author
Margherita Zorzi Universit`a di Verona, Dipartimento di Informatica Author

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

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

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 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 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 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 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 DOI: https://doi.org/10.1305/ndjfl/1093894722

M. Fitting, Proof methods for modal and intuitionistic logics, Springer–Verlag (1983). 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 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 DOI: https://doi.org/10.2307/2275370

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

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 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 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 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 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. 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. 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 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 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 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 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 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 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).

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

L. Vigan`o, Labelled non-classical logics, Kluwer Academic Publishers, Dordrecht (2000). 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 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 DOI: https://doi.org/10.1023/A:1005125717300