On nested sequents for constructive modal logics

DOI10.2168/LMCS-11(3:7)2015zbMATH Open1347.03038arXiv1505.06896MaRDI QIDQ3196338FDOQ3196338

Authors: Ryuta Arisaka, Anupam Das, Lutz Straßburger 

Publication date: 29 October 2015

Published in: Logical Methods in Computer Science (Search for Journal in Brave)

Abstract: We present deductive systems for various modal logics that can be obtained from the constructive variant of the normal modal logic CK by adding combinations of the axioms d, t, b, 4, and 5. This includes the constructive variants of the standard modal logics K4, S4, and S5. We use for our presentation the formalism of nested sequents and give a syntactic proof of cut elimination.

Full work available at URL: https://arxiv.org/abs/1505.06896

Recommendations

• Cut elimination in nested sequents for intuitionistic modal logics
• Modular sequent systems for modal logic
• Proof theory for indexed nested sequents
• Label-free modular systems for classical and intuitionistic modal logics
• Constructive modal logics. I

zbMATH Keywords

intuitionistic logicmodal logiccut-eliminationnested sequents

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Cut-elimination and normal-form theorems (03F05) Subsystems of classical logic (including intuitionistic logic) (03B20)

Cited In (30)

• Proof theory for indexed nested sequents
• Dual and axiomatic systems for constructive S4, a formally verified equivalence
• Axiomatic and dual systems for constructive necessity, a formally verified equivalence
• Maehara-style modal nested calculi
• Nested sequents for intuitionistic logics
• Nested sequent calculi for normal conditional logics
• Title not available (Why is that?)
• The Došen square under construction: a tale of four modalities
• Grafting hypersequents onto nested sequents
• Linear Nested Sequents, 2-Sequents and Hypersequents
• Nested sequents for intuitionistic modal logics via structural refinement
• Terminating calculi and countermodels for constructive modal logics
• Wijesekera-style constructive modal logics
• Combining monotone and normal modal logic in nested sequents -- with countermodels
• Modular sequent systems for modal logic
• Prefixed tableaus and nested sequents
• MOIN: A Nested Sequent Theorem Prover for Intuitionistic Modal Logics (System Description)
• Cut-free Gentzen calculus for multimodal CK
• Intuitionistic non-normal modal logics: a general framework
• Title not available (Why is that?)
• Nested sequents for provability logic GLP: FIG. 1.
• Constructive modal logics. I
• A modal logic for discretely descending chains of sets
• The principle of reflection via nested sequents
• From 2-sequents and linear nested sequents to natural deduction for normal modal logics
• Embedding constructive K into intuitionistic K
• On intuitionistic diamonds (and lack thereof)
• Realization theorems for justification logics: full modularity
• Cut elimination in nested sequents for intuitionistic modal logics
• Title not available (Why is that?)

This page was built for publication: On nested sequents for constructive modal logics

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3196338)