The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

Andrew Pennebaker wrote:
> Oo, the Haskell IO point is apt. So I guess propositional logic 
> tautologies aren't the easiest things to do in Coq? :)

No, they're very easy, either automatically or, after the proper 
preparation, manually.

I don't mean to be argumentative, but I'm going to start ignoring your 
questions if you keep ignoring mine about which chunk of CPDT you have 
read.  I truly believe all of your questions on propositional logic so 
far are answered in CPDT, in reasonably accessible form.

> Re: The law of excluded middle
>
> How much of our logic is not based on the law of excluded middle?
>
> Can Peirce's Law be derived without it?

Peirce's law and excluded middle are logically equivalent.

I don't know of any theorem in, for instance, verification of 
traditional programs that fundamentally relies on classical logic.  
Rather, I view it as more of a shortcut to avoid proving decidability of 
some important families of propositions.