Simple cut elimination proof for hybrid logic

Andrzej Indrzejczak



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.


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

Full Text:



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.

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.

ISSN: 1425-3305 (print version)

ISSN: 2300-9802 (electronic version)

Partnerzy platformy czasopism