Intuitionistic Non-normal Modal Logics: A General Framework
- PDF / 1,516,163 Bytes
- 50 Pages / 439.642 x 666.49 pts Page_size
- 55 Downloads / 204 Views
Intuitionistic Non-normal Modal Logics: A General Framework Tiziano Dalmonte1
· Charles Grellois1
· Nicola Olivetti1
Received: 26 February 2019 / Accepted: 25 November 2019 / © Springer Nature B.V. 2020
Abstract We define a family of intuitionistic non-normal modal logics; they can be seen as intuitionistic counterparts of classical ones. We first consider monomodal logics, which contain only Necessity or Possibility. We then consider the more important case of bimodal logics, which contain both modal operators. In this case we define several interactions between Necessity and Possibility of increasing strength, although weaker than duality. We thereby obtain a lattice of 24 distinct bimodal logics. For all logics we provide both a Hilbert axiomatisation and a cut-free sequent calculus, on its basis we also prove their decidability. We then define a semantic characterisation of our logics in terms of neighbourhood models containing two distinct neighbourhood functions corresponding to the two modalities. Our semantic framework captures modularly not only our systems but also already known intuitionistic non-normal modal logics such as Constructive K (CK) and the propositional fragment of Wijesekera’s Constructive Concurrent Dynamic Logic. Keywords Intuitionistic logic · Non-normal modal logic · Neighbourhood semantics · Sequent calculi
This work was partially supported by the Project TICAMORE ANR-16-CE91-0002-01. Tiziano Dalmonte
[email protected] Charles Grellois [email protected] Nicola Olivetti [email protected] 1
Aix Marseille Univ, Universit´e de Toulon, CNRS, LIS, Marseille, France
T. Dalmonte et al.
1 Introduction Both intuitionistic modal logic and non-normal modal logic have been studied for a long time. The study of modalities with an intuitionistic basis goes back to Fitch in the late 40s [12] and has led to an important stream of research. We can very schematically identify two traditions: so-called intuitionistic modal logics versus constructive modal logics. Intuitionistic modal logics have been systematised by Simpson [35], whose main goal is to define an analogous of classical modalities justified from an intuitionistic point of view. On the other hand, constructive modal logics are mainly motivated by their applications to computer science, such as the type-theoretic interpretations (Curry–Howard correspondence, typed lambda calculi) [5], verification and knowledge representation,1 but also by their mathematical semantics (Goldblatt [17]). For both traditions proof methods have been intensively investigated, see for instance [14], [15], [19], [28], [36]. On the other hand, non-normal modal logics have been strongly motivated on a philosophical and epistemic ground. They are called “non-normal” as they do not satisfy all the axioms and rules of the minimal normal modal logic K. They have been studied since the seminal works of Scott, Montague, Lemmon, and Chellas ([6, 32, 34], see Pacuit [33] for a survey), and can be seen as generalisations of standar
Data Loading...
