coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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:No, from this you can prove the classical "double negation" axiom:
forall (P1 P2 : Prop),
(P1 <-> ~ P2) <-> (~ P1 <-> P2).
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
Archive powered by MHonArc 2.6.18.