Skip to Content.
Sympa Menu

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

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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


Chronological Thread 
  • 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



Archive powered by MHonArc 2.6.18.

Top of Page