Cut Elimination Theorem for Non-Commutative Hypersequent Calculus

Andrzej Indrzejczak

doi:10.18778/0138-0680.46.1.2.10

Authors

Andrzej Indrzejczak University of Łódź, Department of Logic, Lindleya 3/5, Łódź

DOI:

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

Keywords:

temporal logic, linear time, hypersequent calculus, cut elimination

Abstract

Hypersequent calculi (HC) can formalize various non-classical logics. In [9] we presented a non-commutative variant of HC for the weakest temporal logic of linear frames Kt4.3 and some its extensions for dense and serial flow of time. The system was proved to be cut-free HC formalization of respective temporal logics by means of Schütte/Hintikka-style semantical argument using models built from saturated hypersequents. In this paper we present a variant of this calculus for Kt4.3 with a constructive syntactical proof of cut elimination.

References

[1] A. Avron, A Constructive Analysis of RM, Journal of Symbolic Logic 52 (1987), pp. 939–951.
Google Scholar

[2] A. Avron, Using Hypersequents in Proof Systems for Non-Classical Logics, Annals of Mathematics and Artificial Intelligence 4 (1991), pp. 225–248.
Google Scholar

[3] A. Avron, The Method of Hypersequents in the Proof Theory of Propositional Non-Classical Logics, [in:] W. Hodges et al. (eds.), Logic: From Foundations to Applications, Oxford Science Publication, Oxford, 1996, pp. 1–32.
Google Scholar

[4] M. Baaz, A. Ciabattoni and C. G. Fermüller, Hypersequent Calculi for Gödel Logics – a Survey, Journal of Logic and Computation 13 (2003), pp. 1–27.
Google Scholar

[5] K. Bednarska and A. Indrzejczak, Hypersequent Calculi for S5 – the Methods of Cut-elimination, Logic and Logical Philosophy 24/3 (2015), pp. 277–311.
Google Scholar

[6] A. Ciabattoni, N. Galatos and K. Terui, From axioms to analytic rules in nonclassical logics, LICS (2008), pp. 229–240.
Google Scholar

[7] A. Indrzejczak, Cut-free Hypersequent Calculus for S4.3, Bulletin of the Section of Logic 41:1/2 (2012), pp. 89–104.
Google Scholar

[8] A. Indrzejczak, Eliminability of Cut in Hypersequent Calculi for some Modal Logics of Linear Frames, Information Processing Letters 115/2 (2015), pp. 75–81.
Google Scholar

[9] A. Indrzejczak, Linear Time in Hypersequent Framework, The Bulletin of Symbolic Logic 22/1 (2016), pp. 121–144.
Google Scholar

[10] O. Lahav, From Frame Properties to Hypersequent Rules in Modal Logics, LICS 2013.
Google Scholar

[11] B. Lellmann, Axioms vs hypersequent rules with context restrictions, [in:] Proceedings of IJCAR, Springer 2014, pp. 307–321.
Google Scholar

[12] B. Lellmann, Linear Nested Sequents, 2-Sequents and Hypersequents, [in:] TABLEAUX, Springer 2015, pp. 135–150.
Google Scholar

[13] H. Kurokawa, Hypersequent Calculi for Modal Logics Extending S4, [in:] New Frontiers in Artificial Intelligence (2013), pp. 51–68, Springer, 2014.
Google Scholar

[14] G. Metcalfe, N. Olivetti and D. Gabbay, Proof Theory for Fuzzy Logics, Springer 2008.
Google Scholar

[15] F. Poggiolesi, A Cut-free Simple Sequent Calculus for Modal Logic S5, Review of Symbolic Logic 1 (2008), pp. 3–15.
Google Scholar

[16] F. Poggiolesi, Gentzen Calculi for Modal Propositional Logics, Springer, 2011.
Google Scholar

[17] G. Pottinger, Uniform Cut-free formulations of T, S4 and S5 (abstract), Journal of Symbolic Logic 48 (1983), p. 900.
Google Scholar

[18] K. Schütte, Proof Theory, Springer, 1977.
Google Scholar