The Coq mailing list

[Saint Wesonga <saintwesonga AT gmail.com>]

I figured out how to solve the proof I was working on without doing the case splitting which led to this scenario. Thank you very much for your insightful explanations though.

On Mon, Apr 23, 2012 at 8:15 AM, Chad E Brown <cebrown2323 AT yahoo.com> wrote:

(~p -> p) implies ~~p constructively, and p classically.

It does not imply ~p and it does not imply False.

Variable p : Prop.

Goal ((~p -> p) -> ~~p).

exact (fun f g => g (f g)).

Qed.

Hope this helps,

Chad

---

From: Bernard Hurley <bernard AT marcade.biz>
To: Adam Chlipala <adamc AT csail.mit.edu>
Cc: coq-club AT inria.fr
Sent: Monday, April 23, 2012 3:56 PM
Subject: Re: [Coq-Club] Inversion of a Prop Hypothesis

On Mon, Apr 23, 2012 at 09:23:53AM -0400, Adam Chlipala wrote:
> On 04/23/2012 09:20 AM, Bernard Hurley wrote:
>> I think Saint is trying to obtain a contradiction from the fact that 
>> he can prove v = v0 from v = v0 -> False.
>
> There fairly clearly is no contradiction inherent in such a deduction. 
> For instance, let [v = 0] and [v0 = 0].  The goal would be proved by 
> reflexivity.

The point I was making is that in Classical logic if you can derive P from ¬P from this you can derive ¬P giving a contradiction. It is easy to imagine this can be done in a case like this,

However in Intitionistic logic "I can derive P from ¬P" informally means something like:

"I have a construction that would turn a proof that 'a proof of P is impossible' into a proof of P."

Clearly this does not allow you to find a proof that "a proof of P is impossible" which is what you need to prove ¬P, so no contradiction can be derived without some further assumptions (e.g. that P is decidable.)

Bernard.