On nested sequents for constructive modal logics

DOI10.2168/LMCS-11(3:7)2015MaRDI QIDQ3196338zbMATH OpenFDO

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)

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

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)

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.

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

Cited in

(30)

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

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)