diff options
Diffstat (limited to 'theories/Logic')
| -rw-r--r-- | theories/Logic/ChoiceFacts.v | 462 | ||||
| -rw-r--r-- | theories/Logic/ClassicalFacts.v | 66 | ||||
| -rw-r--r-- | theories/Logic/Diaconescu.v | 20 | ||||
| -rw-r--r-- | theories/Logic/ExtensionalFunctionRepresentative.v | 24 | ||||
| -rw-r--r-- | theories/Logic/PropExtensionality.v | 22 | ||||
| -rw-r--r-- | theories/Logic/PropExtensionalityFacts.v | 109 | ||||
| -rw-r--r-- | theories/Logic/SetoidChoice.v | 60 | ||||
| -rw-r--r-- | theories/Logic/vo.itarget | 5 |
8 files changed, 744 insertions, 24 deletions
diff --git a/theories/Logic/ChoiceFacts.v b/theories/Logic/ChoiceFacts.v index 1420a000b..07e8b6ef8 100644 --- a/theories/Logic/ChoiceFacts.v +++ b/theories/Logic/ChoiceFacts.v @@ -22,7 +22,16 @@ description principles - AC! = functional relation reification (known as axiom of unique choice in topos theory, sometimes called principle of definite description in - the context of constructive type theory) + the context of constructive type theory, sometimes + called axiom of no choice) + +- AC_fun_repr = functional choice of a representative in an equivalence class +- AC_fun_setoid_gen = functional form of the general form of the (so-called + extensional) axiom of choice over setoids +- AC_fun_setoid = functional form of the (so-called extensional) axiom of + choice from setoids +- AC_fun_setoid_simple = functional form of the (so-called extensional) axiom of + choice from setoids on locally compatible relations - GAC_rel = guarded relational form of the (non extensional) axiom of choice - GAC_fun = guarded functional form of the (non extensional) axiom of choice @@ -45,6 +54,11 @@ description principles independence of premises) - Drinker = drinker's paradox (small form) (called Ex in Bell [[Bell]]) +- EM = excluded-middle + +- Ext_pred_repr = choice of a representative among extensional predicates +- Ext_pred = extensionality of predicates +- Ext_fun_prop_repr = choice of a representative among extensional functions to Prop We let also @@ -76,6 +90,10 @@ Table of contents 8. Choice -> Dependent choice -> Countable choice +9.1. AC_fun_ext = AC_fun + Ext_fun_repr + EM + +9.2. AC_fun_ext = AC_fun + Ext_prop_fun_repr + PI + References: [[Bell]] John L. Bell, Choice principles in intuitionistic set theory, @@ -84,8 +102,13 @@ unpublished. [[Bell93]] John L. Bell, Hilbert's Epsilon Operator in Intuitionistic Type Theories, Mathematical Logic Quarterly, volume 39, 1993. +[[Carlström04]] Jesper Carlström, EM + Ext_ + AC_int is equivalent to +AC_ext, Mathematical Logic Quaterly, vol 50(3), pp 236-240, 2004. + [[Carlström05]] Jesper Carlström, Interpreting descriptions in intentional type theory, Journal of Symbolic Logic 70(2):488-514, 2005. + +[[Werner97]] Benjamin Werner, Sets in Types, Types in Sets, TACS, 1997. *) Set Implicit Arguments. @@ -108,8 +131,6 @@ Variables A B :Type. Variable P:A->Prop. -Variable R:A->B->Prop. - (** ** Constructive choice and description *) (** AC_rel *) @@ -121,6 +142,10 @@ Definition RelationalChoice_on := (** AC_fun *) +(* Note: This is called Type-Theoretic Description Axiom (TTDA) in + [[Werner97]] (using a non-standard meaning of "description"). This + is called intensional axiom of choice (AC_int) in [[Carlström04]] *) + Definition FunctionalChoice_on := forall R:A->B->Prop, (forall x : A, exists y : B, R x y) -> @@ -148,6 +173,55 @@ Definition FunctionalRelReification_on := (forall x : A, exists! y : B, R x y) -> (exists f : A->B, forall x : A, R x (f x)). +(** AC_fun_repr *) + +(* Note: This is called Type-Theoretic Choice Axiom (TTCA) in + [[Werner97]] (by reference to the extensional set-theoretic + formulation of choice); Note also a typo in its intended + formulation in [[Werner97]]. *) + +Require Import RelationClasses Logic. + +Definition RepresentativeFunctionalChoice_on := + forall R:A->A->Prop, + (Equivalence R) -> + (exists f : A->A, forall x : A, (R x (f x)) /\ forall x', R x x' -> f x = f x'). + +(** AC_fun_setoid *) + +Definition SetoidFunctionalChoice_on := + forall R : A -> A -> Prop, + forall T : A -> B -> Prop, + Equivalence R -> + (forall x x' y, R x x' -> T x y -> T x' y) -> + (forall x, exists y, T x y) -> + exists f : A -> B, forall x : A, T x (f x) /\ (forall x' : A, R x x' -> f x = f x'). + +(** AC_fun_setoid_gen *) + +(* Note: This is called extensional axiom of choice (AC_ext) in + [[Carlström04]]. *) + +Definition GeneralizedSetoidFunctionalChoice_on := + forall R : A -> A -> Prop, + forall S : B -> B -> Prop, + forall T : A -> B -> Prop, + Equivalence R -> + Equivalence S -> + (forall x x' y y', R x x' -> S y y' -> T x y -> T x' y') -> + (forall x, exists y, T x y) -> + exists f : A -> B, + forall x : A, T x (f x) /\ (forall x' : A, R x x' -> S (f x) (f x')). + +(** AC_fun_setoid_simple *) + +Definition SimpleSetoidFunctionalChoice_on A B := + forall R : A -> A -> Prop, + forall T : A -> B -> Prop, + Equivalence R -> + (forall x, exists y, forall x', R x x' -> T x' y) -> + exists f : A -> B, forall x : A, T x (f x) /\ (forall x' : A, R x x' -> f x = f x'). + (** ID_epsilon (constructive version of indefinite description; combined with proof-irrelevance, it may be connected to Carlström's type theory with a constructive indefinite description @@ -234,6 +308,14 @@ Notation FunctionalChoiceOnInhabitedSet := (forall A B : Type, inhabited B -> FunctionalChoice_on A B). Notation FunctionalRelReification := (forall A B : Type, FunctionalRelReification_on A B). +Notation RepresentativeFunctionalChoice := + (forall A : Type, RepresentativeFunctionalChoice_on A). +Notation SetoidFunctionalChoice := + (forall A B: Type, SetoidFunctionalChoice_on A B). +Notation GeneralizedSetoidFunctionalChoice := + (forall A B : Type, GeneralizedSetoidFunctionalChoice_on A B). +Notation SimpleSetoidFunctionalChoice := + (forall A B : Type, SimpleSetoidFunctionalChoice_on A B). Notation GuardedRelationalChoice := (forall A B : Type, GuardedRelationalChoice_on A B). @@ -271,6 +353,26 @@ Definition SmallDrinker'sParadox := forall (A:Type) (P:A -> Prop), inhabited A -> exists x, (exists x, P x) -> P x. +Definition ExcludedMiddle := + forall P:Prop, P \/ ~ P. + +(** Extensional schemes *) + +Local Notation ExtensionalPropositionRepresentative := + (forall (A:Type), + exists h : Prop -> Prop, + forall P : Prop, (P <-> h P) /\ forall Q, (P <-> Q) -> h P = h Q). + +Local Notation ExtensionalPredicateRepresentative := + (forall (A:Type), + exists h : (A->Prop) -> (A->Prop), + forall (P : A -> Prop), (forall x, P x <-> h P x) /\ forall Q, (forall x, P x <-> Q x) -> h P = h Q). + +Local Notation ExtensionalFunctionRepresentative := + (forall (A B:Type), + exists h : (A->B) -> (A->B), + forall (f : A -> B), (forall x, f x = h f x) /\ forall g, (forall x, f x = g x) -> h f = h g). + (**********************************************************************) (** * AC_rel + AC! = AC_fun @@ -284,7 +386,7 @@ Definition SmallDrinker'sParadox := relational formulation) without known inconsistency with classical logic, though functional relation reification conflicts with classical logic *) -Lemma description_rel_choice_imp_funct_choice : +Lemma functional_rel_reification_and_rel_choice_imp_fun_choice : forall A B : Type, FunctionalRelReification_on A B -> RelationalChoice_on A B -> FunctionalChoice_on A B. Proof. @@ -298,7 +400,10 @@ Proof. apply HR'R; assumption. Qed. -Lemma funct_choice_imp_rel_choice : +Notation description_rel_choice_imp_funct_choice := + functional_rel_reification_and_rel_choice_imp_fun_choice (compat "8.6"). + +Lemma fun_choice_imp_rel_choice : forall A B : Type, FunctionalChoice_on A B -> RelationalChoice_on A B. Proof. intros A B FunCh R H. @@ -311,7 +416,9 @@ Proof. trivial. Qed. -Lemma funct_choice_imp_description : +Notation funct_choice_imp_rel_choice := fun_choice_imp_rel_choice (compat "8.6"). + +Lemma fun_choice_imp_functional_rel_reification : forall A B : Type, FunctionalChoice_on A B -> FunctionalRelReification_on A B. Proof. intros A B FunCh R H. @@ -324,17 +431,21 @@ Proof. exists f; exact H0. Qed. -Corollary FunChoice_Equiv_RelChoice_and_ParamDefinDescr : +Notation funct_choice_imp_description := fun_choice_imp_functional_rel_reification (compat "8.6"). + +Corollary fun_choice_iff_rel_choice_and_functional_rel_reification : forall A B : Type, FunctionalChoice_on A B <-> RelationalChoice_on A B /\ FunctionalRelReification_on A B. Proof. intros A B. split. intro H; split; - [ exact (funct_choice_imp_rel_choice H) - | exact (funct_choice_imp_description H) ]. - intros [H H0]; exact (description_rel_choice_imp_funct_choice H0 H). + [ exact (fun_choice_imp_rel_choice H) + | exact (fun_choice_imp_functional_rel_reification H) ]. + intros [H H0]; exact (functional_rel_reification_and_rel_choice_imp_fun_choice H0 H). Qed. +Notation FunChoice_Equiv_RelChoice_and_ParamDefinDescr := + fun_choice_iff_rel_choice_and_functional_rel_reification (compat "8.6"). (**********************************************************************) (** * Connection between the guarded, non guarded and omniscient choices *) @@ -862,3 +973,334 @@ Proof. rewrite Heq in HR. assumption. Qed. + +(**********************************************************************) +(** * About the axiom of choice over setoids *) + +Require Import ClassicalFacts PropExtensionalityFacts. + +(**********************************************************************) +(** ** Consequences of the choice of a representative in an equivalence class *) + +Theorem repr_fun_choice_imp_ext_prop_repr : + RepresentativeFunctionalChoice -> ExtensionalPropositionRepresentative. +Proof. + intros ReprFunChoice A. + pose (R P Q := P <-> Q). + assert (Hequiv:Equivalence R) by (split; firstorder). + apply (ReprFunChoice _ R Hequiv). +Qed. + +Theorem repr_fun_choice_imp_ext_pred_repr : + RepresentativeFunctionalChoice -> ExtensionalPredicateRepresentative. +Proof. + intros ReprFunChoice A. + pose (R P Q := forall x : A, P x <-> Q x). + assert (Hequiv:Equivalence R) by (split; firstorder). + apply (ReprFunChoice _ R Hequiv). +Qed. + +Theorem repr_fun_choice_imp_ext_function_repr : + RepresentativeFunctionalChoice -> ExtensionalFunctionRepresentative. +Proof. + intros ReprFunChoice A B. + pose (R (f g : A -> B) := forall x : A, f x = g x). + assert (Hequiv:Equivalence R). + { split; try easy. firstorder using eq_trans. } + apply (ReprFunChoice _ R Hequiv). +Qed. + +(** *** This is a variant of Diaconescu and Goodman-Myhill theorems *) + +Theorem repr_fun_choice_imp_excluded_middle : + RepresentativeFunctionalChoice -> ExcludedMiddle. +Proof. + intros ReprFunChoice. + apply representative_boolean_partition_imp_excluded_middle, ReprFunChoice. +Qed. + +Theorem repr_fun_choice_imp_relational_choice : + RepresentativeFunctionalChoice -> RelationalChoice. +Proof. + intros ReprFunChoice A B T Hexists. + pose (D := (A*B)%type). + pose (R (z z':D) := + let x := fst z in + let x' := fst z' in + let y := snd z in + let y' := snd z' in + x = x' /\ (T x y -> y = y' \/ T x y') /\ (T x y' -> y = y' \/ T x y)). + assert (Hequiv : Equivalence R). + { split. + - split. easy. firstorder. + - intros (x,y) (x',y') (H1,(H2,H2')). split. easy. simpl fst in *. simpl snd in *. + subst x'. split; intro H. + + destruct (H2' H); firstorder. + + destruct (H2 H); firstorder. + - intros (x,y) (x',y') (x'',y'') (H1,(H2,H2')) (H3,(H4,H4')). + simpl fst in *. simpl snd in *. subst x'' x'. split. easy. split; intro H. + + simpl fst in *. simpl snd in *. destruct (H2 H) as [<-|H0]. + * destruct (H4 H); firstorder. + * destruct (H2' H0), (H4 H0); try subst y'; try subst y''; try firstorder. + + simpl fst in *. simpl snd in *. destruct (H4' H) as [<-|H0]. + * destruct (H2' H); firstorder. + * destruct (H2' H0), (H4 H0); try subst y'; try subst y''; try firstorder. } + destruct (ReprFunChoice D R Hequiv) as (g,Hg). + set (T' x y := T x y /\ exists y', T x y' /\ g (x,y') = (x,y)). + exists T'. split. + - intros x y (H,_); easy. + - intro x. destruct (Hexists x) as (y,Hy). + exists (snd (g (x,y))). + destruct (Hg (x,y)) as ((Heq1,(H',H'')),Hgxyuniq); clear Hg. + destruct (H' Hy) as [Heq2|Hgy]; clear H'. + + split. split. + * rewrite <- Heq2. assumption. + * exists y. destruct (g (x,y)) as (x',y'). simpl in Heq1, Heq2. subst; easy. + * intros y' (Hy',(y'',(Hy'',Heq))). + rewrite (Hgxyuniq (x,y'')), Heq. easy. split. easy. + split; right; easy. + + split. split. + * assumption. + * exists y. destruct (g (x,y)) as (x',y'). simpl in Heq1. subst x'; easy. + * intros y' (Hy',(y'',(Hy'',Heq))). + rewrite (Hgxyuniq (x,y'')), Heq. easy. split. easy. + split; right; easy. +Qed. + +(**********************************************************************) +(** ** AC_fun_setoid = AC_fun_setoid_gen = AC_fun_setoid_simple *) + +Theorem gen_setoid_fun_choice_imp_setoid_fun_choice : + forall A B, GeneralizedSetoidFunctionalChoice_on A B -> SetoidFunctionalChoice_on A B. +Proof. + intros A B GenSetoidFunChoice R T Hequiv Hcompat Hex. + apply GenSetoidFunChoice; try easy. + apply eq_equivalence. + intros * H <-. firstorder. +Qed. + +Theorem setoid_fun_choice_imp_gen_setoid_fun_choice : + forall A B, SetoidFunctionalChoice_on A B -> GeneralizedSetoidFunctionalChoice_on A B. +Proof. + intros A B SetoidFunChoice R S T HequivR HequivS Hcompat Hex. + destruct SetoidFunChoice with (R:=R) (T:=T) as (f,Hf); try easy. + { intros; apply (Hcompat x x' y y); try easy. } + exists f. intros x; specialize Hf with x as (Hf,Huniq). intuition. now erewrite Huniq. +Qed. + +Corollary setoid_fun_choice_iff_gen_setoid_fun_choice : + forall A B, SetoidFunctionalChoice_on A B <-> GeneralizedSetoidFunctionalChoice_on A B. +Proof. + split; auto using gen_setoid_fun_choice_imp_setoid_fun_choice, setoid_fun_choice_imp_gen_setoid_fun_choice. +Qed. + +Theorem setoid_fun_choice_imp_simple_setoid_fun_choice : + forall A B, SetoidFunctionalChoice_on A B -> SimpleSetoidFunctionalChoice_on A B. +Proof. + intros A B SetoidFunChoice R T Hequiv Hexists. + pose (T' x y := forall x', R x x' -> T x' y). + assert (Hcompat : forall (x x' : A) (y : B), R x x' -> T' x y -> T' x' y) by firstorder. + destruct (SetoidFunChoice R T' Hequiv Hcompat Hexists) as (f,Hf). + exists f. firstorder. +Qed. + +Theorem simple_setoid_fun_choice_imp_setoid_fun_choice : + forall A B, SimpleSetoidFunctionalChoice_on A B -> SetoidFunctionalChoice_on A B. +Proof. + intros A B SimpleSetoidFunChoice R T Hequiv Hcompat Hexists. + destruct (SimpleSetoidFunChoice R T Hequiv) as (f,Hf); firstorder. +Qed. + +Corollary setoid_fun_choice_iff_simple_setoid_fun_choice : + forall A B, SetoidFunctionalChoice_on A B <-> SimpleSetoidFunctionalChoice_on A B. +Proof. + split; auto using simple_setoid_fun_choice_imp_setoid_fun_choice, setoid_fun_choice_imp_simple_setoid_fun_choice. +Qed. + +(**********************************************************************) +(** ** AC_fun_setoid = AC! + AC_fun_repr *) + +Theorem setoid_fun_choice_imp_fun_choice : + forall A B, SetoidFunctionalChoice_on A B -> FunctionalChoice_on A B. +Proof. + intros A B SetoidFunChoice T Hexists. + destruct SetoidFunChoice with (R:=@eq A) (T:=T) as (f,Hf). + - apply eq_equivalence. + - now intros * ->. + - assumption. + - exists f. firstorder. +Qed. + +Corollary setoid_fun_choice_imp_functional_rel_reification : + forall A B, SetoidFunctionalChoice_on A B -> FunctionalRelReification_on A B. +Proof. + intros A B SetoidFunChoice. + apply fun_choice_imp_functional_rel_reification. + now apply setoid_fun_choice_imp_fun_choice. +Qed. + +Theorem setoid_fun_choice_imp_repr_fun_choice : + SetoidFunctionalChoice -> RepresentativeFunctionalChoice . +Proof. + intros SetoidFunChoice A R Hequiv. + apply SetoidFunChoice; firstorder. +Qed. + +Theorem functional_rel_reification_and_repr_fun_choice_imp_setoid_fun_choice : + FunctionalRelReification -> RepresentativeFunctionalChoice -> SetoidFunctionalChoice. +Proof. + intros FunRelReify ReprFunChoice A B R T Hequiv Hcompat Hexists. + assert (FunChoice : FunctionalChoice). + { intros A' B'. apply functional_rel_reification_and_rel_choice_imp_fun_choice. + - apply FunRelReify. + - now apply repr_fun_choice_imp_relational_choice. } + destruct (FunChoice _ _ T Hexists) as (f,Hf). + destruct (ReprFunChoice A R Hequiv) as (g,Hg). + exists (fun a => f (g a)). + intro x. destruct (Hg x) as (Hgx,HRuniq). + split. + - eapply Hcompat. symmetry. apply Hgx. apply Hf. + - intros y Hxy. f_equal. auto. +Qed. + +Theorem functional_rel_reification_and_repr_fun_choice_iff_setoid_fun_choice : + FunctionalRelReification /\ RepresentativeFunctionalChoice <-> SetoidFunctionalChoice. +Proof. + split; intros. + - now apply functional_rel_reification_and_repr_fun_choice_imp_setoid_fun_choice. + - split. + + now intros A B; apply setoid_fun_choice_imp_functional_rel_reification. + + now apply setoid_fun_choice_imp_repr_fun_choice. +Qed. + +(** Note: What characterization to give of +RepresentativeFunctionalChoice? A formulation of it as a functional +relation would certainly be equivalent to the formulation of +SetoidFunctionalChoice as a functional relation, but in their +functional forms, SetoidFunctionalChoice seems strictly stronger *) + +(**********************************************************************) +(** * AC_fun_setoid = AC_fun + Ext_fun_repr + EM *) + +Import EqNotations. + +(** ** This is the main theorem in [[Carlström04]] *) + +(** Note: all ingredients have a computational meaning when taken in + separation. However, to compute with the functional choice, + existential quantification has to be thought as a strong + existential, which is incompatible with the computational content of + excluded-middle *) + +Theorem fun_choice_and_ext_functions_repr_and_excluded_middle_imp_setoid_fun_choice : + FunctionalChoice -> ExtensionalFunctionRepresentative -> ExcludedMiddle -> RepresentativeFunctionalChoice. +Proof. + intros FunChoice SetoidFunRepr EM A R (Hrefl,Hsym,Htrans). + assert (H:forall P:Prop, exists b, b = true <-> P). + { intros P. destruct (EM P). + - exists true; firstorder. + - exists false; easy. } + destruct (FunChoice _ _ _ H) as (c,Hc). + pose (class_of a y := c (R a y)). + pose (isclass f := exists x:A, f x = true). + pose (class := {f:A -> bool | isclass f}). + pose (contains (c:class) (a:A) := proj1_sig c a = true). + destruct (FunChoice class A contains) as (f,Hf). + - intros f. destruct (proj2_sig f) as (x,Hx). + exists x. easy. + - destruct (SetoidFunRepr A bool) as (h,Hh). + assert (Hisclass:forall a, isclass (h (class_of a))). + { intro a. exists a. destruct (Hh (class_of a)) as (Ha,Huniqa). + rewrite <- Ha. apply Hc. apply Hrefl. } + pose (f':= fun a => exist _ (h (class_of a)) (Hisclass a) : class). + exists (fun a => f (f' a)). + intros x. destruct (Hh (class_of x)) as (Hx,Huniqx). split. + + specialize Hf with (f' x). unfold contains in Hf. simpl in Hf. rewrite <- Hx in Hf. apply Hc. assumption. + + intros y Hxy. + f_equal. + assert (Heq1: h (class_of x) = h (class_of y)). + { apply Huniqx. intro z. unfold class_of. + destruct (c (R x z)) eqn:Hxz. + - symmetry. apply Hc. apply -> Hc in Hxz. firstorder. + - destruct (c (R y z)) eqn:Hyz. + + apply -> Hc in Hyz. rewrite <- Hxz. apply Hc. firstorder. + + easy. } + assert (Heq2:rew Heq1 in Hisclass x = Hisclass y). + { apply proof_irrelevance_cci, EM. } + unfold f'. + rewrite <- Heq2. + rewrite <- Heq1. + reflexivity. +Qed. + +Theorem setoid_functional_choice_first_characterization : + FunctionalChoice /\ ExtensionalFunctionRepresentative /\ ExcludedMiddle <-> SetoidFunctionalChoice. +Proof. + split. + - intros (FunChoice & SetoidFunRepr & EM). + apply functional_rel_reification_and_repr_fun_choice_imp_setoid_fun_choice. + + intros A B. apply fun_choice_imp_functional_rel_reification, FunChoice. + + now apply fun_choice_and_ext_functions_repr_and_excluded_middle_imp_setoid_fun_choice. + - intro SetoidFunChoice. repeat split. + + now intros A B; apply setoid_fun_choice_imp_fun_choice. + + apply repr_fun_choice_imp_ext_function_repr. + now apply setoid_fun_choice_imp_repr_fun_choice. + + apply repr_fun_choice_imp_excluded_middle. + now apply setoid_fun_choice_imp_repr_fun_choice. +Qed. + +(**********************************************************************) +(** ** AC_fun_setoid = AC_fun + Ext_pred_repr + PI *) + +(** Note: all ingredients have a computational meaning when taken in + separation. However, to compute with the functional choice, + existential quantification has to be thought as a strong + existential, which is incompatible with proof-irrelevance which + requires existential quantification to be truncated *) + +Theorem fun_choice_and_ext_pred_ext_and_proof_irrel_imp_setoid_fun_choice : + FunctionalChoice -> ExtensionalPredicateRepresentative -> ProofIrrelevance -> RepresentativeFunctionalChoice. +Proof. + intros FunChoice PredExtRepr PI A R (Hrefl,Hsym,Htrans). + pose (isclass P := exists x:A, P x). + pose (class := {P:A -> Prop | isclass P}). + pose (contains (c:class) (a:A) := proj1_sig c a). + pose (class_of a := R a). + destruct (FunChoice class A contains) as (f,Hf). + - intros c. apply proj2_sig. + - destruct (PredExtRepr A) as (h,Hh). + assert (Hisclass:forall a, isclass (h (class_of a))). + { intro a. exists a. destruct (Hh (class_of a)) as (Ha,Huniqa). + rewrite <- Ha; apply Hrefl. } + pose (f':= fun a => exist _ (h (class_of a)) (Hisclass a) : class). + exists (fun a => f (f' a)). + intros x. destruct (Hh (class_of x)) as (Hx,Huniqx). split. + + specialize Hf with (f' x). simpl in Hf. rewrite <- Hx in Hf. assumption. + + intros y Hxy. + f_equal. + assert (Heq1: h (class_of x) = h (class_of y)). + { apply Huniqx. intro z. unfold class_of. firstorder. } + assert (Heq2:rew Heq1 in Hisclass x = Hisclass y). + { apply PI. } + unfold f'. + rewrite <- Heq2. + rewrite <- Heq1. + reflexivity. +Qed. + +Theorem setoid_functional_choice_second_characterization : + FunctionalChoice /\ ExtensionalPredicateRepresentative /\ ProofIrrelevance <-> SetoidFunctionalChoice. +Proof. + split. + - intros (FunChoice & ExtPredRepr & PI). + apply functional_rel_reification_and_repr_fun_choice_imp_setoid_fun_choice. + + intros A B. now apply fun_choice_imp_functional_rel_reification. + + now apply fun_choice_and_ext_pred_ext_and_proof_irrel_imp_setoid_fun_choice. + - intro SetoidFunChoice. repeat split. + + now intros A B; apply setoid_fun_choice_imp_fun_choice. + + apply repr_fun_choice_imp_ext_pred_repr. + now apply setoid_fun_choice_imp_repr_fun_choice. + + red. apply proof_irrelevance_cci. + apply repr_fun_choice_imp_excluded_middle. + now apply setoid_fun_choice_imp_repr_fun_choice. +Qed. diff --git a/theories/Logic/ClassicalFacts.v b/theories/Logic/ClassicalFacts.v index afd64efdf..021408a37 100644 --- a/theories/Logic/ClassicalFacts.v +++ b/theories/Logic/ClassicalFacts.v @@ -34,8 +34,11 @@ Table of contents: 3 3. Independence of general premises and drinker's paradox -4. Classical logic and principle of unrestricted minimization +4. Principles equivalent to classical logic +4.1 Classical logic = principle of unrestricted minimization + +4.2 Classical logic = choice of representatives in a partition of bool *) (************************************************************************) @@ -94,12 +97,14 @@ Qed. (** A weakest form of propositional extensionality: extensionality for provable propositions only *) +Require Import PropExtensionalityFacts. + Definition provable_prop_extensionality := forall A:Prop, A -> A = True. Lemma provable_prop_ext : prop_extensionality -> provable_prop_extensionality. Proof. - intros Ext A Ha; apply Ext; split; trivial. + exact PropExt_imp_ProvPropExt. Qed. (************************************************************************) @@ -516,7 +521,7 @@ End Weak_proof_irrelevance_CCI. (** ** Weak excluded-middle *) (** The weak classical logic based on [~~A \/ ~A] is referred to with - name KC in {[ChagrovZakharyaschev97]] + name KC in [[ChagrovZakharyaschev97]] [[ChagrovZakharyaschev97]] Alexander Chagrov and Michael Zakharyaschev, "Modal Logic", Clarendon Press, 1997. @@ -661,6 +666,8 @@ Proof. exists x0; exact Hnot. Qed. +(** * Axioms equivalent to classical logic *) + (** ** Principle of unrestricted minimization *) Require Import Coq.Arith.PeanoNat. @@ -736,3 +743,56 @@ Section Example_of_undecidable_predicate_with_the_minimization_property. Qed. End Example_of_undecidable_predicate_with_the_minimization_property. + +(** ** Choice of representatives in a partition of bool *) + +(** This is similar to Bell's "weak extensional selection principle" in [[Bell]] + + [[Bell]] John L. Bell, Choice principles in intuitionistic set theory, unpublished. +*) + +Require Import RelationClasses. + +Local Notation representative_boolean_partition := + (forall R:bool->bool->Prop, + Equivalence R -> exists f, forall x, R x (f x) /\ forall y, R x y -> f x = f y). + +Theorem representative_boolean_partition_imp_excluded_middle : + representative_boolean_partition -> excluded_middle. +Proof. + intros ReprFunChoice P. + pose (R (b1 b2 : bool) := b1 = b2 \/ P). + assert (Equivalence R). + { split. + - now left. + - destruct 1. now left. now right. + - destruct 1, 1; try now right. left; now transitivity y. } + destruct (ReprFunChoice R H) as (f,Hf). clear H. + destruct (Bool.bool_dec (f true) (f false)) as [Heq|Hneq]. + + left. + destruct (Hf false) as ([Hfalse|HP],_); try easy. + destruct (Hf true) as ([Htrue|HP],_); try easy. + congruence. + + right. intro HP. + destruct (Hf true) as (_,H). apply Hneq, H. now right. +Qed. + +Theorem excluded_middle_imp_representative_boolean_partition : + excluded_middle -> representative_boolean_partition. +Proof. + intros EM R H. + destruct (EM (R true false)). + - exists (fun _ => true). + intros []; firstorder. + - exists (fun b => b). + intro b. split. + + reflexivity. + + destruct b, y; intros HR; easy || now symmetry in HR. +Qed. + +Theorem excluded_middle_iff_representative_boolean_partition : + excluded_middle <-> representative_boolean_partition. +Proof. + split; auto using excluded_middle_imp_representative_boolean_partition, + representative_boolean_partition_imp_excluded_middle. +Qed. diff --git a/theories/Logic/Diaconescu.v b/theories/Logic/Diaconescu.v index 23af5afc6..896be7c33 100644 --- a/theories/Logic/Diaconescu.v +++ b/theories/Logic/Diaconescu.v @@ -8,9 +8,9 @@ (************************************************************************) (** Diaconescu showed that the Axiom of Choice entails Excluded-Middle - in topoi [Diaconescu75]. Lacas and Werner adapted the proof to show + 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]. + Excluded-Middle in Type Theory [[LacasWerner99]]. Three variants of Diaconescu's result in type theory are shown below. @@ -23,22 +23,22 @@ Benjamin Werner) C. A proof that extensional Hilbert epsilon's description operator - entails excluded-middle (taken from Bell [Bell93]) + entails excluded-middle (taken from Bell [[Bell93]]) - See also [Carlström] for a discussion of the connection between the + See also [[Carlström04]] for a discussion of the connection between the Extensional Axiom of Choice and Excluded-Middle - [Diaconescu75] Radu Diaconescu, Axiom of Choice and Complementation, + [[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 + [[LacasWerner99]] Samuel Lacas, Benjamin Werner, Which Choices imply the excluded middle?, preprint, 1999. - [Bell93] John L. Bell, Hilbert's epsilon operator and classical + [[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. + [[Carlström04]] Jesper Carlström, EM + Ext_ + AC_int is equivalent + to AC_ext, Mathematical Logic Quaterly, vol 50(3), pp 236-240, 2004. *) (**********************************************************************) @@ -263,7 +263,7 @@ End ProofIrrel_RelChoice_imp_EqEM. (**********************************************************************) (** * Extensional Hilbert's epsilon description operator -> Excluded-Middle *) -(** Proof sketch from Bell [Bell93] (with thanks to P. Castéran) *) +(** Proof sketch from Bell [[Bell93]] (with thanks to P. Castéran) *) Local Notation inhabited A := A (only parsing). diff --git a/theories/Logic/ExtensionalFunctionRepresentative.v b/theories/Logic/ExtensionalFunctionRepresentative.v new file mode 100644 index 000000000..a9da68e16 --- /dev/null +++ b/theories/Logic/ExtensionalFunctionRepresentative.v @@ -0,0 +1,24 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(** This module states a limited form axiom of functional + extensionality which selects a canonical representative in each + class of extensional functions *) + +(** Its main interest is that it is the needed ingredient to provide + axiom of choice on setoids (a.k.a. axiom of extensional choice) + when combined with classical logic and axiom of (intensonal) + choice *) + +(** It provides extensionality of functions while still supporting (a + priori) an intensional interpretation of equality *) + +Axiom extensional_function_representative : + forall A B, exists repr, forall (f : A -> B), + (forall x, f x = repr f x) /\ + (forall g, (forall x, f x = g x) -> repr f = repr g). diff --git a/theories/Logic/PropExtensionality.v b/theories/Logic/PropExtensionality.v new file mode 100644 index 000000000..796c60273 --- /dev/null +++ b/theories/Logic/PropExtensionality.v @@ -0,0 +1,22 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(** This module states propositional extensionality and draws + consequences of it *) + +Axiom propositional_extensionality : + forall (P Q : Prop), (P <-> Q) -> P = Q. + +Require Import ClassicalFacts. + +Theorem proof_irrelevance : forall (P:Prop) (p1 p2:P), p1 = p2. +Proof. + apply ext_prop_dep_proof_irrel_cic. + exact propositional_extensionality. +Qed. + diff --git a/theories/Logic/PropExtensionalityFacts.v b/theories/Logic/PropExtensionalityFacts.v new file mode 100644 index 000000000..7e455dfa1 --- /dev/null +++ b/theories/Logic/PropExtensionalityFacts.v @@ -0,0 +1,109 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(** Some facts and definitions about propositional and predicate extensionality + +We investigate the relations between the following extensionality principles + +- Proposition extensionality +- Predicate extensionality +- Propositional functional extensionality +- Provable-proposition extensionality +- Refutable-proposition extensionality +- Extensional proposition representatives +- Extensional predicate representatives +- Extensional propositional function representatives + +Table of contents + +1. Definitions + +2.1 Predicate extensionality <-> Proposition extensionality + Propositional functional extensionality + +2.2 Propositional extensionality -> Provable propositional extensionality + +2.3 Propositional extensionality -> Refutable propositional extensionality + +*) + +Set Implicit Arguments. + +(**********************************************************************) +(** * Definitions *) + +(** Propositional extensionality *) + +Local Notation PropositionalExtensionality := + (forall A B : Prop, (A <-> B) -> A = B). + +(** Provable-proposition extensionality *) + +Local Notation ProvablePropositionExtensionality := + (forall A:Prop, A -> A = True). + +(** Refutable-proposition extensionality *) + +Local Notation RefutablePropositionExtensionality := + (forall A:Prop, ~A -> A = False). + +(** Predicate extensionality *) + +Local Notation PredicateExtensionality := + (forall (A:Type) (P Q : A -> Prop), (forall x, P x <-> Q x) -> P = Q). + +(** Propositional functional extensionality *) + +Local Notation PropositionalFunctionalExtensionality := + (forall (A:Type) (P Q : A -> Prop), (forall x, P x = Q x) -> P = Q). + +(**********************************************************************) +(** * Propositional and predicate extensionality *) + +(**********************************************************************) +(** ** Predicate extensionality <-> Propositional extensionality + Propositional functional extensionality *) + +Lemma PredExt_imp_PropExt : PredicateExtensionality -> PropositionalExtensionality. +Proof. + intros Ext A B Equiv. + change A with ((fun _ => A) I). + now rewrite Ext with (P := fun _ : True =>A) (Q := fun _ => B). +Qed. + +Lemma PredExt_imp_PropFunExt : PredicateExtensionality -> PropositionalFunctionalExtensionality. +Proof. + intros Ext A P Q Eq. apply Ext. intros x. now rewrite (Eq x). +Qed. + +Lemma PropExt_and_PropFunExt_imp_PredExt : + PropositionalExtensionality -> PropositionalFunctionalExtensionality -> PredicateExtensionality. +Proof. + intros Ext FunExt A P Q Equiv. + apply FunExt. intros x. now apply Ext. +Qed. + +Theorem PropExt_and_PropFunExt_iff_PredExt : + PropositionalExtensionality /\ PropositionalFunctionalExtensionality <-> PredicateExtensionality. +Proof. + firstorder using PredExt_imp_PropExt, PredExt_imp_PropFunExt, PropExt_and_PropFunExt_imp_PredExt. +Qed. + +(**********************************************************************) +(** ** Propositional extensionality and provable proposition extensionality *) + +Lemma PropExt_imp_ProvPropExt : PropositionalExtensionality -> ProvablePropositionExtensionality. +Proof. + intros Ext A Ha; apply Ext; split; trivial. +Qed. + +(**********************************************************************) +(** ** Propositional extensionality and refutable proposition extensionality *) + +Lemma PropExt_imp_RefutPropExt : PropositionalExtensionality -> RefutablePropositionExtensionality. +Proof. + intros Ext A Ha; apply Ext; split; easy. +Qed. diff --git a/theories/Logic/SetoidChoice.v b/theories/Logic/SetoidChoice.v new file mode 100644 index 000000000..84432dda1 --- /dev/null +++ b/theories/Logic/SetoidChoice.v @@ -0,0 +1,60 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(** This module states the functional form of the axiom of choice over + setoids, commonly called extensional axiom of choice [[Carlström04]], + [[Martin-Löf05]]. This is obtained by a decomposition of the axiom + into the following components: + + - classical logic + - relational axiom of choice + - axiom of unique choice + - a limited form of functional extensionality + + Among other results, it entails: + - proof irrelevance + - choice of a representative in equivalence classes + + [[Carlström04]] Jesper Carlström, EM + Ext_ + AC_int is equivalent to + AC_ext, Mathematical Logic Quaterly, vol 50(3), pp 236-240, 2004. + + [[Martin-Löf05] Per Martin-Löf, 100 years of Zermelo’s axiom of + choice: what was the problem with it?, lecture notes for KTH/SU + colloquium, 2005. + +*) + +Require Export ClassicalChoice. (* classical logic, relational choice, unique choice *) +Require Export ExtensionalFunctionRepresentative. + +Require Import ChoiceFacts. +Require Import ClassicalFacts. +Require Import RelationClasses. + +Theorem setoid_choice : + forall A B, + forall R : A -> A -> Prop, + forall T : A -> B -> Prop, + Equivalence R -> + (forall x x' y, R x x' -> T x y -> T x' y) -> + (forall x, exists y, T x y) -> + exists f : A -> B, forall x : A, T x (f x) /\ (forall x' : A, R x x' -> f x = f x'). +Proof. + apply setoid_functional_choice_first_characterization. split; [|split]. + - exact choice. + - exact extensional_function_representative. + - exact classic. +Qed. + +Theorem representative_choice : + forall A (R:A->A->Prop), (Equivalence R) -> + exists f : A->A, forall x : A, R x (f x) /\ forall x', R x x' -> f x = f x'. +Proof. + apply setoid_fun_choice_imp_repr_fun_choice. + exact setoid_choice. +Qed. diff --git a/theories/Logic/vo.itarget b/theories/Logic/vo.itarget index 323597395..ef2709b47 100644 --- a/theories/Logic/vo.itarget +++ b/theories/Logic/vo.itarget @@ -20,11 +20,14 @@ WeakFan.vo WKL.vo FunctionalExtensionality.vo ExtensionalityFacts.vo +ExtensionalFunctionRepresentative.vo Hurkens.vo IndefiniteDescription.vo JMeq.vo ProofIrrelevanceFacts.vo ProofIrrelevance.vo +PropExtensionality.vo RelationalChoice.vo SetIsType.vo -FinFun.vo
\ No newline at end of file +SetoidChoice.vo +FinFun.vo |