<p>Why is the combination of</p>

<p>impredicativity + excluded middle + large elimination</p>

<p>inconsistent in dependent type theory? </p>

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

<p>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.</p>

CC BY-SA 4.0
2018-06-20T13:36:14.997Z
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
CC BY-SA 4.0
2018-06-21T11:23:23.100Z
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
CC BY-SA 4.0
2018-06-22T20:39:08.593Z
@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
CC BY-SA 4.0
2018-06-25T22:12:29.083Z
@PetercommandHsu Yes, excluded middle implies proof irrelevance in impredicative prop.
cody
<type-theory><dependent-type>
What is the proof for the inconsistency of impredicativity + excluded middle + large elimination in type theory
Petercommand Hsu
# What is the proof for the inconsistency of impredicativity + excluded middle + large elimination in type theory

(Asked by: username_0 on 2018-06-19)

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.

**Tags:** type-theory, dependent-type

> **Comments:**
> **username_1**: 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?  
> **username_2**: 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.  
> **username_0**: @username_1 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 username_2's link.  
> **username_2**: @PetercommandHsu Yes, excluded middle implies proof irrelevance in impredicative prop.  

---

## 0 answers

