The Coq mailing list

[Guillaume Melquiond <guillaume.melquiond AT inria.fr>]

Le 02/10/2018 à 18:53, Pierre Casteran a écrit :
> Hi,
>
>    It's probably a folklore result, but I didn't find a good reference 
> in the litterature.
>    Sorry if it is the case.
>
>    The question is :
>    Does there exists a sequent of propositional logic H1, H2, ... , Hn 
> |- False, which is provable in classical logic, but not in 
> intuitionnistic logic ?
>    All the examples I tried have been succesfully proved by tauto.
>
>    If it does not exists, is there a known (constructive ?) proof of that ?

Unless I am missing something, this is a corollary of the 
double-negation translation (Glivenko). In other words, if P -> False is 
provable in classical logic, then ((P -> False) -> False) -> False is 
provable in intuitionistic logic, which intuitionistically implies P -> 
False.

Best regards,

Guillaume