diff options
author | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-11-02 22:59:12 +0000 |
---|---|---|
committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-11-02 22:59:12 +0000 |
commit | b490f4216e68a5432f69b19ee1def2bcc454c2e8 (patch) | |
tree | e685cad414d327a2be7b9b1a2bd72336d8e61fe6 | |
parent | 9e95b47304c98e4bc41b6b31bf5ef96aba410851 (diff) |
Cosmetique
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4780 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r-- | theories/Logic/Diaconescu.v | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/theories/Logic/Diaconescu.v b/theories/Logic/Diaconescu.v index 12a14f7dc..ff94d8e3b 100644 --- a/theories/Logic/Diaconescu.v +++ b/theories/Logic/Diaconescu.v @@ -8,19 +8,19 @@ (*i $Id$ i*) -(* R. Diaconescu [1] showed that the Axiom of Choice in Set Theory - entails Excluded-Middle; S. Lacas and B. Werner [2] adapted the proof to - show that the axiom of choice in equivalence classes entails - Excluded-Middle in Type Theory. +(* R. Diaconescu [Diaconescu] showed that the Axiom of Choice in Set Theory + entails Excluded-Middle; S. Lacas and B. Werner [LacasWerner] + adapted the proof to show that the axiom of choice in equivalence + classes entails Excluded-Middle in Type Theory. This is an adaptatation of the proof by Hugo Herbelin to show that the relational form of the Axiom of Choice + Extensionality for predicates entails Excluded-Middle - [1] R. Diaconescu, Axiom of Choice and Complementation, in + [Diaconescu] R. Diaconescu, Axiom of Choice and Complementation, in Proceedings of AMS, vol 51, pp 176-178, 1975. - [2] S. Lacas, B Werner, Which Choices imply the excluded middle?, + [LacasWerner] S. Lacas, B Werner, Which Choices imply the excluded middle?, preprint, 1999. *) @@ -88,7 +88,7 @@ Qed. (* The proof of the excluded middle *) (* Remark: P could have been in Set or Type *) -Theorem EM : (P:Prop)P\/~P. +Theorem pred_ext_and_rel_choice_imp_EM : (P:Prop)P\/~P. Proof. Intro P. |