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)) $$


My question, then, is twofold:

  1. 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'.
  2. 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)

  • 2
    $\begingroup$ You might want to be more explicit about what exactly each of the principles you're talking about is. I often find that the conversation around these issues is pretty sloppy, and there are presumptions that inequivalent meanings of phrases like "proof irrelevance" are actually the same. The most obvious is "excluded middle" (or rather, its implication of "double negation elimination"), which could easily also be called "global choice" when formulated naively. Which things are contradictory together can depend on these exact meanings. $\endgroup$
    – Dan Doel
    Sep 20 at 16:16
  • 1
    $\begingroup$ BTW, I didn't mean that as a criticism of your question specifically. I mean the general 'folklore' understanding/discussion of these issues can be imprecise, and sometimes misleading. $\endgroup$
    – Dan Doel
    Sep 20 at 16:36
  • 1
    $\begingroup$ Your definition of impredicativity looks just like the normal rule for predicative universes to me. In my book, impredicativity (typically the one implemented by Coq's 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$ Sep 27 at 14:35
  • 1
    $\begingroup$ Still not there: your new phrasing is just a special case of the previous one, (with $U = U_i = U_j$). Impredicativity kicks in when $A$ is large, typically $U$ itself (say of type some other universe $U_{+}$, in pseudo-Coq $U$ would be Prop and $U_{+}$ Type@{1}). In that case, the whole product still lives at $U$, despite $U$ being "lower" in the hierarchy than $U_{+}$. $\endgroup$ Sep 27 at 17:26
  • 1
    $\begingroup$ I think your new-new-phrasing is straight up inconsistent because taking $B = U_0$ and $A = 1$ you get essentially $U_0 : U_0$. The pending edit request seems to be the correct rules. $\endgroup$
    – Trebor
    Sep 28 at 15:59


Your Answer

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