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.

  • $\begingroup$ 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? $\endgroup$
    – Stefan
    Jun 20, 2018 at 13:36
  • $\begingroup$ This may be a duplicate of cstheory.stackexchange.com/questions/40339/…, certainly it contains a reference to the answer to your question. $\endgroup$
    – cody
    Jun 21, 2018 at 11:23
  • 2
    $\begingroup$ @Stefan Hmm, so the reason why Prop with large elimination is inconsistent is because Prop is proof irrelevant in Coq according to github.com/FStarLang/FStar/issues/360 in cody's link. $\endgroup$ Jun 22, 2018 at 20:39
  • $\begingroup$ @PetercommandHsu Yes, excluded middle implies proof irrelevance in impredicative prop. $\endgroup$
    – cody
    Jun 25, 2018 at 22:12


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Browse other questions tagged or ask your own question.