On Nested Sequents for Constructive Modal Logics

TL;DR

This paper develops nested sequent systems for constructive modal logics derived from CK with additional axioms, providing a syntactic proof of cut elimination for these systems.

Contribution

It introduces nested sequent calculi for constructive modal logics with various axioms and proves cut elimination syntactically, extending the proof theory of constructive modal logic.

Findings

Nested sequent systems for constructive modal logics are established.

Cut elimination is proven syntactically for these systems.

The approach covers variants like constructive K4, S4, and S5.

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.