Skip to Main content Skip to Navigation
New interface
Conference papers

Polarizing Double Negation Translations

Abstract : 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 formulae 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.
Document type :
Conference papers
Complete list of metadata

Cited literature [18 references]  Display  Hide  Download
Contributor : Olivier Hermant Connect in order to contact the contributor
Submitted on : Wednesday, December 18, 2013 - 9:30:07 PM
Last modification on : Tuesday, October 25, 2022 - 4:24:10 PM
Long-term archiving on: : Thursday, March 20, 2014 - 11:27:07 AM


Files produced by the author(s)


  • HAL Id : hal-00920224, version 2
  • ARXIV : 1312.5420


Mélanie Boudard, Olivier Hermant. Polarizing Double Negation Translations. LPAR, Dec 2013, Stellenbosch, South Africa. pp.182-197. ⟨hal-00920224v2⟩



Record views


Files downloads