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

https://hal.inria.fr/hal-00920224
Contributor : Olivier Hermant <>
Submitted on : Wednesday, December 18, 2013 - 9:15:29 AM
Last modification on : Tuesday, March 27, 2018 - 4:06:21 PM
Long-term archiving on : Wednesday, March 19, 2014 - 5:45:49 AM

File

main.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-00920224, version 1

Citation

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

Share

Metrics

Record views

31

Files downloads

16