diff options
Diffstat (limited to 'theories/Logic/Diaconescu.v')
| -rw-r--r-- | theories/Logic/Diaconescu.v | 36 |
1 files changed, 18 insertions, 18 deletions
diff --git a/theories/Logic/Diaconescu.v b/theories/Logic/Diaconescu.v index 19d5d7ec..5f139f35 100644 --- a/theories/Logic/Diaconescu.v +++ b/theories/Logic/Diaconescu.v @@ -7,7 +7,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Diaconescu.v 8892 2006-06-04 17:59:53Z herbelin $ i*) +(*i $Id: Diaconescu.v 9245 2006-10-17 12:53:34Z notin $ i*) (** Diaconescu showed that the Axiom of Choice entails Excluded-Middle in topoi [Diaconescu75]. Lacas and Werner adapted the proof to show @@ -44,7 +44,7 @@ *) (**********************************************************************) -(** *** A. Pred. Ext. + Rel. Axiom of Choice -> Excluded-Middle *) +(** * Pred. Ext. + Rel. Axiom of Choice -> Excluded-Middle *) Section PredExt_RelChoice_imp_EM. @@ -156,7 +156,7 @@ Qed. End PredExt_RelChoice_imp_EM. (**********************************************************************) -(** *** B. Proof-Irrel. + Rel. Axiom of Choice -> Excl.-Middle for Equality *) +(** * B. Proof-Irrel. + Rel. Axiom of Choice -> Excl.-Middle for Equality *) (** This is an adaptation of Diaconescu's paradox exploiting that proof-irrelevance is some form of extensionality *) @@ -263,7 +263,7 @@ Qed. End ProofIrrel_RelChoice_imp_EqEM. (**********************************************************************) -(** *** B. Extensional Hilbert's epsilon description operator -> Excluded-Middle *) +(** * Extensional Hilbert's epsilon description operator -> Excluded-Middle *) (** Proof sketch from Bell [Bell93] (with thanks to P. Castéran) *) @@ -285,20 +285,20 @@ Notation Local eps := (epsilon bool true) (only parsing). Theorem extensional_epsilon_imp_EM : forall P:Prop, P \/ ~ P. Proof. -intro P. -pose (B := fun y => y=false \/ P). -pose (C := fun y => y=true \/ P). -assert (B (eps B)) as [Hfalse|HP] - by (apply epsilon_spec; exists false; left; reflexivity). -assert (C (eps C)) as [Htrue|HP] - by (apply epsilon_spec; exists true; left; reflexivity). - right; intro HP. - assert (forall y, B y <-> C y) by (intro y; split; intro; right; assumption). - rewrite epsilon_extensionality with (1:=H) in Hfalse. - rewrite Htrue in Hfalse. - discriminate. -auto. -auto. + intro P. + pose (B := fun y => y=false \/ P). + pose (C := fun y => y=true \/ P). + assert (B (eps B)) as [Hfalse|HP] + by (apply epsilon_spec; exists false; left; reflexivity). + assert (C (eps C)) as [Htrue|HP] + by (apply epsilon_spec; exists true; left; reflexivity). + right; intro HP. + assert (forall y, B y <-> C y) by (intro y; split; intro; right; assumption). + rewrite epsilon_extensionality with (1:=H) in Hfalse. + rewrite Htrue in Hfalse. + discriminate. + auto. + auto. Qed. End ExtensionalEpsilon_imp_EM. |