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 metadatas

Cited literature [30 references]  Display  Hide  Download

https://hal.inria.fr/hal-00697240
Contributor : Hugo Herbelin <>
Submitted on : Tuesday, May 15, 2012 - 3:23:13 AM
Last modification on : Friday, January 4, 2019 - 5:33:25 PM
Long-term archiving on : Thursday, December 15, 2016 - 9:50:35 AM

File

Herbelin-lics12.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-00697240, version 1

Collections

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

Share

Metrics

Record views

244

Files downloads

319