The Coq mailing list

[Abhishek Anand <abhishek.anand.iitg AT gmail.com>]

It seems that Propositional Extensionality is implied by the proof-irrelevant semantics(of Prop) given in 

http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.55.1709&rep=rep1&type=pdf

I quote:

" Propositions  are  interpreted  either  by  the  empty  set  or  by  a  canonical  sin- 

gleton,  depending  upon  their  validity  in  the  model.  As  a  consequence  all 

proof-terms  are  identified.  In  the  same  way,  tile  interpretation  of  Prop  is 

{0,1}. "

So, all true propositions have the same denotation(interpretation). I would guess this means Propositional Extensionality is indeed consistent with Coq's theory.

I hope it is just a fixable bug in the implementation(termination analysis?) of Coq.

-- Abhishek

http://www.cs.cornell.edu/~aa755/

On Thu, Dec 12, 2013 at 6:45 PM, Guillaume Melquiond <guillaume.melquiond AT inria.fr> wrote:

On 13/12/2013 00:30, Daniel Schepler wrote:

The Extensionality_Ensembles axiom in
http://coq.inria.fr/distrib/current/stdlib/Coq.Sets.Ensembles.html
easily implies propositional extensionality

In a similar way, propositional extensionality was used to prove the consistency of the set theory of Why3. And my email would be incomplete if I didn't quote the comment accompanying that Coq proof: "it is folklore that the two together are consistent". Famous last words...

Best regards,

Guillaume