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.

Natural deduction calculi for classical and intuitionistic S5

Andrea Masini;Margherita Zorzi
2023-01-01

Abstract

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.
2023
Proof Theory, Modal logic, Natural Deduction, Deductive Sisyems
File in questo prodotto:
File Dimensione Formato  
Natural deduction calculi for classical and intuitionistic S5-2.pdf

accesso aperto

Licenza: Non specificato
Dimensione 3.1 MB
Formato Adobe PDF
3.1 MB Adobe PDF Visualizza/Apri

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11562/1098986
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus ND
  • ???jsp.display-item.citation.isi??? ND
social impact