Cut Elimination Theorem for Non-Commutative Hypersequent Calculus

Andrzej Indrzejczak

Bulletin of the Section of Logic (2017)

  • Volume: 46, Issue: 1/2
  • ISSN: 0138-0680

Abstract

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

How to cite

top

Andrzej Indrzejczak. "Cut Elimination Theorem for Non-Commutative Hypersequent Calculus." Bulletin of the Section of Logic 46.1/2 (2017): null. <http://eudml.org/doc/295597>.

@article{AndrzejIndrzejczak2017,
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.},
author = {Andrzej Indrzejczak},
journal = {Bulletin of the Section of Logic},
keywords = {temporal logic; linear time; hypersequent calculus; cut elimination},
language = {eng},
number = {1/2},
pages = {null},
title = {Cut Elimination Theorem for Non-Commutative Hypersequent Calculus},
url = {http://eudml.org/doc/295597},
volume = {46},
year = {2017},
}

TY - JOUR
AU - Andrzej Indrzejczak
TI - Cut Elimination Theorem for Non-Commutative Hypersequent Calculus
JO - Bulletin of the Section of Logic
PY - 2017
VL - 46
IS - 1/2
SP - null
AB - 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.
LA - eng
KW - temporal logic; linear time; hypersequent calculus; cut elimination
UR - http://eudml.org/doc/295597
ER -

References

top
  1. [1] A. Avron, A Constructive Analysis of RM, Journal of Symbolic Logic 52 (1987), pp. 939–951. 
  2. [2] A. Avron, Using Hypersequents in Proof Systems for Non-Classical Logics, Annals of Mathematics and Artificial Intelligence 4 (1991), pp. 225–248. 
  3. [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. 
  4. [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. 
  5. [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. 
  6. [6] A. Ciabattoni, N. Galatos and K. Terui, From axioms to analytic rules in nonclassical logics, LICS (2008), pp. 229–240. 
  7. [7] A. Indrzejczak, Cut-free Hypersequent Calculus for S4.3, Bulletin of the Section of Logic 41:1/2 (2012), pp. 89–104. 
  8. [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. 
  9. [9] A. Indrzejczak, Linear Time in Hypersequent Framework, The Bulletin of Symbolic Logic 22/1 (2016), pp. 121–144. 
  10. [10] O. Lahav, From Frame Properties to Hypersequent Rules in Modal Logics, LICS 2013. 
  11. [11] B. Lellmann, Axioms vs hypersequent rules with context restrictions, [in:] Proceedings of IJCAR, Springer 2014, pp. 307–321. 
  12. [12] B. Lellmann, Linear Nested Sequents, 2-Sequents and Hypersequents, [in:] TABLEAUX, Springer 2015, pp. 135–150. 
  13. [13] H. Kurokawa, Hypersequent Calculi for Modal Logics Extending S4, [in:] New Frontiers in Artificial Intelligence (2013), pp. 51–68, Springer, 2014. 
  14. [14] G. Metcalfe, N. Olivetti and D. Gabbay, Proof Theory for Fuzzy Logics, Springer 2008. 
  15. [15] F. Poggiolesi, A Cut-free Simple Sequent Calculus for Modal Logic S5, Review of Symbolic Logic 1 (2008), pp. 3–15. 
  16. [16] F. Poggiolesi, Gentzen Calculi for Modal Propositional Logics, Springer, 2011. 
  17. [17] G. Pottinger, Uniform Cut-free formulations of T, S4 and S5 (abstract), Journal of Symbolic Logic 48 (1983), p. 900. 
  18. [18] K. Schütte, Proof Theory, Springer, 1977. 

NotesEmbed ?

top

You must be logged in to post comments.

To embed these notes on your page include the following JavaScript code on your page where you want the notes to appear.

Only the controls for the widget will be shown in your chosen language. Notes will be shown in their authored language.

Tells the widget how many notes to show per page. You can cycle through additional notes using the next and previous controls.

    
                

                
Note: Best practice suggests putting the JavaScript code just before the closing </body> tag.