Thoroughly Modal Hypersequents

Abstract: In this talk I will introduce a simple hypersequent calculus for the propositional modal logic S5, explaining how this representation encodes a natural form of reasoning about possibility and necessity. I then explain how the familiar structural rules of contraction and weakening take two forms in such a hypersequent calculus: they operate inside sequents, as familiar in substructural logics (linear logic, relevant logics, affine logic, etc.), but they also take an outer form, governing weakening or contraction of zones in a sequent. This motivates the formulation of a thoroughly linear hypersequent modal logic, in which we do without both inner and outer forms of contraction and weakening. This results in a novel modal logic, with a cut-free hypersequent calculus giving a straightforward decision procedure. Simple models (algebras) can be used to show how the logic differs from classical S5. These results help us understand the relationship between operational rules and…