A Constructive Proof of Dependent Choice, Compatible with Classical Logic

Hugo Herbelin 1, 2
2 PI.R2 - Design, study and implementation of languages for proofs and programs
PPS - Preuves, Programmes et Systèmes, Inria Paris-Rocquencourt, UPD7 - Université Paris Diderot - Paris 7, CNRS - Centre National de la Recherche Scientifique : UMR7126
Abstract : Martin-Löf's type theory has strong existential elimination (dependent sum type) that allows to prove the full axiom of choice. However the theory is intuitionistic. We give a condition on strong existential elimination that makes it computationally compatible with classical logic. With this restriction, we lose the full axiom of choice but, thanks to a lazily-evaluated coinductive representation of quantification, we are still able to constructively prove the axiom of countable choice, the axiom of dependent choice, and a form of bar induction in ways that make each of them computationally compatible with classical logic.
Type de document :
Communication dans un congrès
LICS 2012 - 27th Annual ACM/IEEE Symposium on Logic in Computer Science, Jun 2012, Dubrovnik, Croatia. IEEE Computer Society, pp.365-374, 2012, Proceedings of the 27th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2012, 25-28 June 2012, Dubrovnik, Croatia
Liste complète des métadonnées

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

https://hal.inria.fr/hal-00697240
Contributeur : Hugo Herbelin <>
Soumis le : mardi 15 mai 2012 - 03:23:13
Dernière modification le : vendredi 25 mai 2018 - 12:02:06
Document(s) archivé(s) le : jeudi 15 décembre 2016 - 09:50:35

Fichier

Herbelin-lics12.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-00697240, version 1

Collections

INRIA | PPS | USPC

Citation

Hugo Herbelin. A Constructive Proof of Dependent Choice, Compatible with Classical Logic. LICS 2012 - 27th Annual ACM/IEEE Symposium on Logic in Computer Science, Jun 2012, Dubrovnik, Croatia. IEEE Computer Society, pp.365-374, 2012, Proceedings of the 27th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2012, 25-28 June 2012, Dubrovnik, Croatia. 〈hal-00697240〉

Partager

Métriques

Consultations de la notice

208

Téléchargements de fichiers

173