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 metadatas

Cited literature [18 references]  Display  Hide  Download

https://hal.inria.fr/hal-00920224
Contributor : Olivier Hermant <>
Submitted on : Wednesday, December 18, 2013 - 9:30:07 PM
Last modification on : Monday, November 12, 2018 - 11:01:30 AM
Long-term archiving on : Thursday, March 20, 2014 - 11:27:07 AM

Files

main.pdf
Files produced by the author(s)

Identifiers

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

Citation

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

Share

Metrics

Record views

444

Files downloads

211