diff options
Diffstat (limited to 'theories/Logic/Diaconescu.v')
| -rw-r--r-- | theories/Logic/Diaconescu.v | 222 |
1 files changed, 194 insertions, 28 deletions
diff --git a/theories/Logic/Diaconescu.v b/theories/Logic/Diaconescu.v index 3e94deda..19d5d7ec 100644 --- a/theories/Logic/Diaconescu.v +++ b/theories/Logic/Diaconescu.v @@ -1,3 +1,4 @@ +(* -*- coding: utf-8 -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) @@ -6,26 +7,46 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Diaconescu.v 6401 2004-12-05 16:44:57Z herbelin $ i*) +(*i $Id: Diaconescu.v 8892 2006-06-04 17:59:53Z herbelin $ i*) -(** 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. +(** Diaconescu showed that the Axiom of Choice entails Excluded-Middle + in topoi [Diaconescu75]. Lacas and Werner adapted the proof to show + that the axiom of choice in equivalence classes entails + Excluded-Middle in Type Theory [LacasWerner99]. - 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 + Three variants of Diaconescu's result in type theory are shown below. - [Diaconescu] R. Diaconescu, Axiom of Choice and Complementation, in - Proceedings of AMS, vol 51, pp 176-178, 1975. + A. A proof that the relational form of the Axiom of Choice + + Extensionality for Predicates entails Excluded-Middle (by Hugo + Herbelin) - [LacasWerner] S. Lacas, B Werner, Which Choices imply the excluded middle?, - preprint, 1999. + B. A proof that the relational form of the Axiom of Choice + Proof + Irrelevance entails Excluded-Middle for Equality Statements (by + Benjamin Werner) + C. A proof that extensional Hilbert epsilon's description operator + entails excluded-middle (taken from Bell [Bell93]) + + See also [Carlström] for a discussion of the connection between the + Extensional Axiom of Choice and Excluded-Middle + + [Diaconescu75] Radu Diaconescu, Axiom of Choice and Complementation, + in Proceedings of AMS, vol 51, pp 176-178, 1975. + + [LacasWerner99] Samuel Lacas, Benjamin Werner, Which Choices imply + the excluded middle?, preprint, 1999. + + [Bell93] John L. Bell, Hilbert's epsilon operator and classical + logic, Journal of Philosophical Logic, 22: 1-18, 1993 + + [Carlström04] Jesper Carlström, EM + Ext_ + AC_int <-> AC_ext, + Mathematical Logic Quaterly, vol 50(3), pp 236-240, 2004. *) -Section PredExt_GuardRelChoice_imp_EM. +(**********************************************************************) +(** *** A. Pred. Ext. + Rel. Axiom of Choice -> Excluded-Middle *) + +Section PredExt_RelChoice_imp_EM. (** The axiom of extensionality for predicates *) @@ -59,15 +80,9 @@ Qed. Require Import ChoiceFacts. -Variable rel_choice : forall A B:Type, RelationalChoice A B. +Variable rel_choice : RelationalChoice. -Lemma guarded_rel_choice : - forall (A B:Type) (P:A -> Prop) (R:A -> B -> Prop), - (forall x:A, P x -> exists y : B, R x y) -> - exists R' : A -> B -> Prop, - (forall x:A, - P x -> - exists y : B, R x y /\ R' x y /\ (forall y':B, R' x y' -> y = y')). +Lemma guarded_rel_choice : GuardedRelationalChoice. Proof. apply (rel_choice_and_proof_irrel_imp_guarded_rel_choice rel_choice proof_irrel). @@ -78,16 +93,19 @@ Qed. Require Import Bool. -Lemma AC : +Lemma AC_bool_subset_to_bool : exists R : (bool -> Prop) -> bool -> Prop, (forall P:bool -> Prop, (exists b : bool, P b) -> exists b : bool, P b /\ R P b /\ (forall b':bool, R P b' -> b = b')). Proof. - apply guarded_rel_choice with - (P := fun Q:bool -> Prop => exists y : _, Q y) - (R := fun (Q:bool -> Prop) (y:bool) => Q y). - exact (fun _ H => H). + destruct (guarded_rel_choice _ _ + (fun Q:bool -> Prop => exists y : _, Q y) + (fun (Q:bool -> Prop) (y:bool) => Q y)) as (R,(HRsub,HR)). + exact (fun _ H => H). + exists R; intros P HP. + destruct (HR P HP) as (y,(Hy,Huni)). + exists y; firstorder. Qed. (** The proof of the excluded middle *) @@ -98,7 +116,7 @@ Proof. intro P. (** first we exhibit the choice functional relation R *) -destruct AC as [R H]. +destruct AC_bool_subset_to_bool as [R H]. set (class_of_true := fun b => b = true \/ P). set (class_of_false := fun b => b = false \/ P). @@ -135,4 +153,152 @@ left; assumption. Qed. -End PredExt_GuardRelChoice_imp_EM. +End PredExt_RelChoice_imp_EM. + +(**********************************************************************) +(** *** 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 *) + +Section ProofIrrel_RelChoice_imp_EqEM. + +Variable rel_choice : RelationalChoice. + +Variable proof_irrelevance : forall P:Prop , forall x y:P, x=y. + +(** Let [a1] and [a2] be two elements in some type [A] *) + +Variable A :Type. +Variables a1 a2 : A. + +(** We build the subset [A'] of [A] made of [a1] and [a2] *) + +Definition A' := sigT (fun x => x=a1 \/ x=a2). + +Definition a1':A'. +exists a1 ; auto. +Defined. + +Definition a2':A'. +exists a2 ; auto. +Defined. + +(** By proof-irrelevance, projection is a retraction *) + +Lemma projT1_injective : a1=a2 -> a1'=a2'. +Proof. + intro Heq ; unfold a1', a2', A'. + rewrite Heq. + replace (or_introl (a2=a2) (refl_equal a2)) + with (or_intror (a2=a2) (refl_equal a2)). + reflexivity. + apply proof_irrelevance. +Qed. + +(** But from the actual proofs of being in [A'], we can assert in the + proof-irrelevant world the existence of relevant boolean witnesses *) + +Lemma decide : forall x:A', exists y:bool , + (projT1 x = a1 /\ y = true ) \/ (projT1 x = a2 /\ y = false). +Proof. + intros [a [Ha1|Ha2]]; [exists true | exists false]; auto. +Qed. + +(** Thanks to the axiom of choice, the boolean witnesses move from the + propositional world to the relevant world *) + +Theorem proof_irrel_rel_choice_imp_eq_dec : a1=a2 \/ ~a1=a2. +Proof. + destruct + (rel_choice A' bool + (fun x y => projT1 x = a1 /\ y = true \/ projT1 x = a2 /\ y = false)) + as (R,(HRsub,HR)). + apply decide. + destruct (HR a1') as (b1,(Ha1'b1,_Huni1)). + destruct (HRsub a1' b1 Ha1'b1) as [(_, Hb1true)|(Ha1a2, _Hb1false)]. + destruct (HR a2') as (b2,(Ha2'b2,Huni2)). + destruct (HRsub a2' b2 Ha2'b2) as [(Ha2a1, _Hb2true)|(_, Hb2false)]. + left; symmetry; assumption. + right; intro H. + subst b1; subst b2. + rewrite (projT1_injective H) in Ha1'b1. + assert (false = true) by auto using Huni2. + discriminate. + left; assumption. +Qed. + +(** An alternative more concise proof can be done by directly using + the guarded relational choice *) + +Declare Implicit Tactic auto. + +Lemma proof_irrel_rel_choice_imp_eq_dec' : a1=a2 \/ ~a1=a2. +Proof. + assert (decide: forall x:A, x=a1 \/ x=a2 -> + exists y:bool, x=a1 /\ y=true \/ x=a2 /\ y=false). + intros a [Ha1|Ha2]; [exists true | exists false]; auto. + assert (guarded_rel_choice := + rel_choice_and_proof_irrel_imp_guarded_rel_choice + rel_choice + proof_irrelevance). + destruct + (guarded_rel_choice A bool + (fun x => x=a1 \/ x=a2) + (fun x y => x=a1 /\ y=true \/ x=a2 /\ y=false)) + as (R,(HRsub,HR)). + apply decide. + destruct (HR a1) as (b1,(Ha1b1,_Huni1)). left; reflexivity. + destruct (HRsub a1 b1 Ha1b1) as [(_, Hb1true)|(Ha1a2, _Hb1false)]. + destruct (HR a2) as (b2,(Ha2b2,Huni2)). right; reflexivity. + destruct (HRsub a2 b2 Ha2b2) as [(Ha2a1, _Hb2true)|(_, Hb2false)]. + left; symmetry; assumption. + right; intro H. + subst b1; subst b2; subst a1. + assert (false = true) by auto using Huni2, Ha1b1. + discriminate. + left; assumption. +Qed. + +End ProofIrrel_RelChoice_imp_EqEM. + +(**********************************************************************) +(** *** B. Extensional Hilbert's epsilon description operator -> Excluded-Middle *) + +(** Proof sketch from Bell [Bell93] (with thanks to P. Castéran) *) + +Notation Local "'inhabited' A" := A (at level 10, only parsing). + +Section ExtensionalEpsilon_imp_EM. + +Variable epsilon : forall A : Type, inhabited A -> (A -> Prop) -> A. + +Hypothesis epsilon_spec : + forall (A:Type) (i:inhabited A) (P:A->Prop), + (exists x, P x) -> P (epsilon A i P). + +Hypothesis epsilon_extensionality : + forall (A:Type) (i:inhabited A) (P Q:A->Prop), + (forall a, P a <-> Q a) -> epsilon A i P = epsilon A i Q. + +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. +Qed. + +End ExtensionalEpsilon_imp_EM. |