The Coq mailing list

[gang chen <gangchen_sh AT yahoo.com>]

Hello,

Thanks for all replies.

From the discussion, it appears that neither PE nor its negation are
provable in Coq.

The motivation of this property is to use logical equivalence in rewriting,
I just discovered that Coq has added this capability in many situations.

Gang Chen


Bruno Barras wrote:
> 
> 
> PE is (believed) consistent with Coq since there is (but this is not
> formally established yet) a boolean model of Coq (i.e. where Prop is
> interpreted by booleans), and PE is valid in this model.
> (And this shows that the godelisation above cannot be effective without
> axiom.)
> 
> However PE is (believed) not provable, because there is also an
> intuitionistic model of Coq (but this is not formally established yet).
> You could think of it as assuming that Prop and Set are indeed the same
> sort. In that case, GC(Prop:=Set) does not hold:
> take F X := { x:X| forall y:X, x=y}  (X has exacly one inhabitant).
> unit <-> bool since they are both inhabited.
> (F unit) holds but (F bool) does not (true<>false).
> 
> Bruno Barras.
> 
> --------------------------------------------------------
> Bug reports: http://logical.futurs.inria.fr/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>           http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club
> 
> 

-- 
View this message in context: 
http://www.nabble.com/is-%22%28A%3C-%3EB%29-%3E%28%28F-A%29%3C-%3E%28F-B%29%29%22-provable---tp15470251p15482946.html
Sent from the Coq mailing list archive at Nabble.com.