The Coq mailing list

[Valentin Blot <coq-club AT valentinblot.org>]

One has to be careful when dealing with negative translation and first-
order logic. The same argument does not go through because there are
formulas that do not intuitionistically imply their negative
translation. From P -> False in classical logic you still get Pn ->
False in intuitionistic logic (where Pn is the negative translation of
P), but from there you cannot conclude P -> False because you may not
have P -> Pn intuitionistically.

Valentin

On mar., 2018-10-02 at 14:03 -0400, Shahab Tasharrofi wrote:
> 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