Setup
Current Understanding
I've recently been trying to learn about the interaction of Impredicative Polymorphism, Large Elimination and Excluded Middle (notably, inconsistency). Notably, this is broken down into two implications:
- Impredicative polymorphism + Excluded Middle $\to$ Proof Irrelevance
- Proof Irrelevance + Large elimination $\to \bot$
Unfortunately, I'm not quite up to speed on all the formal intricacies, but I'll try my best to get the good definitions:
For Impredicative polymorphism + Excluded middle, I am going off of the Coq formalisation of Berardi's paradox. By my understanding, this uses the following definitions:
A universe $U$ is impredicative when it contains quantifications such as dependent product whose domains do not live in $U$. The judgement therefore looks like:
$$ \frac {\Gamma, x : A \vdash B : U} {\prod_{x:A}B : U} $$
There could be additional limitations on what $A$ may be, but they must allow at least a case like $A = U$ to be considered impredicative. Sometimes this is the only such case, giving the rule:
$$ \frac {\Gamma, X : U \vdash B : U} {\prod_{X:U}B : U} $$ A universe further has excluded middle holds for a if the following type is inhabited:
$$ \prod_{A:U}A\lor \lnot A $$
My understanding of the proof irrelevance then implied is that the following type is also inhabited (assuming some propositional equality type $=$):
$$ \prod_{A:U} \prod_{x,y:A}x = y $$
i.e. for any two propositions x, y of type A, we have x = y.
Finally large elimination (also called strong elimination?) my understanding much less formal, but basically if you have some notion of inductive types (e.g. W-types), then strong/large elimination is the ability to construct inhabitants of some universe $U_i$ by pattern-matching on the value, e.g. one might be able to construct the function:
toProp : Bool -> U
toProp b = case b of
True -> Unit
False -> Empty
New Data
However, I have also recently learned about the idea of restricting excluded middle to only mere propositions, i.e. we first introduce a predicate on types, mereprop, which is true when we can show that for any two elements of that type, they are equal.
$$ \text{mereProp } P := \prod _{x,y:P}(x= y) $$
Then, restrict Excluded Middle(EM) to only those types which are mere propositions, i.e. $$ EM := \prod_{A:\mathcal U}(\text{mereProp } A \to (A \lor \lnot A)) $$
Question
My question, then, is twofold:
- If we combine this more restricted form of excluded middle with impredicative polymorphism, does proof irrelevance necessarily follow? I feel like the answer should be no, given that proof irrelevance seems to be the statement of 'every type in a given universe is a mere proposition'.
- Would the Combination of Impredicative Polymorphism + Mere Excluded Middle + Large Elimination Necessarily lead to inconsistency?
(also, as a bonus: do we lose any proof power with this restricted form of excluded middle)
Prop) gives you a universe $U$ which is closed under any quantification, ie if $x : A \vdash B : U$ then $\vdash \Pi x : A.B : U$, whatever the universe of $A$. $\endgroup$Propand $U_{+}$Type@{1}). In that case, the whole product still lives at $U$, despite $U$ being "lower" in the hierarchy than $U_{+}$. $\endgroup$