The Coq mailing list

[Robbert Krebbers <mail AT robbertkrebbers.nl>]

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 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 using theories/Logic/Hurkens.v to show that this yields a 
paradox. Unfortunately it 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 works, 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 modify Hurkens.v such that it works for bool : 
Set, but failed since I had no actual clue what is going on. 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)