Rea Golan

Proof theorists have long been struggling to provide simple accounts of various modal logics. Drawing on the recent literature on metainferences, I develop in the present paper a novel approach to this challenge: regular sequent systems augmented with natural deduction-like rules for assuming and discharging sequents. Based on this approach, I introduce an elegant calculus for the modal logic. Various discharging conditions on assumptions are shown to yield the weaker logics, and. The rules in these calculi have attractive proof-theoretic properties: they are explicit, symmetrical, and non-circular, and they enjoy the subformula property.