Philippe Balbiani
CNRS researcher at Toulouse Institute of Computer Science Research (Toulouse, France)
Rooted in Intuitionistic and Constructive Reasoning, Intermediate Logics have found important applications through the Curry-Howard correspondence. Nowadays, there is an Intuitionistic Modal Logics renaissance in Computer Science and Artificial Intelligence. Connections between, on one hand, Intuitionistic and Constructive Mathematics and, on the other hand, Epistemic Reasoning have emerged through different applications. This renaissance in Intuitionistic and Constructive Reasoning constitute modern illustrations of the classical Brouwer-Heyting-Kolmogorov reading of the intuitionistic connectives: a proof of A&B consists of both a proof of A, and a proof of B, a proof of AvB consists of either a proof of A, or a proof of B, a proof of A->B consists of a procedure transforming any proof of A into a proof of B, etc. The notion of explanation is becoming more and more central in the recent development of logic, witness its increasing use within the context of automated systems deciding and learning on how to act. And undoubtedly, the classical Brouwer-Heyting-Kolmogorov reading can also be understood in terms of it: an explanation of A&B consists of both an explanation of A, and an explanation of B, an explanation of AvB consists of either an explanation of A, or an explanation of B, an explanation of A->B consists of a procedure transforming any explanation of A into an explanation of B, etc. Firstly, we will make a survey of the different Intuitionistic Modal Logics that can be found in the literature (especially what we know about them and what we do not know about them in terms of axiomatization/completeness and decidability/complexity), we will compare their currently known applications and we will study their proof theory as well as their relational semantics. Secondly, we will address some of the logical and computational aspects of the multifarious combinations of intuitionistic concepts and modal concepts that has been considered in the literature. And much remains to be done. For example, the complete axiomatization of many intuitionistic modal logics as well as their decidability status. This is especially true for what concerns the extensions of these intuitionistic modal logics by means of axioms coming from the modal cube. And thirdly, maybe the most promising aspects of intuitionistic modal logics seem to be those related to the interplay between explanations and knowledge. Replacing the above-mentioned classical Brouwer-Heyting-Kolmogorov reading of the intuitionistic connectives by a reading based on the notion of explanation, we plan to determine the relationships between the intuitionistic connectives and the modal connectives when the former ones are interpreted in terms of knowledge and belief. What is becoming of the principles of positive introspection and negative introspection in the intuitionistic and constructive setting? What is the right multiagent intuitionistic logic of knowledge?
Keywords: Explanations and reasoning, Intuitionistic modal logics, Epistemic logics, Proof theory and model theory, Axiomatization/completeness and decidability/complexity
Scientific area: Artificial Intelligence, Knowledge representation and reasoning, Logic and computation
Bio: Philippe Balbiani is a CNRS researcher at the Toulouse Institute of Computer Science Research (Toulouse, France). His research interests include the logical models of the dynamic aspects of communications in multi-agent systems as well as the development of qualitative models of reasoning about space and time.
Visiting period: June 10th – July 15th 2024 at Barcelona University, Department of Philosophy