Playing with Modalities (Invited Talk)

Authors Elaine Pimentel , Carlos Olarte , Timo Lang , Robert Freiman , Christian G. Fermüller



PDF
Thumbnail PDF

File

LIPIcs.CSL.2025.4.pdf
  • Filesize: 1.03 MB
  • 20 pages

Document Identifiers

Author Details

Elaine Pimentel
  • Computer Science Department, University College London, UK
Carlos Olarte
  • LIPN, CNRS UMR 7030, Université Sorbonne Paris Nord, France
Timo Lang
  • Computer Science Department, University College London, UK
Robert Freiman
  • TU Wien, Austria
Christian G. Fermüller
  • TU Wien, Austria

Cite As Get BibTex

Elaine Pimentel, Carlos Olarte, Timo Lang, Robert Freiman, and Christian G. Fermüller. Playing with Modalities (Invited Talk). In 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 326, pp. 4:1-4:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.CSL.2025.4

Abstract

In this work, we will explore modalities through dialogical game lenses. Games provide a powerful tool for bridging the gap between intended and formal semantics, often offering a more conceptually natural approach to logic than traditional model-theoretic semantics.
We begin by exploring substructural calculi from a game semantic perspective, driven by intuitions about resource-consciousness and, more specifically, cost-sensitive reasoning. The game comes into full swing as we introduce cost labels to assumptions and a corresponding budget. Different proofs of the same end-sequent are interpreted as strategies for a player to defend a claim, which vary in cost. This leads to a labelled calculus, which can be viewed as a fragment of subexponential linear logic. We conclude this first part with a discussion of cut-admissibility for the proposed system. 
In the second part, we show that our games offer an interesting insight also into modal logics. More precisely, we will focus on the modal logic PNL, characterised by Kripke frames with two types of disjoint and symmetric reachability relations. This framework is motivated by the study of group polarisation, where the opinions or beliefs of individuals within a group become more extreme or polarised after interaction. Our approach to reasoning about group polarisation is based on PNL and highlights a different aspect of formal reasoning about the corresponding models - using games and proof systems. We conclude by outlining potential directions for future research.

Subject Classification

ACM Subject Classification
  • Theory of computation → Linear logic
  • Theory of computation → Modal and temporal logics
  • Theory of computation → Proof theory
Keywords
  • Linear logic
  • modal logic
  • proof theory
  • game semantics

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads

References

  1. Samson Abramsky and Paul-André Melliès. Concurrent games and full completeness. In 14th Annual IEEE Symposium on Logic in Computer Science, Trento, Italy, July 2-5, 1999, pages 431-442. IEEE Computer Society, 1999. URL: https://doi.org/10.1109/LICS.1999.782638.
  2. Beniamino Accattoli, Stéphane Graham-Lengrand, and Delia Kesner. Tight typings and split bounds, fully developed. J. Funct. Program., 30:e14, 2020. URL: https://doi.org/10.1017/S095679682000012X.
  3. Matteo Acclavio and Davide Catta. Lorenzen-style strategies as proof-search strategies. In Vadim Malvone and Aniello Murano, editors, EUMAS 2023, volume 14282 of LNCS, pages 150-166. Springer, 2023. URL: https://doi.org/10.1007/978-3-031-43264-4_10.
  4. Matteo Acclavio, Davide Catta, and Lutz Straßburger. Game semantics for constructive modal logic. In Anupam Das and Sara Negri, editors, TABLEAUX, volume 12842 of Lecture Notes in Computer Science, pages 428-445. Springer, 2021. URL: https://doi.org/10.1007/978-3-030-86059-2_25.
  5. Jean-Marc Andreoli. Logic programming with focusing proofs in linear logic. J. Log. Comput., 2(3):297-347, 1992. URL: https://doi.org/10.1093/LOGCOM/2.3.297.
  6. Carlos Areces, Raul Fervari, and Guillaume Hoffmann. Relation-changing modal operators. Log. J. IGPL, 23(4):601-627, 2015. URL: https://doi.org/10.1093/JIGPAL/JZV020.
  7. Guillaume Aucher, Johan van Benthem, and Davide Grossi. Modal logics of sabotage revisited. J. Log. Comput., 28(2):269-303, 2018. URL: https://doi.org/10.1093/LOGCOM/EXX034.
  8. Gavin M. Bierman and Valeria de Paiva. On an intuitionistic modal logic. Stud Logica, 65(3):383-416, 2000. URL: https://doi.org/10.1023/A:1005291931660.
  9. Patrick Blackburn. Modal logic as dialogical logic. Synthese, 127:57-93, 2001. URL: https://doi.org/10.1023/A:1010358017657.
  10. Patrick Blackburn and Jerry Seligman. Hybrid languages. J. Log. Lang. Inf., 4(3):251-272, 1995. URL: https://doi.org/10.1007/BF01049415.
  11. Torben Braüner. Hybrid logic and its proof-theory, volume 37. Springer Science & Business Media, 2010. URL: https://doi.org/10.1007/978-94-007-0002-4.
  12. Torben Braüner and Valeria de Paiva. Intuitionistic hybrid logic. J. Appl. Log., 4(3):231-255, 2006. URL: https://doi.org/10.1016/J.JAL.2005.06.009.
  13. Simon Castellan, Pierre Clairambault, Silvain Rideau, and Glynn Winskel. Games and strategies as event structures. Log. Methods Comput. Sci., 13(3), 2017. URL: https://doi.org/10.23638/LMCS-13(3:35)2017.
  14. Vincent Danos, Jean-Baptiste Joinet, and Harold Schellinx. The structure of exponentials: Uncovering the dynamics of linear logic proofs. In Georg Gottlob, Alexander Leitsch, and Daniele Mundici, editors, KGC, volume 713 of Lecture Notes in Computer Science, pages 159-171. Springer, 1993. URL: https://doi.org/10.1007/BFB0022564.
  15. Claudia Faggian and François Maurel. Ludics nets, a game model of concurrent interaction. In LICS, pages 376-385. IEEE Computer Society, 2005. URL: https://doi.org/10.1109/LICS.2005.25.
  16. Christian G. Fermüller and Timo Lang. Interpreting sequent calculi as client-server games. In Renate A. Schmidt and Cláudia Nalon, editors, TABLEAUX, volume 10501 of LNCS, pages 98-113. Springer, 2017. URL: https://doi.org/10.1007/978-3-319-66902-1_6.
  17. F. B. Fitch. Intuitionistic modal logic with quantifiers. Portugaliae Mathematicae, 7:113-118, 1948. URL: https://doi.org/doi:10.2307/2269275.
  18. Robert Freiman. Games for hybrid logic - from semantic games to analytic calculi. In Alexandra Silva, Renata Wassermann, and Ruy J. G. B. de Queiroz, editors, WoLLIC 2021, volume 13038 of LNCS, pages 133-149. Springer, 2021. URL: https://doi.org/10.1007/978-3-030-88853-4_9.
  19. Robert Freiman. From Semantic Games to Analytic Calculi. PhD thesis, Technische Universität Wien, 2024. Google Scholar
  20. Robert Freiman and Michael Bernreiter. Truth and preferences - A game approach for qualitative choice logic. In Sarah A. Gaggl, Maria V. Martinez, and Magdalena Ortiz, editors, JELIA, volume 14281 of LNCS, pages 547-560. Springer, 2023. URL: https://doi.org/10.1007/978-3-031-43619-2_37.
  21. Robert Freiman and Michael Bernreiter. Validity in choice logics - A game-theoretic investigation. In Helle Hvid Hansen, Andre Scedrov, and Ruy J. G. B. de Queiroz, editors, WoLLIC 2023, volume 13923 of LNCS, pages 211-226. Springer, 2023. URL: https://doi.org/10.1007/978-3-031-39784-4_13.
  22. Robert Freiman, Carlos Olarte, Elaine Pimentel, and Christian Fermüller. Reasoning about group polarization: From semantic games to sequent systems. In Nikolaj Bjorner, Marijn Heule, and Andrei Voronkov, editors, LPAR, volume 100 of EPiC Series in Computing, pages 70-87. EasyChair, 2024. URL: https://doi.org/10.29007/wptz.
  23. Robert Freiman, Carlos Olarte, Elaine Pimentel, and Christian G. Fermüller. Reasoning about group polarization: From semantic games to sequent systems. Technical report and tool available at https://github.com/promueva/PNL-game.git, 2024.
  24. Jean-Yves Girard. Linear logic. Theor. Comput. Sci., 50:1-102, 1987. URL: https://doi.org/10.1016/0304-3975(87)90045-4.
  25. Jaakko Hintikka. Logic, language-games and information, Kantian themes in the philosophy of logic. Revue Philosophique de la France Et de l'Etranger, 163:477-478, 1973. Google Scholar
  26. J. M. E. Hyland and C.-H. Luke Ong. On full abstraction for PCF: i, ii, and III. Inf. Comput., 163(2):285-408, 2000. URL: https://doi.org/10.1006/INCO.2000.2917.
  27. Timo Lang. Games, modalities and analytic proofs in nonclassical logics. PhD thesis, Technische Universität Wien, 2021. URL: https://doi.org/10.34726/hss.2021.92047.
  28. Timo Lang, Carlos Olarte, Elaine Pimentel, and Christian G. Fermüller. A game model for proofs with costs. In Serenella Cerrito and Andrei Popescu, editors, TABLEAUX, volume 11714 of LNCS, pages 241-258. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-29026-9_14.
  29. Paul Lorenzen and Kuno Lorenz, editors. Dialogische Logik. Wissenschaftliche Buchgesellschaft, [Abt. Verl.], Darmstadt, 1978. Google Scholar
  30. Sonia Marin, Dale Miller, Elaine Pimentel, and Marco Volpe. From axioms to synthetic inference rules via focusing. Ann. Pure Appl. Log., 173(5):103091, 2022. URL: https://doi.org/10.1016/j.apal.2022.103091.
  31. Sara Negri. Proof analysis in modal logic. J. Philosophical Logic, 34(5-6):507-544, 2005. URL: https://doi.org/10.1007/s10992-005-2267-3.
  32. Vivek Nigam and Dale Miller. Algorithmic specifications in linear logic with subexponentials. In António Porto and Francisco Javier López-Fraguas, editors, PPDP, pages 129-140. ACM, 2009. URL: https://doi.org/10.1145/1599410.1599427.
  33. Vivek Nigam and Dale Miller. A framework for proof systems. J. Autom. Reason., 45(2):157-188, 2010. URL: https://doi.org/10.1007/S10817-010-9182-1.
  34. Catarina Dutilh Novaes and Rohan French. Paradoxes and structural rules from a dialogue perspective. Philosophical Issues, 28:129-158, 2018. URL: https://doi.org/10.1111/phis.12119.
  35. Mina Young Pedersen, Sonja Smets, and Thomas Ågotnes. Modal logics and group polarization. J. Log. Comput., 31(8):2240-2269, 2021. URL: https://doi.org/10.1093/logcom/exab062.
  36. Elise Perrotin and Fernando R. Velázquez-Quesada. A semantic approach to non-prioritized belief revision. Log. J. IGPL, 29(4):644-671, 2021. URL: https://doi.org/10.1093/JIGPAL/JZZ045.
  37. Elaine Pimentel, Carlos Olarte, and Vivek Nigam. Process-as-formula interpretation: A substructural multimodal view (invited talk). In Naoki Kobayashi, editor, FSCD, volume 195 of LIPIcs, pages 3:1-3:21. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. URL: https://doi.org/10.4230/LIPICS.FSCD.2021.3.
  38. Gordon D. Plotkin and Colin P. Stirling. A framework for intuitionistic modal logic. In J. Y. Halpern, editor, 1st Conference on Theoretical Aspects of Reasoning About Knowledge. Morgan Kaufmann, 1986. URL: https://doi.org/10.2307/2274559.
  39. Alex K. Simpson. The Proof Theory and Semantics of Intuitionistic Modal Logic. PhD thesis, College of Science and Engineering, School of Informatics, University of Edinburgh, 1994. Google Scholar
  40. Lutz Straßburger. MELL in the calculus of structures. Theor. Comput. Sci., 309(1-3):213-285, 2003. URL: https://doi.org/10.1016/S0304-3975(03)00240-8.
  41. Lutz Straßburger and Alessio Guglielmi. A system of interaction and structure IV: the exponentials and decomposition. ACM Trans. Comput. Log., 12(4):23:1-23:39, 2011. URL: https://doi.org/10.1145/1970398.1970399.
  42. Johan van Benthem, Sujata Ghosh, and Fenrong Liu. Modelling simultaneous games in dynamic logic. Synth., 165(2):247-268, 2008. URL: https://doi.org/10.1007/S11229-008-9390-Y.
  43. Johan van Benthem, Lei Li, Chenwei Shi, and Haoxuan Yin. Hybrid sabotage modal logic. J. Log. Comput., 33(6):1216-1242, 2023. URL: https://doi.org/10.1093/LOGCOM/EXAC006.
  44. Fernando R. Velázquez-Quesada. Reliability-based preference dynamics: lexicographic upgrade. J. Log. Comput., 27(8):2341-2381, 2017. URL: https://doi.org/10.1093/LOGCOM/EXX019.
  45. Luca Viganò. Labelled Non-Classical Logics. Kluwer Academic Publishers, 2000. Google Scholar
  46. Bruno Xavier, Carlos Olarte, and Elaine Pimentel. A linear logic framework for multimodal logics. Math. Struct. Comput. Sci., 32(9):1176-1204, 2022. URL: https://doi.org/10.1017/S0960129522000366.
  47. Zuojun Xiong and Thomas Ågotnes. On the logic of balance in social networks. J. Log. Lang. Inf., 29(1):53-75, 2020. URL: https://doi.org/10.1007/S10849-019-09297-0.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail