Skip to Main content Skip to Navigation
New interface
Conference papers

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

Cited literature [30 references]  Display  Hide  Download
Contributor : Hugo Herbelin Connect in order to contact the contributor
Submitted on : Tuesday, May 15, 2012 - 3:23:13 AM
Last modification on : Friday, January 21, 2022 - 3:21:15 AM
Long-term archiving on: : Thursday, December 15, 2016 - 9:50:35 AM


Files produced by the author(s)


  • HAL Id : hal-00697240, version 1



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. pp.365-374. ⟨hal-00697240⟩



Record views


Files downloads