coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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)))
- [Coq-Club] reasoning out of type equalities, Aleks Nanevski, 08/04/2012
- Message not available
- Re: [Coq-Club] reasoning out of type equalities, Kristopher Micinski, 08/04/2012
- Message not available
- Re: [Coq-Club] reasoning out of type equalities, Chung-Kil Hur, 08/04/2012
- Re: [Coq-Club] reasoning out of type equalities, Vladimir Voevodsky, 08/04/2012
- Re: [Coq-Club] reasoning out of type equalities, Aleksandar Nanevski, 08/05/2012
- Re: [Coq-Club] reasoning out of type equalities, andré hirschowitz, 08/05/2012
- Re: [Coq-Club] reasoning out of type equalities, Aleksandar Nanevski, 08/05/2012
- Re: [Coq-Club] reasoning out of type equalities, Vladimir Voevodsky, 08/05/2012
- Re: [Coq-Club] reasoning out of type equalities, Aleksandar Nanevski, 08/05/2012
- Re: [Coq-Club] reasoning out of type equalities, Vladimir Voevodsky, 08/05/2012
- Re: [Coq-Club] reasoning out of type equalities, Aleksandar Nanevski, 08/05/2012
- Re: [Coq-Club] reasoning out of type equalities, Adam Chlipala, 08/05/2012
- Re: [Coq-Club] reasoning out of type equalities, Aleksandar Nanevski, 08/05/2012
- Re: [Coq-Club] reasoning out of type equalities, andré hirschowitz, 08/05/2012
- Re: [Coq-Club] reasoning out of type equalities, Vladimir Voevodsky, 08/05/2012
- Re: [Coq-Club] reasoning out of type equalities, Vladimir Voevodsky, 08/06/2012
- Re: [Coq-Club] reasoning out of type equalities, Aleksandar Nanevski, 08/05/2012
- Re: [Coq-Club] reasoning out of type equalities, Vladimir Voevodsky, 08/05/2012
- Re: [Coq-Club] reasoning out of type equalities, Aleksandar Nanevski, 08/05/2012
Archive powered by MHonArc 2.6.18.