Simple cut elimination proof for hybrid logic

• Authors: Indrzejczak Andrzej
• Languages of publication: EN

Abstracts

EN

In the paper we present a relatively simple proof of cut elimination theorem for variety of hybrid logics in the language with satisfaction operators and universal modality. The proof is based on the strategy introduced originally in the framework of hypersequent calculi but it works well also for standard sequent calculi. Sequent calculus examined in the paper works on so called satisfaction formulae and cover all logics adequate with respect to classes of frames defined by so called geometric conditions.

Keywords

EN

hybrid logic; cut elimination theorem; hypersequent calculi; sequent calculi; geometric conditions

• Publisher: Uniwersytet Mikołaja Kopernika (Nicolaus Copernicus University in Toruń)
• Journal: Logic and Logical Philosophy
• Year: 2016
• Volume: 25
• Issue: 2
• Pages: 129–141

Dates

online

2016-04-04

Contributors

author

Indrzejczak Andrzej

• Department of Logic, University of Łódź, ul. Kopcińskiego 16/18, 90–232 Łódź, Poland

References

• Blackburn, P., “Nominal tense logic”, Notre Dame Journal of Formal Logic, 34, 1 (1992): 56–83. DOI:10.1305/ndjfl/1093634564
• Blackburn, P., “Internalizing labelled deduction”, Journal of Logic and Computation, 10, 1 (2000): 137–168. DOI:10.1093/logcom/10.1.137
• Bolander, T., and T. Braüner, “Tableau-based decision procedures for hybrid logic”, Journal of Logic and Computation, 16, 6 (2006): 737–763. DOI:10.1093/logcom/exl008
• Braüner, T., “Natural deduction for hybrid logic”, Journal of Logic and Computation, 14, 3 (2004): 137–168. DOI:10.1093/logcom/14.3.329
• Braüner, T., “Hybrid logic”, in Edward N. Zalta (ed.), The Stanford Encyclopedia of Philosophy, Winter 2014 edition, 2014. http://plato.stanford.edu/archives/win2014/entries/logic-hybrid/
• Braüner, T., Hybrid Logic and its Proof-Theory, Roskilde, 2009.
• Ciabattoni, A., G. Metcalfe, and F. Montagna, “Algebraic and proof-theoretic characterizations of truth stressers for mtl and its extensions”, Fuzzy Sets and Systems, 161, 3 (2010): 369–389. DOI:10.1016/j.fss.2009.09.001
• Curry, H.B., Foundations of Mathematical Logic, McGraw-Hill, New York, 1963.
• Demri, S., “Sequent calculi for nominal tense logics: A step towards mechanization”, pages 140–154 in N. Murray (ed.), Tableaux 99, volume 1617 of Lecture Notes in Computer Science, Springer, Berlin, 1999.
• Demri, S., and R. Goré, “Cut-free display calculi for nominal tense logics”, pages 155–170 in N. Murray (ed.), Tableaux 99, volume 1617 of Lecture Notes in Computer Science, Springer, Berlin, 1999.
• Gargov, G., and V. Goranko, “Modal logic with names”, Journal of Philosophical Logic, 22, 6 (1993): 607–636. DOI:10.1007/BF01054038
• Goranko, V., “Temporal logic with reference pointers”, chapter 9, pages 133–148, in Temporal Logic, volume 827 of Lecture Notes in Computer Science, Springer, 1994. DOI:10.1007/BFb0013985
• Indrzejczak, A., “Modal hybrid logic”, Logic and Logical Philosophy, 16, 2–3 (2007): 147–257. DOI:10.12775/LLP.2007.006
• Indrzejczak, A., Natural Deduction, Hybrid Systems and Modal Logics, vol. 30 of Trends in Logic, Springer, 2010. DOI:10.1007/978-90-481-8785-0
• Indrzejczak, A., and M. Zawidzki, “Decision procedures for some strong hybrid logics”, Logic and Logical Philosophy, 22, 4 (2013): 389–409. DOI:10.12775/LLP.2013.022
• Negri, S., “Proof analysis in modal logic”, Journal of Philosophical Logic, 34, 5–6 (2005): 507–544. DOI:10.1007/s10992-005-2267-3
• Prior, A., Time and Modality, Oxford University Press, Oxford, 1957.
• Seligman, J., “Internalization: The case of hybrid logics”, Journal of Logic and Computation, 11, 5 (2001): 671–689. DOI:10.1093/logcom/11.5.671
• Zawidzki, M., Deductive Systems and the Decidability Problem for Hybrid Logics, Univ. of Lódź Press and Jagielonian Univ. Press, 2013.

Identifiers

DOI

10.12775/LLP.2016.004