A hypersequent approach to modal logic

Andrew Parisi (University of Connecticut)

Several hypersequent accounts of modality have been presented (see Avron (1991); Restall (2009); Lellmann (2014); Lahav (2013)). This paper develops several hypersequent systems of modal logic. In particular systems K, D, T, S4, B, and S5 are given. S5 is the same hypersequent system given in Restall (2009). The other systems are generated from this by restricting the external structural rules of the calculus. In this sense, the calculi mirror the standard possible world account of modality: the different systems are generated by restricting structural features modal frames as opposed to the rules explicitly governing the modal operators. Cut Elimination has been proved for K and D, and Cut admissibility for S5 is proved by Restall (2009). The paper concludes by considering the results of adding different accounts of first-order quantification to the calculus.