Semantical Analysis of Intuitionistic Modal Logics between CK and IK
Fuente:
arXiv
Salvato in:
| Autori principali: | , , |
|---|---|
| Natura: | Preprint |
| Pubblicazione: |
2024
|
| Soggetti: | |
| Accesso online: | |
| Tags: |
Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
|
| _version_ | 1866915252753399808 |
|---|---|
| author | de Groot, Jim Shillito, Ian Clouston, Ranald |
| author_facet | de Groot, Jim Shillito, Ian Clouston, Ranald |
| contents | The intuitionistic modal logics considered between Constructive K (CK) and Intuitionistic K (IK) differ in their treatment of the possibility (diamond) connective. It was recently rediscovered that some logics between CK and IK also disagree on their diamond-free fragments, with only some remaining conservative over the standard axiomatisation of intuitionistic modal logic with necessity (box) alone. We show that relational Kripke semantics for CK can be extended with frame conditions for all axioms in the standard axiomatisation of IK, as well as other axioms previously studied. This allows us to answer open questions about the (non-)conservativity of such logics over intuitionistic modal logic without diamond. Our results are formalised using the Coq Proof Assistant. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2408_00262 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Semantical Analysis of Intuitionistic Modal Logics between CK and IK de Groot, Jim Shillito, Ian Clouston, Ranald Logic in Computer Science Logic The intuitionistic modal logics considered between Constructive K (CK) and Intuitionistic K (IK) differ in their treatment of the possibility (diamond) connective. It was recently rediscovered that some logics between CK and IK also disagree on their diamond-free fragments, with only some remaining conservative over the standard axiomatisation of intuitionistic modal logic with necessity (box) alone. We show that relational Kripke semantics for CK can be extended with frame conditions for all axioms in the standard axiomatisation of IK, as well as other axioms previously studied. This allows us to answer open questions about the (non-)conservativity of such logics over intuitionistic modal logic without diamond. Our results are formalised using the Coq Proof Assistant. |
| title | Semantical Analysis of Intuitionistic Modal Logics between CK and IK |
| topic | Logic in Computer Science Logic |
| url | https://arxiv.org/abs/2408.00262 |