The Coq mailing list

[Thorsten Altenkirch <Thorsten.Altenkirch AT nottingham.ac.uk>]

Thank you, Valentin.

It is true that the double negation of PEM is provable intuitionistically, 
that is ~~(P \/ ~P) for all P:Prop, but it is not true the double negation of 
universally quantified PEM is provable, that is ~~(forall x:A.P x \/ ~ P x) 
is not provable, and indeed if we accept Church's priniciple we may want that 
~ forall n:Nat.Hold(n) \/ ~Hold(n) is provable (Here Hold(n) means that the 
nth TM applied to n terminates).

Thorsten 
On 03/10/2018, 08:38, 
"coq-club-request AT inria.fr
 on b

ehalf of Valentin Blot" 
<coq-club-request AT inria.fr
 on behalf of 
coq-club AT valentinblot.org>
 wrote:

    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
    
    




This message and any attachment are intended solely for the addressee
and may contain confidential information. If you have received this
message in error, please contact the sender and delete the email and
attachment. 

Any views or opinions expressed by the author of this email do not
necessarily reflect the views of the University of Nottingham. Email
communications with the University of Nottingham may be monitored 
where permitted by law.