Thoroughly Modal Hypersequents

May 5, 2026 COMING SOON

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 structural rules in a generalised sequent calculus setting. The talk ends with some gestures toward open problems and possible applications.

• The slides for the talk can be downloaded here.

• The talk is a presentation at the Laboratory for Foundations of Computer Science at the University of Edinburgh.