Abstract

This thesis surveys and examines hypersequent approaches to the proof theory of modal logics. Traditional sequent calculi for modal logics often fail to have many of the desirable properties that we expect of a sequent calculus. Cut cannot be eliminated from the system for S5, the axioms of each logic are not straightforwardly related to the sequent rules, and variation between modal sequent calculi occurs in the presence and absence of logical rules, rather than structural rules, which violates Došen’s principle. The hypersequent framework is beneficial as we can provide Cut-free complete treatments of many modal logics. However, hypersequent approaches often lack generality, or do not conform to Došen’s principle. A recent development in the proof theory of modal logics, called relational hypersequents, appears to overcome many of these issues. Relational hypersequents provide a unified proof theory for many modal logics, where the logical rules are held constant between modal systems. This thesis provides some preliminary results for relational hypersequents by providing a Cut-free completeness proof for the modal logic K.