The Coq mailing list

[Julian Michael <julianjohnmichael AT gmail.com>]

whoops, Robbert beat me to it :) yup, generally to verify that a proposition 
isn't intuitionistically provable, you can reduce it to LEM, WEM (~p \/ ~~p), 
or the law of double negation (~~p -> p); the latter two of which are 
equivalent to LEM when taken together. Also, if it's classically provable and 
begins with a negation, then it's intuitionistically provable (by Glivenko's 
theorem). But these are just tools for propositional formulas.

> On Feb 25, 2016, at 9:28 AM, Robbert Krebbers 
> <mailinglists AT robbertkrebbers.nl>
>  wrote:
> 
>> On 02/25/2016 05:52 PM, Stefan Ciobaca wrote:
>> I'm wondering if the following is provable constructively:
>> 
>>   forall (P1 P2 : Prop),
>>     (P1 <-> ~ P2) <-> (~ P1 <-> P2).
> No, from this you can prove the classical "double negation" axiom:
> 
>  Goal
>    (forall (P1 P2 : Prop), (P1 <-> ~ P2) <-> (~ P1 <-> P2)) ->
>    forall (P : Prop), ~~P -> P.
>  Proof. intros ax P HP; now apply (ax P (~P)). Qed.
> 
> This is done by taking (P1:=P) and (P2:=~P), so this gives:
> 
>  (P <-> ~~P) <-> (~ P <-> ~P).
> 
> The RHS is trivial, and the LHS is double negation. Qed :).
> 
> Best,
> 
> Robbert