Analytic Non-Labelled Proof-Systems for Hybrid Logic: Overview and a couple of striking facts

Torben Braüner

doi:10.18778/0138-0680.2022.02

Authors

Torben Braüner Roskilde University, Department of People and Technology, Building 10.1, Universitetsvej 1, P.O. Box 260, DK-4000 Roskilde, Denmark https://orcid.org/0000-0003-4582-1702

DOI:

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

Keywords:

hybrid logic, natural deduction systems, sequent systems, normalization, cut-elimination, analycity

Abstract

This paper is about non-labelled proof-systems for hybrid logic, that is, proofsystems where arbitrary formulas can occur, not just satisfaction statements. We give an overview of such proof-systems, focusing on analytic systems: Natural deduction systems, Gentzen sequent systems and tableau systems. We point out major results and we discuss a couple of striking facts, in particular that nonlabelled hybrid-logical natural deduction systems are analytic, but this is not proved in the usual way via step-by-step normalization of derivations.

References

M. Baaz, A. Leitsch, Methods of Cut-Elimination, vol. 34 of Trends in Logic Series, Springer, Dordrecht (2011), DOI: https://doi.org/10.1007/978-94-007-0320-9
Google Scholar DOI: https://doi.org/10.1007/978-94-007-0320-9

G. Bierman, V. de Paiva, On an Intuitionistic Modal Logic, Studia Logica, vol. 65 (2000), pp. 383–416, DOI: https://doi.org/10.1023/A:1005291931660
Google Scholar DOI: https://doi.org/10.1023/A:1005291931660

P. Blackburn, T. Bolander, T. Braüner, K. Jørgensen, Completeness and Termination for a Seligman-style Tableau System, Journal of Logic and Computation, vol. 27(1) (2017), pp. 81–107, DOI: https://doi.org/10.1093/logcom/exv052
Google Scholar DOI: https://doi.org/10.1093/logcom/exv052

T. Braüner, Two Natural Deduction Systems for Hybrid Logic: A Comparison, Journal of Logic, Language and Information, vol. 13 (2004), pp. 1–23, DOI: https://doi.org/10.1023/A:1026187215321
Google Scholar DOI: https://doi.org/10.1023/A:1026187215321

T. Braüner, Hybrid Logic, [in:] E. Zalta (ed.), The Stanford Encyclopedia of Philosophy, Stanford University (2005), URL: http://plato.stanford.edu/entries/logic-hybrid, substantive revision in 2017.
Google Scholar

T. Braüner, Hybrid Logic and its Proof-Theory, vol. 37 of Applied Logic Series, Springer, Dordrecht (2011), DOI: https://doi.org/10.1007/978-94-007-0002-4
Google Scholar DOI: https://doi.org/10.1007/978-94-007-0002-4

T. Braüner, Hybrid-Logical Reasoning in the Smarties and Sally-Anne Tasks, Journal of Logic, Language and Information, vol. 23 (2014), pp. 415–439, DOI: https://doi.org/10.1007/s10849-014-9206-z
Google Scholar DOI: https://doi.org/10.1007/s10849-014-9206-z

T. Braüner, I. Polyanskaya, P. Blackburn, A logical investigation of false-belief tasks, [in:] Proceedings of the 40th Annual Meeting of the Cognitive Science Society, Cognitive Science Society, Madison, Wisconsin, USA (2018), pp. 45–46, URL: https://cogsci.mindmodeling.org/2018/papers/0023/0023.pdf
Google Scholar

M. Fitting, Modal Proof Theory, [in:] P. Blackburn, J. van Benthem, F. Wolter (eds.), Handbook of Modal Logic, vol. 3 of Studies in Logic and Practical Reasoning, Elsevier, Amsterdam (2007), pp. 85–138, DOI: https://doi.org/10.1016/S1570-2464(07)80005-X
Google Scholar DOI: https://doi.org/10.1016/S1570-2464(07)80005-X

A. From, Synthetic Completeness for a Terminating Seligman-Style Tableau System, [in:] U. de’Liguoro, S. Berardi, T. Altenkirch (eds.), 26th International Conference on Types for Proofs and Programs (TYPES 2020), vol. 188 of Leibniz International Proceedings in Informatics (LIPIcs), Leibniz-Zentrum für Informatik, Schloss Dagstuhl (2021), pp. 5:1–5:17, DOI: https://doi.org/10.4230/LIPIcs.TYPES.2020.5
Google Scholar

A. From, P. Blackburn, J. Villadsen, Formalizing a Seligman-Style Tableau System for Hybrid Logic, [in:] N. Peltier, V. Sofronie-Stokkermans (eds.), Proceedings of 10th International Joint Conference on Automated Reasoning (IJCAR), vol. 12166 of Lecture Notes in Computer Science, Springer-Verlag, Cham (2020), pp. 474–482, DOI: https://doi.org/10.1007/978-3-030-51074-9_27
Google Scholar

J.-Y. Girard, Linear Logic, Theoretical Computer Science, vol. 50(1) (1987), pp. 1–102, DOI: https://doi.org/10.1016/0304-3975(87)90045-4
Google Scholar DOI: https://doi.org/10.1016/0304-3975(87)90045-4

J.-Y. Girard, Y. Lafont, P. Taylor, Proofs and Types, vol. 7 of Cambridge Tracts in Theoretical Computer Science, Cambridge University Press, Cambridge (1989).
Google Scholar

A. Indrzejczak, Natural Deduction, Hybrid Systems and Modal Logics, vol. 30 of Trends in Logic Series, Springer, Dordrecht (2010), DOI: https://doi.org/10.1007/978-90-481-8785-0
Google Scholar DOI: https://doi.org/10.1007/978-90-481-8785-0

K. Jørgensen, P. Blackburn, T. Bolander, T. Braüner, Completeness Proofs for Seligman-style Tableau Systems, [in:] L. Beklemishev, S. Demri (eds.), Proceedings of Advances in Modal Logic 2016, vol. 11 of Advances in Modal Logic, College Publications, Rickmansworth (2016), pp. 302–321, DOI: https://doi.org/10.1007/978-3-030-51074-9_27
Google Scholar DOI: https://doi.org/10.1007/978-3-030-51074-9_27

H. Kushida, M. Okada, A Proof-Theoretic Study of the Correspondence of Hybrid Logic and Classical Logic, Journal of Logic, Language and Information, vol. 16 (2007), pp. 35–61, DOI: https://doi.org/10.1007/s10849-006-9023-0
Google Scholar DOI: https://doi.org/10.1007/s10849-006-9023-0

D. Prawitz, Natural Deduction. A Proof-Theoretical Study, Almqvist and Wiksell, Stockholm (1965).
Google Scholar

D. Prawitz, Proofs and the Meaning and Completeness of the Logical Constants, [in:] J. Hintikka, I. Niiniluoto, E. Saarinen (eds.), Essays on Mathematical and Philosophical Logic, vol. 122 of Synthese Library (Studies in Epistemology, Logic, Methodology, and Philosophy of Science), Springer, Dordrecht (1979), pp. 25–40, DOI: https://doi.org/10.1007/978-94-009-9825-4_2
Google Scholar DOI: https://doi.org/10.1007/978-94-009-9825-4_2

L. Rips, Logical Approaches to Human Deductive Reasoning, [in:] J. Adler, L. Rips (eds.), Reasoning: Studies of Human Inference and Its Foundations, Cambridge University Press, Cambridge (2008), pp. 187–205.
Google Scholar DOI: https://doi.org/10.1017/CBO9780511814273.011

J. Seligman, The Logic of Correct Description, [in:] M. de Rijke (ed.), Advances in Intensional Logic, vol. 7 of Applied Logic Series, Springer, Dordrecht (1997), pp. 107 – 135, DOI: https://doi.org/10.1007/978-94-015-8879-9_5
Google Scholar DOI: https://doi.org/10.1007/978-94-015-8879-9_5

J. Seligman, Internalization: The Case of Hybrid Logics, Journal of Logic and Computation, vol. 11(5) (2001), pp. 671–689, DOI: https://doi.org/10.1093/logcom/11.5.671
Google Scholar DOI: https://doi.org/10.1093/logcom/11.5.671

A. Simpson, The Proof Theory and Semantics of Intuitionistic Modal logic, Ph.D. thesis, University of Edinburgh (1994).
Google Scholar

H. Wansing, Sequent Systems for Modal Logics, [in:] D. Gabbay, F. Guenthner (eds.), Handbook of Philosophical Logic, 2nd ed., vol. 8, Springer, Dordrecht (2002), pp. 61–145, DOI: https://doi.org/10.1007/978-94-010-0387-2_2
Google Scholar DOI: https://doi.org/10.1007/978-94-010-0387-2_2