The Coq mailing list

[AUGER <Cedric.Auger AT lri.fr>]

Le Tue, 09 Mar 2010 23:17:57 +0100, Robbert Krebbers  
<robbertkrebbers AT student.ru.nl> 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)

I don't think strong em is inconsistant,
according to the non-scientific "else, it should be known" argument.
What is inconsistant is that a computable em exists
(else we could decide programs halting), so we can't
instantiate it. That is why we prefer to put it in Prop than Type, so we
are sure we can't try to compute with it.

But if you can prove that ptrue <> pfalse,
 (which would make inconsistant Proof irrelevance described in some coq  
file)
 you will have this proof: (I passed through elimination in Prop via em:
                            match p with ptrue => x | pfalse => y end ~
                            if em (p=ptrue) then x else y)

(* this axiom seems to be necessary *)
Axiom Ax: ptrue <> pfalse.

Goal False.
Proof with auto.
 Require Import Logic.Hurkens.
 (* now we apply Hurkens' paradox *)
 apply paradox with pbool (fun P => if em P then ptrue else pfalse)
                          (fun (b: pbool) => if em (b=ptrue) then True  
else False).
 (* b2p p2b specification *)
 intro A; destruct (em A).
  easy.
 case_eq (em (pfalse = ptrue)).
  intro e; case (Ax (sym_equal e)).
 easy.
 (* p2b b2p specification *)
 intros A a; case (em A).
  intros _; case (em (ptrue = ptrue)).
   easy.
  auto.
 intro n; case (n a).
Qed.

I have no proof of
(~(forall P, {P}+{~P})) -> (ptrue <> pfalse), if I had one then
strong em would be classically equivalent to proof-irrelevance on pbool,
but I doubt such a proof exists.

Take a look at the file ClassicalFacts.v,
my previous proof is essentially the
(** ** CC |- excluded-middle + dep elim on bool -> proof-irrelevance *)
part, as
I proved (~proof-irrelevance on pbool) -> (~strong em)
so by the contraposée (in its intuitionnistic version)
 (I don't know the english word of contraposée), we have
strong em (-> em) (-> proof-irr) -> proof-irr on pbool




--
Cédric AUGER

Univ Paris-Sud, Laboratoire LRI, UMR 8623, F-91405, Orsay