The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

On Tue, Oct 2, 2018 at 10:09 AM 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.

Minor variant of this argument: More generally, Gamma |- P in
classical propositional logic if and only if Gamma |- ~~P in
intuitionistic propositional logic.  So, if H1, H2, ..., Hn |- False
classically, then H1, H2, ..., Hn |- (False -> False) -> False
intuitionistically.  But clearly, H1, H2, ..., Hn |- (False -> False)
intuitionistically also, so it would follow that H1, H2, ..., Hn |-
False intuitionistically.
-- 
Daniel