coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] constructive proof of (P1 <-> ~ P2) <-> (~ P1 <-> P2)

From: Michel Levy <michel.levy1948 AT gmail.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] constructive proof of (P1 <-> ~ P2) <-> (~ P1 <-> P2)
Date: Thu, 25 Feb 2016 21:16:34 +0100
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=michel.levy1948 AT gmail.com; spf=Pass smtp.mailfrom=michel.levy1948 AT gmail.com; spf=None smtp.helo=postmaster AT mail-wm0-f43.google.com
Ironport-phdr: 9a23:hI1UlBFEbU2do3t12YfCLJ1GYnF86YWxBRYc798ds5kLTJ75o8ywAkXT6L1XgUPTWs2DsrQf27WQ7fmrCDFIyK3CmU5BWaQEbwUCh8QSkl5oK+++Imq/EsTXaTcnFt9JTl5v8iLzG0FUHMHjew+a+SXqvnYsExnyfTB4Ov7yUtaLyZ/niKbsotaCPk1hv3mUX/BbFF2OtwLft80b08NJC50a7V/3mEZOYPlc3mhyJFiezF7W78a0+4N/oWwL46pyv50IbaKvdKMhCLdcET4OMmYv5cStuwOQYxGI4y45U24Wnx4AJwXb/VmuW5b6sib+8O5wxjjDbJGmZb8xUDWmqaxsTUm72288Kzcl/TSP2YRLh6VBrUf5qg==

On 25/02/2016 17:52, Stefan Ciobaca wrote:

Hello, coq-club!

I'm wondering if the following is provable constructively:

forall (P1 P2 : Prop),

(P1 <-> ~ P2) <-> (~ P1 <-> P2).

The tactic tauto solves it in the presence of EM:

Require Import Classical.

Lemma P1_if_not_P2 :

forall (P1 P2 : Prop),

(P1 <-> ~ P2) <-> (~ P1 <-> P2).

Proof.

intros.

tauto.

Qed.

But tauto fails without the Classical module.

Best wishes,

Stefan Ciobaca

As Ralf Jung says, tauto is complete for intuitionistic logic. So, if you can't prove this formula with tauto, it mean that the formula is not intuitionistically provable.
I have written (a long time ago) a prover http://teachinglogic.liglab.fr/INT1/index.php which can build a (Kripke) counter-model of this formula.
Warning : in this prover, <-> is written <=> and ~ is written -.

-- 
courriel : michel.levy1948 AT gmail.com
web : http://membres-liglab.imag.fr/michel.levy 
fixe : 04 76 24 33 39
mobile : 06 59 13 42 53

[Coq-Club] constructive proof of (P1 <-> ~ P2) <-> (~ P1 <-> P2), Stefan Ciobaca, 02/25/2016
- Re: [Coq-Club] constructive proof of (P1 <-> ~ P2) <-> (~ P1 <-> P2), Benoît Viguier, 02/25/2016
- Re: [Coq-Club] constructive proof of (P1 <-> ~ P2) <-> (~ P1 <-> P2), Jonathan Leivent, 02/25/2016
  - Re: [Coq-Club] constructive proof of (P1 <-> ~ P2) <-> (~ P1 <-> P2), Julian Michael, 02/25/2016
- Re: [Coq-Club] constructive proof of (P1 <-> ~ P2) <-> (~ P1 <-> P2), Robbert Krebbers, 02/25/2016
  - Re: [Coq-Club] constructive proof of (P1 <-> ~ P2) <-> (~ P1 <-> P2), Julian Michael, 02/25/2016
- Re: [Coq-Club] constructive proof of (P1 <-> ~ P2) <-> (~ P1 <-> P2), Ralf Jung, 02/25/2016
- Re: [Coq-Club] constructive proof of (P1 <-> ~ P2) <-> (~ P1 <-> P2), Michel Levy, 02/25/2016