The Coq mailing list

[Aleksandar Nanevski <aleks.nanevski AT imdea.org>]

Interesting.

Ok, what if nonempty B is defined as (exists v : B, True), rather than as (B <> False)?

-Aleks

On 8/5/12 2:20 PM, Vladimir Voevodsky wrote:

No. 

not((A or (not A)) = False) <-> not(not(A or (not A)) <->  not ((not A) and A) <-> not(False) <-> True.

V.

On Aug 5, 2012, at 7:48 AM, Aleksandar Nanevski wrote:

Is False supposed to be the type B that gets cancelled in my example

  A1 * B = A2 * B -> A1 = A2?

If so, then I'm not sure your argument applies. I have postulated that B is nonempty, and hence can't be False.

I now realize that the same issue appears in Vladimir's email: If B = (A or not A) is nonempty, then isn't excluded middle already assumed?

-Aleks

On 8/5/12 12:53 PM, andré hirschowitz wrote:

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)))