The Coq mailing list

[Julian Michael <julianjohnmichael AT gmail.com>]

I think a more concrete way to see it is just to consider instantiating P1 
with Bottom. In that case this is equivalent to double negation elimination 
~~P2 -> P2, which is not intuitionistically valid.

> On Feb 25, 2016, at 9:16 AM, Jonathan Leivent 
> <jonikelee AT gmail.com>
>  wrote:
> 
> 
> 
>> On 02/25/2016 11:52 AM, Stefan Ciobaca wrote:
>> Hello, coq-club!
>> 
>> I'm wondering if the following is provable constructively:
>> 
>>   forall (P1 P2 : Prop),
>>     (P1 <-> ~ P2) <-> (~ P1 <-> P2).
> 
> I don't think so.  Not being used to constructive logic myself, I use this 
> trick (which I'm not sure is always valid - so use at your own risk) to 
> spot such cases quickly.  Replace each negation of a Prop (~ P1) with a new 
> Prop (Q1), and see what that gives you:
> 
> forall (P1 P2 Q1 Q2 : Prop),
>    (P1 <-> Q2) <-> (Q1 <-> P2).
> 
> which is obviously not provable.  It's easy to see this way that the two 
> sides of the top <-> aren't even talking about the same things.  Otherwise, 
> my classic logic upbringing causes me to see negation as more meaningful 
> than it constructively is, and I get confused.
> 
> 
> -- Jonathan
>