coq-club AT inria.fr

Subject: The Coq mailing list

List archive

From: sunil <sarswat AT gmail.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Folklore ?
Date: Wed, 3 Oct 2018 00:06:58 +0530
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=sarswat AT gmail.com; spf=Pass smtp.mailfrom=sarswat AT gmail.com; spf=None smtp.helo=postmaster AT mail-it1-f177.google.com
Ironport-phdr: 9a23:iY0V0RypCa6Q737XCy+O+j09IxM/srCxBDY+r6Qd1ewVIJqq85mqBkHD//Il1AaPAd2Eraocw8Pt8InYEVQa5piAtH1QOLdtbDQizfssogo7HcSeAlf6JvO5JwYzHcBFSUM3tyrjaRsdF8nxfUDdrWOv5jAOBBr/KRB1JuPoEYLOksi7ze+/94HRbglSmDaxfa55IQmrownWqsQYm5ZpJLwryhvOrHtIeuBWyn1tKFmOgRvy5dq+8YB6/ShItP0v68BPUaPhf6QlVrNYFygpM3o05MLwqxbOSxaE62YGXWUXlhpIBBXF7A3/U5zsvCb2qvZx1S+HNsDwULs6Wymt771zRRDnhicINT43/m/UhMJtkqxUvAmsqAZjz4POeoyZKOZyc6HbcNgHRWRBRMFRVylZD4OncosPCesBPeJFpIT6vFsBtwG+BRKiBez11j9FnXD23agg3OQgFQHKxhAvH9ULsHnNqtj+KaQcUfitwaXW0TnOa+la1DT95YTSbxwsoPCBUahtfcfTy0QiER7OgE+Kpoz/JTyV0/wAs2iF4OpkUuKik2snpBtwojir38ssi5XJip8MxlDK6Cl0woQ4Kce3SE58Zt6kH59QuD+AO4RqRcMiRnlkuCc8yrIYpZ62ZDYGxIgjyhLFaPGKc5KE7g/iWeuQOzt0mXBodbCnixa360egy+n8Vseu0FZNqypIisLMuWoX1xzI5MmIUOd981yu2TaKzQ/T6+VELVoomqrcLp4t2qQwmYYLsUTfAi/2n137g7ORdkU94+Sn9+DnYqj9qZKHLI91igT+Mrw0lcClAOQ4NBIOX2mB9uim2r3j5x6xfLIfhfov16LdrZryJMIBp6f/DRUG/Jwk7kOkEjGn1JxMhnAdN01MZDqIioHoPxfFJ/WuXqT3uEiljDo+n6OOBbbmGJiYdiGSwoekRq507gtn8CR2yNle45xODbRYeaD8X0bwsJrTCRpralXokdaiM81008YlYUzKGrWQafqAvlqB5+ZpKO6JNtdM5WTNbsM97vurtkcX3F8Qea7zg8kSYXG8W/V6egCXOCWzxNgGFmgOs0w1S+m40FA=

अहिंसा परमो धर्म । धर्मो़ ( .( बिन्दु right). उपर.).🕉️- an example of a folklore.

On Tue 2 Oct, 2018, 10:24 PM Pierre Casteran, <pierre.casteran AT labri.fr> wrote:

Hi,

It's probably a folklore result, but I didn't find a good reference in the litterature.

Please define term folklore .

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 ?

Pierre

- suneel sarswat

Yes/no?

[Coq-Club] Folklore ?, Pierre Casteran, 10/02/2018
- Re: [Coq-Club] Folklore ?, Dan Frumin, 10/02/2018
- Re: [Coq-Club] Folklore ?, Guillaume Melquiond, 10/02/2018
  - Re: [Coq-Club] Folklore ?, Shahab Tasharrofi, 10/02/2018
    - Re: [Coq-Club] Folklore ?, Valentin Blot, 10/03/2018
      - Re: [Coq-Club] Folklore ?, Thorsten Altenkirch, 10/03/2018
  - Re: [Coq-Club] Folklore ?, Daniel Schepler, 10/03/2018
- Re: [Coq-Club] Folklore ?, sunil, 10/02/2018