The Coq mailing list

[Bernard Hurley <bernard AT marcade.biz>]

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.