Label-free Modular Systems for Classical and Intuitionistic Modal Logics
Sonia Marin, Lutz Straßburger · 2014
In this paper we show for each of the modal axioms d, t, b, 4, and 5 an equivalent set of inference rules in a nested sequent system, such that, when added to the basic system for the modal logic K, the resulting system admits cut elimination. Then we show the same result also for intuitionistic modal logic. We achieve this by combining structural and logical rules.