The Coq mailing list

[Bernard Hurley <bernard AT marcade.biz>]

Sorry I was getting confused!

Bernard.

On Mon, Apr 23, 2012 at 07:15:23AM -0700, Chad E Brown 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.