Geodesic
Analytic Non-Labelled Proof-Systems for Hybrid Logic: Overview and a couple of striking facts
Bulletin of the Section of Logic, Tome 51 (2022) no. 2, pp. 143-162.

Voir la notice de l'article provenant de la source Library of Science

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.
Keywords: hybrid logic, natural deduction systems, sequent systems, normalization, cut-elimination, analycity 
@article{BSL_2022_51_2_a0,
     author = {Bra\"uner, Torben},
     title = {Analytic {Non-Labelled} {Proof-Systems} for {Hybrid} {Logic:} {Overview} and a couple of striking facts},
     journal = {Bulletin of the Section of Logic},
     pages = {143--162},
     publisher = {mathdoc},
     volume = {51},
     number = {2},
     year = {2022},
     language = {en},
     url = {http://geodesic.mathdoc.fr/item/BSL_2022_51_2_a0/}
}
TY  - JOUR
AU  - Braüner, Torben
TI  - Analytic Non-Labelled Proof-Systems for Hybrid Logic: Overview and a couple of striking facts
JO  - Bulletin of the Section of Logic
PY  - 2022
SP  - 143
EP  - 162
VL  - 51
IS  - 2
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/item/BSL_2022_51_2_a0/
LA  - en
ID  - BSL_2022_51_2_a0
ER  - 
%0 Journal Article
%A Braüner, Torben
%T Analytic Non-Labelled Proof-Systems for Hybrid Logic: Overview and a couple of striking facts
%J Bulletin of the Section of Logic
%D 2022
%P 143-162
%V 51
%N 2
%I mathdoc
%U http://geodesic.mathdoc.fr/item/BSL_2022_51_2_a0/
%G en
%F BSL_2022_51_2_a0
Braüner, Torben. Analytic Non-Labelled Proof-Systems for Hybrid Logic: Overview and a couple of striking facts. Bulletin of the Section of Logic, Tome 51 (2022) no. 2, pp. 143-162. http://geodesic.mathdoc.fr/item/BSL_2022_51_2_a0/

[1] M. Baaz, A. Leitsch, Methods of Cut-Elimination, vol. 34 of Trends in Logic Series, Springer, Dordrecht (2011) | DOI

[2] G. Bierman, V. de Paiva, On an Intuitionistic Modal Logic, Studia Logica, vol. 65 (2000), pp. 383–416 | DOI

[3] 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

[4] 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

[5] 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.

[6] T. Braüner, Hybrid Logic and its Proof-Theory, vol. 37 of Applied Logic Series, Springer, Dordrecht (2011) | DOI

[7] 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

[8] 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

[9] 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

[10] 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

[11] 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

[12] J.-Y. Girard, Linear Logic, Theoretical Computer Science, vol. 50(1) (1987), pp. 1–102 | DOI

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

[14] A. Indrzejczak, Natural Deduction, Hybrid Systems and Modal Logics, vol. 30 of Trends in Logic Series, Springer, Dordrecht (2010) | DOI

[15] 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

[16] 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

[17] D. Prawitz, Natural Deduction. A Proof-Theoretical Study, Almqvist and Wiksell, Stockholm (1965).

[18] 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

[19] 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.

[20] 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

[21] J. Seligman, Internalization: The Case of Hybrid Logics, Journal of Logic and Computation, vol. 11(5) (2001), pp. 671–689 | DOI

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

[23] 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