[Prev][Next][Index][Thread]

Classical Logic and Coq

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.
Here, {A}+{~A} means that we have a disjunction that allows us to define
a function (e.g. to bool : Set) by case distinction.
The inconsistency is proved by adapting the proof of Girard's paradox of
Hurkens (TLCA 1995) to it.
Probably this result is known by some of you, but I think that the proof
is really very short.

Best Regards & Comments are welcomed

--
Herman Geuvers
Dept. of Computer Science, KUN
Toernooiveld 1
6525 ED Nijmegen, NL
Room: A4028
tel: ++31 (0)243-652603 (secr: ++31 (0)243-652643)
fax: ++31 (0)243-652525
mail: herman@cs.kun.nl
url: http:://www.cs.kun.nl/~herman



--------------6C2E1452246FECD2F31EBF6E
Content-Type: text/html; charset=us-ascii
Content-Transfer-Encoding: 7bit

<!doctype html public "-//w3c//dtd html 4.0 transitional//en">
<html>
<tt>LS,</tt><tt></tt>
<p><tt>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 <A HREF="http::/www.cs.kun.nl/~herman/note.ps.gz">http::/www.cs.kun.nl/~herman/note.ps.gz</A></tt><tt></tt>
<p><tt>What is shown is that (A:Prop){A}+{~A} implies bottom, in Coq.</tt>
<br><tt>Here, {A}+{~A} means that we have a disjunction that allows us
to define a function (e.g. to bool : Set) by case distinction.</tt>
<br><tt>The inconsistency is proved by adapting the proof of Girard's paradox
of Hurkens (TLCA 1995) to it.</tt>
<br><tt>Probably this result is known by some of you, but I think that
the proof is really very short.</tt><tt></tt>
<p><tt>Best Regards &amp; Comments are welcomed</tt>
<pre>--&nbsp;
Herman Geuvers
Dept. of Computer Science, KUN
Toernooiveld 1
6525 ED Nijmegen, NL
Room: A4028
tel: ++31 (0)243-652603 (secr: ++31 (0)243-652643)
fax: ++31 (0)243-652525
mail: herman@cs.kun.nl
url: <A HREF="http:://www.cs.kun.nl/~herman">http:://www.cs.kun.nl/~herman</A></pre>
&nbsp;</html>

--------------6C2E1452246FECD2F31EBF6E--