Natural deduction calculi for classical and intuitionistic S5

We propose an indexed natural deduction system for the modal logic S5, ideally following Wansing’s previous work in the context of tableaux sequents. The system, given both in the classical and intuitionistic versions (called Nc5 and Ni5 respectively), is designed to match as much as possible the structure and properties of the standard system of natural deduction for first-order logic, exploiting the formal analogy between modalities and quantifiers. We study a (syntactical) normalization theorem for both Nc5 and Ni5 and its main consequences, the sub-formula principle and the consistency theorem. In particular, we propose an intuitionistic encoding of classical S5(via a suitable extension of the Gödel translation for first-order classical logic). Moreover, via the BHKinterpretation of intuitionistic proofs, we propose a suitable Curry–Howard isomorphism for Ni5. By translation into the natural deduction system given by Galmiche and Salhi in [(2010b). Label-free proof systems for intuitionistic modal logic is5. In E. M. Clarke & A. Voronkov (Eds.), Logicfor programming, artificial intelligence, and reasoning(pp. 255–271). Springer Berlin Heidelberg.], we prove the equivalence of Ni5 w.r.t. an Hilbert-style axiomatization of IS5. However, when considering the sheer provability of labelled formulas, our system is comparable to the one presented by Simpson in [(1993). The proof theoryand semantics of intuitionistic modal logic [PhD thesis], University of Edinburgh, UK.]. Nevertheless, it remains uncertain whether it is feasible to establish a translation between the corresponding derivations.