Gentzen-type sequent calculus for modal logic S5

Abstract We consider a Gentzen-type cut-free sequent calculus GS5 for the modal logic S5 with a restriction on backward applications of modal rule $(\Box \Rightarrow )$. Using Schütte’s method of reduction trees, we prove that the calculus is complete for S5. We also prove that all rules are invertible and the cut rule is admissible in the calculus. We show that any backward proof search terminates, obtaining a decision procedure for S5 using the introduced calculus GS5.