Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] reasoning out of type equalities

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] reasoning out of type equalities


Chronological Thread 
  • From: andré hirschowitz <ah AT unice.fr>
  • To: Vladimir Voevodsky <vladimir AT ias.edu>
  • Cc: Aleks Nanevski <aleks.nanevski AT imdea.org>, coq-club AT inria.fr
  • Subject: Re: [Coq-Club] reasoning out of type equalities
  • Date: Sun, 5 Aug 2012 12:53:05 +0200

This could probably be simplified into

False * True <-> False <-> False * False.

ah 

2012/8/4 Vladimir Voevodsky <vladimir AT ias.edu>
This is not provable. In fact in combination with propositional extensionality (axiom saying that for A,B:Prop one has (A<->B)->(A=B ) it would imply the excluded middle.

Indeed, for all A:Prop, (A or (not A) is nonempty and on the other hand

((A or (not A)) and True)  <->  (A or (not A) )  <-> ((A or (not A)) and (A or (not A)))

 



Archive powered by MHonArc 2.6.18.

Top of Page