A deep inference system for the modal logic S5 (Q2642520)

In this paper a cut-admissibility system for modal logic S5 in the calculus of structures is presented. This system makes an explicit and intensive use of deep inference and it satisfies important properties with respect to their modal rules such as \textit{systemacity} (a technique for formulating the modal rules out of the modal axioms) and \textit{modularity} (every axiom corresponds to a finite number of rules). The system for S5 offered in the paper is a conservative extension for S4 presented by \textit{C. Stewart} and \textit{P. Stouppa} [``A systematic proof theory for several modal logics'', in: R. Schmidt et al. (eds.), Advances in modal logic. Vol. 5. Selected papers from the 5th conference (AiML 2004), Manchester, UK, September 9--11, 2004. London: King's College Publications. 309--333 (2005; Zbl 1107.03016)] with rules corresponding to axiom 5. Another remarkable feature of the system is that it has few rules and enjoys a direct way of formalizing the modal rules out their axioms. Moreover, the applications of these rules can be restricted so that they affect only a bounded portion of the data structures and, as a consequence, there is a bounded computational cost for rule applications.