The Coq mailing list

[Shahab Tasharrofi <shahab.tasharrofi AT gmail.com>]

In addition to what others said, you can also generalize it to first-order logic: https://en.wikipedia.org/wiki/Double-negation_translation

On Tue, Oct 2, 2018 at 1:09 PM Guillaume Melquiond <guillaume.melquiond AT inria.fr> wrote:

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