Classical polarizations yield double-negation translations

Zakaria Chihani 1 Danko Ilik 1 Dale Miller 1
1 PARSIFAL - Proof search and reasoning with logic specifications
LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau], Inria Saclay - Ile de France
Abstract : Double-negation translations map formulas to formulas in such a way that if a formula is a classical theorem then its translation is an intuitionistic theorem. We shall go beyond just examining provability by looking at correspondences between inference rules in classical proofs and in intuitionistic proofs of translated formulas. In order to make this comparison interesting and precise, we will examine focused versions of proofs in classical and intuitionistic logics using the LKF and LJF proof systems. We shall show that for a number of known double-negation translations, one can get essentially identical (focused) intuitionistic proofs as (focused) classical proofs. Thus the choice of a common double-negation translation is really the same choice as a polarization of classical logic (of which there are many).
Type de document :
Pré-publication, Document de travail
2016
Liste complète des métadonnées

Littérature citée [9 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01354298
Contributeur : Danko Ilik <>
Soumis le : jeudi 18 août 2016 - 13:25:46
Dernière modification le : mercredi 14 novembre 2018 - 16:14:01
Document(s) archivé(s) le : samedi 19 novembre 2016 - 20:03:20

Fichier

main.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-01354298, version 1

Citation

Zakaria Chihani, Danko Ilik, Dale Miller. Classical polarizations yield double-negation translations. 2016. 〈hal-01354298〉

Partager

Métriques

Consultations de la notice

397

Téléchargements de fichiers

63