Search

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 N 5 c and N 5 i 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 N 5 c and N 5 i 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 BHK interpretation of intuitionistic proofs, we propose a suitable Curry–Howard isomorphism for N 5 i . 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.), Logic for programming, artificial intelligence, and reasoning (pp. 255–271). Springer Berlin Heidelberg.], we prove the equivalence of N 5 i 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 theory and 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. [ABSTRACT FROM AUTHOR]