The Coq mailing list

[Dan Doel <dan.doel AT gmail.com>]

On Fri, Jan 20, 2012 at 11:24 PM, Daniel Schepler 
<dschepler AT gmail.com>
 wrote:
> Ah, OK.  Another issue is that if you go back and replace Prop with bool in
> the original example, then injectivity of a map ((T->bool)->bool) -> T is
> inconsistent with the axiom "classic_dec : forall P:Prop, {P} + {~P}".  The
> proof is pretty much the same, where you use classic_dec to convert certain
> Props to bools.
>
> I don't know whether that would be much of an issue in Agda; but in Coq, I
> wouldn't want to lose the ability to formalize classical mathematics (and 
> have
> the results be meaningful instead of just following from an inconsistency).
> But then, I guess it's fairly well-known that classic mathematics is
> inconsistent with an impredicative type system, at least if you want to be
> able to have "constructor discrimination".

You're right. It's probably not a viable option for Coq.

I'd still be interested to see a type theory that included them,
accepting the anti-classical implications and whatnot. I think it
could be useful from a programming perspective. I have a contrived
example or two that uses them.