coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Jonathan Leivent <jonikelee 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 12:16:06 -0500
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=jonikelee AT gmail.com; spf=Pass smtp.mailfrom=jonikelee AT gmail.com; spf=None smtp.helo=postmaster AT mail-qg0-f43.google.com
Ironport-phdr: 9a23:i3jVnBdV5a3BTWfR/oaIdjT7lGMj4u6mDksu8pMizoh2WeGdxc65bR7h7PlgxGXEQZ/co6odzbGG7Oa+ACddsd6oizMrTt9lb1c9k8IYnggtUoauKHbQC7rUVRE8B9lIT1R//nu2YgB/Ecf6YEDO8DXptWZBUiv2OQc9HOnpAIma153xjLDtvcOKKFgYzBOGIppMbzyO5T3LsccXhYYwYo0Q8TDu5kVyRuJN2GlzLkiSlRuvru25/Zpk7jgC86l5r50IAu3GePEzSqUdBzA7OUg04tfqvF/NV1ih/HwZB0cRlBNUAwHDpDX3X4n8tDey4uh63iiZMMn7QJg7XD2j6+FgTxq+23RPDCIw7GyC0p84t6lcuh/0/xE=

On 02/25/2016 11:52 AM, Stefan Ciobaca wrote:

Hello, coq-club!

I'm wondering if the following is provable constructively:

forall (P1 P2 : Prop),
(P1 <-> ~ P2) <-> (~ P1 <-> P2).

I don't think so. Not being used to constructive logic myself, I use this trick (which I'm not sure is always valid - so use at your own risk) to spot such cases quickly. Replace each negation of a Prop (~ P1) with a new Prop (Q1), and see what that gives you:

forall (P1 P2 Q1 Q2 : Prop),
(P1 <-> Q2) <-> (Q1 <-> P2).

which is obviously not provable. It's easy to see this way that the two sides of
the top <-> aren't even talking about the same things. Otherwise, my classic
logic upbringing causes me to see negation as more meaningful than it
constructively is, and I get confused.

-- Jonathan

[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