5

Why is the combination of

impredicativity + excluded middle + large elimination

inconsistent in dependent type theory?

My understanding of large elimination is I am doing large elimination if I am eliminating an inductive type to build a type.

I am trying to learn more about large elimination and how large elimination interacts with other constructs like predicativity and EM. In particular, I would like to know whether such inconsistency can be derived in for example, the impredicative Prop in Coq when large elimination is allowed and if so, how it's derived.

NJay
  • 117
  • 6
Petercommand Hsu
  • 51
  • 2
  • I believe what you call "large elimination" is normally called "strong elimination". AFAIK the problem with it appears when you do a "strong elimination" of a "large inductive type", where the "large" refers to the fact that it's an inductive type where there is an impredicative quantification over Prop. But that inconsistency exists without any need for the excluded-middle, so maybe you're referring to something else? – Stefan Jun 20 '18 at 13:36
  • This may be a duplicate of https://cstheory.stackexchange.com/questions/40339/what-exactly-is-large-elimination, certainly it contains a reference to the answer to your question. – cody Jun 21 '18 at 11:23
  • 2
    @Stefan Hmm, so the reason why Prop with large elimination is inconsistent is because Prop is proof irrelevant in Coq according to https://github.com/FStarLang/FStar/issues/360 in cody's link. – Petercommand Hsu Jun 22 '18 at 20:39
  • @PetercommandHsu Yes, excluded middle implies proof irrelevance in impredicative prop. – cody Jun 25 '18 at 22:12

0 Answers0