coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Robbert Krebbers <mailinglists AT robbertkrebbers.nl>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] constructive proof of (P1 <-> ~ P2) <-> (~ P1 <-> P2)
Date: Thu, 25 Feb 2016 18:28:03 +0100
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=mailinglists AT robbertkrebbers.nl; spf=None smtp.mailfrom=mailinglists AT robbertkrebbers.nl; spf=None smtp.helo=postmaster AT smtp1.science.ru.nl
Ironport-phdr: 9a23:SSxBrxSxFFRsHy05L36UNWoNMdpsv+yvbD5Q0YIujvd0So/mwa64YRWN2/xhgRfzUJnB7Loc0qyN4/+mBzVLvMbJmUtBWaIPfidNsd8RkQ0kDZzNImzAB9muURYHGt9fXkRu5XCxPBsdMs//Y1rPvi/6tmZKSV3BPAZ4bt74BpTVx5zukbvipNuNOk4V1HKUWvBbElaflU3prM4YgI9veO4a6yDihT92QdlQ3n5iPlmJnhzxtY+a9Z9n9DlM6bp6r5YTGfayQ6NtRrtBST8iLmod5cvxtBCFQxHcyGEbVzAslRBCDhLZpDLgU537vzHh/r540SiePMv5SbEvRS+K9aBhQhLylCQdOjQz/XvMzMp02vEI6Cm9rgByltaHKLqeM+BzK/vQ

On 02/25/2016 05:52 PM, Stefan Ciobaca wrote:

I'm wondering if the following is provable constructively:

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

No, from this you can prove the classical "double negation" axiom:

Goal
(forall (P1 P2 : Prop), (P1 <-> ~ P2) <-> (~ P1 <-> P2)) ->
forall (P : Prop), ~~P -> P.
Proof. intros ax P HP; now apply (ax P (~P)). Qed.

This is done by taking (P1:=P) and (P2:=~P), so this gives:

(P <-> ~~P) <-> (~ P <-> ~P).

The RHS is trivial, and the LHS is double negation. Qed :).

Best,

Robbert

[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