coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] (A : Ens) ~(empty A) -> (EXT a : Ens | (IN a A))

From: "Lukasz Stafiniak" <l_stafiniak AT hoga.pl>
To: <coq-club AT pauillac.inria.fr>
Subject: [Coq-Club] (A : Ens) ~(empty A) -> (EXT a : Ens | (IN a A))
Date: Fri, 22 Aug 2003 22:55:12 +0200
Importance: normal
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
Priority: normal

Hi,

What about the above supposition?
Is it a safe axiom on the ground of Benjamin Werner's ZF?
(I don't know if I remember well the name -- I mean the ZF contribution.)
Perhaps it is derivable from some more general axiom?
(Excluded middle seems too weak (perhaps not?); think a minute -- is excl.
middle for predicates over Ens a consequence of this axiom?)

What is the best way to develop classical mathematics in Coq?

Thank You in advance,
Kindest Regards,
Lukasz

Uwaga! Do ko�ca sierpnia przed�u�yli�my promocje, do pakiet�w
wielostanowiskowych dok�adamy PenDrive Sprawd�:
http://www.mks.com.pl/promocja-mobile.html

[Coq-Club] (A : Ens) ~(empty A) -> (EXT a : Ens | (IN a A)), Lukasz Stafiniak