The Coq mailing list

[Conor McBride <conor AT strictlypositive.org>]

Hi

I sent a message to Gang Chen when I meant to send it
to the list, but it basically says what Bruno says...

On 14 Feb 2008, at 11:54, Bruno Barras wrote:
> In fact, Gang Chen's property (GC) is equivalent to propositional
> extensionality
> PE : forall A B: Prop,(A<->B)->A=B.
>
> Obviously PE -> GC.
> GC->PE is also provable:
> Axiom equiv : forall (F : Prop->Prop) (A B : Prop), (A<->B)->((F A) 
> <->(F
> B)).
> Goal forall A B, (A<->B) -> A=B.
> intros.
> elim (equiv (fun P => P=B) _ _ H); intros.
> auto.
> Qed.
>
> 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,

...and adds a more syntactic account of non-provability
of PE, which I'll repeat and expand.

If PE held in Coq, we could use it to prove that, for
some trivial closed proposition T, we have

  T = T -> T

in the empty context. But reflexvity cannot construct
such a proof.

In Epigram 2's core theory, propositional equality
(defined type by type, extensional for functions) on
propositions is defined to be logical equivalence. Of
course, we then have to ensure that there are no
possible observations on propositions which allow finer
distinctions. It's rather nice, because if we have an
equivalence relation R, then

  R x y <-> R x = R y

But I digress.

All the best

Conor