Re: Classical Logic and Coq

• To: Herman Geuvers <herman@cs.kun.nl>, types@cis.upenn.edu
• Subject: Re: Classical Logic and Coq
• From: Gerard Huet <Gerard.Huet@inria.fr>
• Date: Fri, 27 Apr 2001 17:49:30 +0200

At 15:02 27/04/01 +0200, Herman Geuvers wrote: 
> I have just completed a short proof of the fact that a strong form of 
> classical logic is inconsistent in Coq. I wrote a short note about it, 
> which can be found here http::/www.cs.kun.nl/~herman/note.ps.gz 
>
> What is shown is that (A:Prop){A}+{~A} implies bottom, in Coq. 


Hi, Herman, this is nicely concise.
I would personally not call it an inconsistency of a strong form of classical
logic, but rather an internal proof of undecidability of the underlying logic.
But it ought definitely be pointed out to users who may be tempted to mix
classical reasoning with constructive operators in higher order logic, with
catastrophic effects indeed. 
Bravo
Gerard

• Prev: Classical Logic and Coq
• Next: Technical Report Available
• Index(es):
  • Main
  • Thread