Double-negation translations are used to encode and decode classical proofs in intuitionistic logic. We show that, in the cut-free fragment, we can simplify the translations and introduce fewer negations. To achieve this, we consider the polarization of the formulæ and adapt those translation to the different connectives and quantifiers.We show that the embedding results still hold, using a customized version of the focused classical sequent calculus. We also prove the latter equivalent to more usual versions of the sequent calculus. This polarization process allows lighter embeddings, and sheds some light on the relationship between intuitionistic and classical connectives. © Springer-Verlag 2013.
CITATION STYLE
Boudard, M., & Hermant, O. (2013). Polarizing double-negation translations. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 8312 LNCS, pp. 182–197). https://doi.org/10.1007/978-3-642-45221-5_14
Mendeley helps you to discover research relevant for your work.