On Intuitionistic Diamonds (and Lack Thereof)

Anupam Das; Sonia Marin

doi:10.1007/978-3-031-43513-3_16

On Intuitionistic Diamonds (and Lack Thereof)

Anupam Das, Sonia Marin^*

^*Corresponding author for this work

Computer Science

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Abstract

A variety of intuitionistic versions of modal logic $$ K $$ have been proposed in the literature. An apparent misconception is that all these logics coincide on their $$\Box $$ -only (or $$\Diamond $$ -free) fragment, suggesting some robustness of ‘ $$\Box $$ -only intuitionistic modal logic’. However in this work we show that this is not true, by consideration of negative translations from classical modal logic: Fischer Servi’s $$ IK $$ proves strictly more $$\Diamond $$ -free theorems than Fitch’s $$ CK $$, and indeed $$i K $$, the minimal $$\Box $$ -normal intuitionistic modal logic. On the other hand we show that the smallest extension of $$i K $$ by a normal $$\Diamond $$ is in fact conservative over $$i K $$ (over $$\Diamond $$ -free formulas). To this end, we develop a novel proof calculus based on nested sequents for intuitionistic propositional logic due to Fitting. Along the way we establish a number of new metalogical results.

Original language	English
Title of host publication	Automated Reasoning with Analytic Tableaux and Related Methods
Subtitle of host publication	32nd International Conference, TABLEAUX 2023, Prague, Czech Republic, September 18–21, 2023, Proceedings
Editors	Revantha Ramanayake, Josef Urban
Publisher	Springer
Pages	283-301
Number of pages	19
ISBN (Electronic)	9783031435133
ISBN (Print)	9783031435126
DOIs	https://doi.org/10.1007/978-3-031-43513-3_16
Publication status	Published - 14 Sept 2023
Event	32nd International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX 2023 - Prague, Czech Republic Duration: 18 Sept 2023 → 21 Sept 2023

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	14278 LNAI
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	32nd International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX 2023
Country/Territory	Czech Republic
City	Prague
Period	18/09/23 → 21/09/23

Bibliographical note

Funding Information:
The authors would like to thank The Proof Theory Blog community for all the feedback from their post [11]. In particular this work would not have been possible without several insightful interactions with Alex Simpson, Reuben Rowe, Nicola Olivetti, Tiziano Dalmonte, Dale Miller, Dominik Kirst, Iris van der Giessen, and Marianna Girlando. We thank Nicola Olivetti in particular for encouraging us to publish these results. This (alphabetically) first author was supported by a UKRI Future Leaders Fellowship, ‘Structure vs Invariants in Proofs’, project reference MR/S035540/1.

Funding Information:
This (alphabetically) first author was supported by a UKRI Future Leaders Fellowship, ‘Structure vs Invariants in Proofs’, project reference MR/S035540/1.

Publisher Copyright:
© 2023, The Author(s).

Keywords

Cut-elimination
Intuitionistic logic
Modal logic
Negative translation
Nested sequents
Proof theory

ASJC Scopus subject areas

Theoretical Computer Science
General Computer Science

Access to Document

10.1007/978-3-031-43513-3_16Licence: Creative Commons: Attribution (CC BY)

Cite this

Das, A., & Marin, S. (2023). On Intuitionistic Diamonds (and Lack Thereof). In R. Ramanayake, & J. Urban (Eds.), Automated Reasoning with Analytic Tableaux and Related Methods: 32nd International Conference, TABLEAUX 2023, Prague, Czech Republic, September 18–21, 2023, Proceedings (pp. 283-301). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 14278 LNAI). Springer. https://doi.org/10.1007/978-3-031-43513-3_16

Das, Anupam ; Marin, Sonia. / On Intuitionistic Diamonds (and Lack Thereof). Automated Reasoning with Analytic Tableaux and Related Methods: 32nd International Conference, TABLEAUX 2023, Prague, Czech Republic, September 18–21, 2023, Proceedings. editor / Revantha Ramanayake ; Josef Urban. Springer, 2023. pp. 283-301 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{5eaf87b9daba4b5eab07b6805bc821a0,

title = "On Intuitionistic Diamonds (and Lack Thereof)",

abstract = "A variety of intuitionistic versions of modal logic $$ K $$ have been proposed in the literature. An apparent misconception is that all these logics coincide on their $$\Box $$ -only (or $$\Diamond $$ -free) fragment, suggesting some robustness of {\textquoteleft} $$\Box $$ -only intuitionistic modal logic{\textquoteright}. However in this work we show that this is not true, by consideration of negative translations from classical modal logic: Fischer Servi{\textquoteright}s $$ IK $$ proves strictly more $$\Diamond $$ -free theorems than Fitch{\textquoteright}s $$ CK $$, and indeed $$i K $$, the minimal $$\Box $$ -normal intuitionistic modal logic. On the other hand we show that the smallest extension of $$i K $$ by a normal $$\Diamond $$ is in fact conservative over $$i K $$ (over $$\Diamond $$ -free formulas). To this end, we develop a novel proof calculus based on nested sequents for intuitionistic propositional logic due to Fitting. Along the way we establish a number of new metalogical results.",

keywords = "Cut-elimination, Intuitionistic logic, Modal logic, Negative translation, Nested sequents, Proof theory",

author = "Anupam Das and Sonia Marin",

note = "Funding Information: The authors would like to thank The Proof Theory Blog community for all the feedback from their post [11]. In particular this work would not have been possible without several insightful interactions with Alex Simpson, Reuben Rowe, Nicola Olivetti, Tiziano Dalmonte, Dale Miller, Dominik Kirst, Iris van der Giessen, and Marianna Girlando. We thank Nicola Olivetti in particular for encouraging us to publish these results. This (alphabetically) first author was supported by a UKRI Future Leaders Fellowship, {\textquoteleft}Structure vs Invariants in Proofs{\textquoteright}, project reference MR/S035540/1. Funding Information: This (alphabetically) first author was supported by a UKRI Future Leaders Fellowship, {\textquoteleft}Structure vs Invariants in Proofs{\textquoteright}, project reference MR/S035540/1. Publisher Copyright: {\textcopyright} 2023, The Author(s).; 32nd International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX 2023 ; Conference date: 18-09-2023 Through 21-09-2023",

year = "2023",

month = sep,

day = "14",

doi = "10.1007/978-3-031-43513-3_16",

language = "English",

isbn = "9783031435126",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer",

pages = "283--301",

editor = "Revantha Ramanayake and Josef Urban",

booktitle = "Automated Reasoning with Analytic Tableaux and Related Methods",

}

Das, A & Marin, S 2023, On Intuitionistic Diamonds (and Lack Thereof). in R Ramanayake & J Urban (eds), Automated Reasoning with Analytic Tableaux and Related Methods: 32nd International Conference, TABLEAUX 2023, Prague, Czech Republic, September 18–21, 2023, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 14278 LNAI, Springer, pp. 283-301, 32nd International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX 2023, Prague, Czech Republic, 18/09/23. https://doi.org/10.1007/978-3-031-43513-3_16

On Intuitionistic Diamonds (and Lack Thereof). / Das, Anupam ; Marin, Sonia.
Automated Reasoning with Analytic Tableaux and Related Methods: 32nd International Conference, TABLEAUX 2023, Prague, Czech Republic, September 18–21, 2023, Proceedings. ed. / Revantha Ramanayake; Josef Urban. Springer, 2023. p. 283-301 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 14278 LNAI).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

TY - GEN

T1 - On Intuitionistic Diamonds (and Lack Thereof)

AU - Das, Anupam

AU - Marin, Sonia

N1 - Funding Information: The authors would like to thank The Proof Theory Blog community for all the feedback from their post [11]. In particular this work would not have been possible without several insightful interactions with Alex Simpson, Reuben Rowe, Nicola Olivetti, Tiziano Dalmonte, Dale Miller, Dominik Kirst, Iris van der Giessen, and Marianna Girlando. We thank Nicola Olivetti in particular for encouraging us to publish these results. This (alphabetically) first author was supported by a UKRI Future Leaders Fellowship, ‘Structure vs Invariants in Proofs’, project reference MR/S035540/1. Funding Information: This (alphabetically) first author was supported by a UKRI Future Leaders Fellowship, ‘Structure vs Invariants in Proofs’, project reference MR/S035540/1. Publisher Copyright: © 2023, The Author(s).

PY - 2023/9/14

Y1 - 2023/9/14

N2 - A variety of intuitionistic versions of modal logic $$ K $$ have been proposed in the literature. An apparent misconception is that all these logics coincide on their $$\Box $$ -only (or $$\Diamond $$ -free) fragment, suggesting some robustness of ‘ $$\Box $$ -only intuitionistic modal logic’. However in this work we show that this is not true, by consideration of negative translations from classical modal logic: Fischer Servi’s $$ IK $$ proves strictly more $$\Diamond $$ -free theorems than Fitch’s $$ CK $$, and indeed $$i K $$, the minimal $$\Box $$ -normal intuitionistic modal logic. On the other hand we show that the smallest extension of $$i K $$ by a normal $$\Diamond $$ is in fact conservative over $$i K $$ (over $$\Diamond $$ -free formulas). To this end, we develop a novel proof calculus based on nested sequents for intuitionistic propositional logic due to Fitting. Along the way we establish a number of new metalogical results.

AB - A variety of intuitionistic versions of modal logic $$ K $$ have been proposed in the literature. An apparent misconception is that all these logics coincide on their $$\Box $$ -only (or $$\Diamond $$ -free) fragment, suggesting some robustness of ‘ $$\Box $$ -only intuitionistic modal logic’. However in this work we show that this is not true, by consideration of negative translations from classical modal logic: Fischer Servi’s $$ IK $$ proves strictly more $$\Diamond $$ -free theorems than Fitch’s $$ CK $$, and indeed $$i K $$, the minimal $$\Box $$ -normal intuitionistic modal logic. On the other hand we show that the smallest extension of $$i K $$ by a normal $$\Diamond $$ is in fact conservative over $$i K $$ (over $$\Diamond $$ -free formulas). To this end, we develop a novel proof calculus based on nested sequents for intuitionistic propositional logic due to Fitting. Along the way we establish a number of new metalogical results.

KW - Cut-elimination

KW - Intuitionistic logic

KW - Modal logic

KW - Negative translation

KW - Nested sequents

KW - Proof theory

UR - http://www.scopus.com/inward/record.url?scp=85172419995&partnerID=8YFLogxK

U2 - 10.1007/978-3-031-43513-3_16

DO - 10.1007/978-3-031-43513-3_16

M3 - Conference contribution

AN - SCOPUS:85172419995

SN - 9783031435126

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 283

EP - 301

BT - Automated Reasoning with Analytic Tableaux and Related Methods

A2 - Ramanayake, Revantha

A2 - Urban, Josef

PB - Springer

T2 - 32nd International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX 2023

Y2 - 18 September 2023 through 21 September 2023

ER -

Das A , Marin S. On Intuitionistic Diamonds (and Lack Thereof). In Ramanayake R, Urban J, editors, Automated Reasoning with Analytic Tableaux and Related Methods: 32nd International Conference, TABLEAUX 2023, Prague, Czech Republic, September 18–21, 2023, Proceedings. Springer. 2023. p. 283-301. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-031-43513-3_16

On Intuitionistic Diamonds (and Lack Thereof)

Abstract

Publication series

Conference

Bibliographical note

Keywords

ASJC Scopus subject areas

Access to Document

Fingerprint

Cite this