The Coq mailing list

[Benjamin Werner <benjamin.werner AT polytechnique.org>]

Hi,

No, excluded middles should not lead to inconsistencies in Coq, unless  
you launch Coq with the option -impredicative-set  which gives you the  
old version of the type theory.

The current version is meant to have a model in classical set theory  
which validates strong excluded middles. In this model, Any Prop has  
atmost one element. This is what prevents the known paradoxes. In  
particular, your

> Inductive pbool : Prop := ptrue | pfalse.

has only one element in the model which "explains" that you cannot  
eliminate towards a Type (which would mean discriminating between  
ptrue and pfalse).

With the option -impredicative-set  you can replace Prop by Set in  
your development and it should "work".

I hope this helps.

Benjamin



Le 9 mars 10 à 23:17, Robbert Krebbers a écrit :

> Hi,
>
> I'm wondering whether a strong version of excluded middle, em :  
> forall P : Prop, { P } + { ~P }, still results in inconsistency in  
> the current version of Coq. To prove inconsistency from it, I  
> defined a retract from Prop to bool (as described in [1] for an  
> older version of Coq), as follows.
>
> Parameter em : forall P, { P } + { ~P }.
>
> Definition b2P (b : bool) : Prop := match b with
> | true => True
> | false => False
> end.
>
> Definition P2b (P : Prop) : bool := match em P with
> | left _ => true
> | right _ => false
> end.
>
> Lemma P2P2 : forall P : Prop, P -> b2P (P2b P).
> Proof with auto.
> unfold P2b. unfold b2P. intros.
> destruct (em P)...
> Qed.
>
> Lemma P2P1 : forall P : Prop, b2P (P2b P) -> P.
> Proof with auto.
> unfold P2b. unfold b2P. intros.
> destruct (em P)...
> contradiction.
> Qed.
>
> Now I tried to use theories/Logic/Hurkens.v to show that this yields  
> a paradox. Unfortunately Hurkens.v requires a type bool : Prop  
> instead of the usual bool : Set (from the Coq library). So I tried  
> to define a boolean type in Prop as follows.
>
> Inductive pbool : Prop := ptrue | pfalse.
>
> This gets accepted, but elimination over inductive types in Prop is  
> not allowed, if I attempt to define P2b for pbool (similarly as for  
> bool) Coq gives the following message:
>
> Error:
> Incorrect elimination of "b" in the inductive type "pbool":
> the return type has sort "Type" while it should be "Prop".
> Elimination of an inductive object of sort Prop
> is not allowed on a predicate in sort Type
> because proofs can be eliminated only to build proofs.
>
> Alternatively I tried to change bool : Prop into bool : Set in  
> Hurkens.v, but then a lot of definitions break (obviously).  
> Therefore I wonder whether assuming em : forall P : Prop, { P } +  
> { ~P } still leads to inconsistency.
>
> Robbert
>
> [1] H. Geuvers, Inconsistency of classical logic in type theory,  
> Short Note (Version of November 27, 2001)