A Constructive Proof of Dependent Choice, Compatible with Classical Logic

被引：18
|
作者：
Herbelin, Hugo [1 ]
机构：
[1] Univ Paris Diderot, PPS, INRIA, Paris, France
来源：
2012 27TH ANNUAL ACM/IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE (LICS) | 2012年
关键词：
Dependent choice; classical logic; constructive logic; strong existential;
D O I：
10.1109/LICS.2012.47
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
Martin-Lof'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.
引用
收藏
页码：365 / 374
页数：10
相关论文
共 50 条
12345