coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Folklore ?

From: Pierre Casteran <pierre.casteran AT labri.fr>
To: coq-club AT inria.fr
Subject: [Coq-Club] Folklore ?
Date: Tue, 2 Oct 2018 18:53:50 +0200 (CEST)
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=pierre.casteran AT labri.fr; spf=Pass smtp.mailfrom=pierre.casteran AT u-bordeaux.fr; spf=None smtp.helo=postmaster AT v-zimmta03.u-bordeaux.fr
Ironport-phdr: 9a23:v8W3TRzKHGC2QzLXCy+O+j09IxM/srCxBDY+r6Qd2+kRIJqq85mqBkHD//Il1AaPAd2Eraocw8Pt8InYEVQa5piAtH1QOLdtbDQizfssogo7HcSeAlf6JvO5JwYzHcBFSUM3tyrjaRsdF8nxfUDdrWOv5jAOBBr/KRB1JuPoEYLOksi7ze+/94HRbglSmDaxfa55IQmrownWqsQYm5ZpJLwryhvOrHtIeuBWyn1tKFmOgRvy5dq+8YB6/ShItP0v68BPUaPhf6QlVrNYFygpM3o05MLwqxbOSxaE62YGXWUXlhpIBBXF7A3/U5zsvCb2qvZx1S+HNsDwULs6Wymt771zRRHmiCkHLSA3/mLKhMN/kK1boRWvpwBkzoHOfI2aKOBzc7nBcd4YQ2dKQ8ZfVzZGAoO5d4YBFesBMvhCr4nnuVQFsAWzChO3BOPz1DBInGX53asn2OkmCQHG3RIvH8gUsHvKttn6KL0dUfupzKbW1zXMdfVW1Cz56IfSaR8hu/CMUah+ccrL0EQiER7OgFaIqYH9Ij+Y2eYAv3KF4+Z9Se6jkXArpxxxrzS1xcohhJHFi4YJxlze6Cl13po5KcelREJlf9KoCoZcuiCaOoduX88vTGNltDwkxrEbpZK3ZjYGxIkkyhLFdfCLbYiF7xT+X+iLOzh4nmhqeLenihay70egzur8W9Gq0FpTrytFk9zMtnUR1xPJ9sSKROFx/lq41TmU0ADT8PxLLl4umqrGJJ8t2LAwloALvUTCGC/5hln2gbeLekgr+OWk8frrbqj6qpOGKYN4lwHzPr4tl8GxGeg4NxIBX2mf+eSyzr3j+kj5Ta1Sjv03jKbZqoraKtoBqqGlGQBVyZoj5AilDzi81tQVhmQHIEtedxKAlYjmJk/BL+rlDfawmVisni1ry+jcPrL9GpXNMmTDkLD5cLlh7E5c0RM/wsxb55JJEb4MO+nzW0/0tNzAFBA1KQ20w+D9CNV8zIwSQ2yPArXKeJ/V5FSP/6ckJ/SGTI4Tojf0bfY/tMTjlXsopVhIZaikx4EaLnuxBehrOUyfSX7liM0AV2kQ7SQkS+m/sFyPSyReL127RL4x/Dg9QNa+DIrZXI3ri7WawCqhF5t+YmlMEFHKH22+JNbMYOsFdC/HepwpqTcDT7X0E9ZwhyHrjxfzzv9cFsSR/yQZsZz5090sur/O0Bs17zB5BtmNlW+XHTgtwjE4AgQu1aU6mnRTj0+Z2PEg0fhRH8ZSof1TAF9jaMzsitdiAtW3YTrvO9eETFH8HIe4RCMwS9ctyodVJVs4EdK4gh3KwjrsDaVHz7E=

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