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

• Autorzy: Torben Braüner

Abstrakty

EN

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.

Słowa kluczowe

EN

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

• Wydawca: Wydawnictwo Uniwersytetu Łódzkiego
• Czasopismo: Bulletin of the Section of Logic
• Rocznik: 2022
• Tom: 51
• Numer: 2
• Strony: 143-162

Daty

wydano

2022

Twórcy

autor

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/0000000345821702

Bibliografia

• 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
• 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
• 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
• 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
• 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.
• 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
• 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
• 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
• 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
• 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
• 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
• 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
• J.-Y. Girard, Y. Lafont, P. Taylor, Proofs and Types, vol. 7 of Cambridge Tracts in Theoretical Computer Science, Cambridge University Press, Cambridge (1989).
• 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
• 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
• 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
• D. Prawitz, Natural Deduction. A Proof-Theoretical Study, Almqvist and Wiksell, Stockholm (1965).
• 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
• 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.
• 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
• 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
• A. Simpson, The Proof Theory and Semantics of Intuitionistic Modal logic, Ph.D. thesis, University of Edinburgh (1994).
• 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

Identyfikatory

DOI

10.18778/0138-0680.2022.02

nonstd.3pn.id

2142755