coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Folklore ?

From: Dan Frumin <dfrumin AT cs.ru.nl>
To: coq-club AT inria.fr, Pierre Casteran <pierre.casteran AT labri.fr>
Subject: Re: [Coq-Club] Folklore ?
Date: Tue, 2 Oct 2018 19:08:28 +0200
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=dfrumin AT cs.ru.nl; spf=Pass smtp.mailfrom=dfrumin AT cs.ru.nl; spf=None smtp.helo=postmaster AT smtp2.science.ru.nl
Ironport-phdr: 9a23:H+xJwh/62XY1YP9uRHKM819IXTAuvvDOBiVQ1KB42+gcTK2v8tzYMVDF4r011RmVBdqds6oMotGVmpioYXYH75eFvSJKW713fDhBt/8rmRc9CtWOE0zxIa2iRSU7GMNfSA0tpCnjYgBaF8nkelLdvGC54yIMFRXjLwp1Ifn+FpLPg8it2O2+55/ebx9UiDahfLh/MAi4oQLNu8cMnIBsMLwxyhzHontJf+RZ22ZlLk+Nkhj/+8m94odt/zxftPw9+cFAV776f7kjQrxDEDsmKWE169b1uhTFUACC+2ETUmQSkhpPHgjF8BT3VYr/vyfmquZw3jSRMNboRr4oRzut86ZrSAfpiCgZMT457HrXgdF0gK5CvR6tuwBzz4vSbYqINvRxY7ndcMsHS2RfUMZfVy9PDI2yYIQADeUOIelWopLhp1YNtxayGRWgCe3txzJOm3T43bc60+MkEQze0gIvBdQOu2nUotXvKacSVOG1zK/VxjjEcvxW1y396JXNchAgp/GBRq5/cdHLxUk1CgPJlFOQqYj8Mj6Ty+8DsHCb4vJ9We+hlmIrsRx9rzqgy8s2l4XEh5gZxk3L+Ch52Io5ONK1RU5hbdK5DZddtjuWO5Z1T84mWW1luSc3x7sbspChZicK0o4oxxvHZvyHbYeI5hXjWf6KITd9mHJlYKyziwyp8Ue8y+3zSM+030pUoSZfiNnMq2oB1xrX6sSfS/t9+Fmu2SqX2gzO5OxIPFo4mbfZJpMu2LI8i5sevV7eEiL5mEj6lKqWeV8l+uis5eTneLLmppqEOoBphAH+KLkumsm+AeQ+KQUBQ3Ob9f6m1L3+50H5RrFKguUskqbFqJDaOdgbpqmhDgBJ1YYj8g+zACui0NQFhnYKN0lFeRKCj4jxIV7COvH4DfGlg1Stijhn3f7GPqeySqnKe3PEifLqeat3w09a0gs6i95Fo9psC7wbOv+7cUbqqNHCBxlxZxS1zvz9BZN235gCVHiGBIedOanIsBmG/LR8DfOLYdo5sTC1BeI44v/oxSs1l0UAeKiv9ZAMLmqlWPJidRbKKUHwi8sMRD9Z9jE1S/bn3RjbCWYKNiSCGpkk7zR+M7qISILKR4SjmruEhX/pFYYQfH0ADFTeSC60JbXBYO8FbWepGuEkiiYNDODzQJRnzwzosguok+M6fNqRwTURsNfY7PYw5+DXkktrpydxE9zHlXqGTmxylW5OXSJw2qQt+UE=

Hi Pierre,

I don't think such sequent exists.

W.l.o.g. we can consider the case P |- False.
By deduction lemma we get that |- P -> False is provable classically.
But then by Gilvenko's theorem |- ((P -> False) -> False) -> False is
provable intuitionistically.
In this specific case we can eliminate double negation and get |- P -> False
intuitonistically.

Best,
-Dan

On 02-10-18 18:53, Pierre Casteran wrote:

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 ?

Pierre

[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