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 in the intuitionistic versions (called N5c and N5i respectively), is designed to match as much as possible the structure and the properties of the standard system of natu- ral deduction for first-order logic, exploiting the formal analogy between modalities and quantifiers. We study a (syntactical) normalization the- orem for both N5c and N5i and its main consequences, the sub-formula principle and the consistency theorem. In particular, we propose an intu- itionistic encoding of classical S5 (via a suitable extension of the G ̈odel translation for first order classical logic). Moreover, via the BHK in- terpretation of intuitionistic proofs, we propose a suitable Curry–Howard isomorphism for N5i. By translation into the natural deduction system given by Galmiche and Salhi in [12], we prove the equivalence of N5i w.r.t. an Hilbert-style axiomatization of IS5. However, when considering the sheer provability of labeled formulas, our system is comparable to the one presented by Simpson in [35]. Nevertheless, it remains uncertain whether it is feasible to establish a translation between the corresponding derivations.