diff options
Diffstat (limited to 'theories/Logic')
| -rw-r--r-- | theories/Logic/ChoiceFacts.v | 425 |
1 files changed, 422 insertions, 3 deletions
diff --git a/theories/Logic/ChoiceFacts.v b/theories/Logic/ChoiceFacts.v index 2ab851e29..3f17ba5a9 100644 --- a/theories/Logic/ChoiceFacts.v +++ b/theories/Logic/ChoiceFacts.v @@ -22,7 +22,14 @@ 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 - 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 +52,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 +88,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 +100,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 +129,6 @@ Variables A B :Type. Variable P:A->Prop. -Variable R:A->B->Prop. - (** ** Constructive choice and description *) (** AC_rel *) @@ -121,6 +140,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 +171,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 y, R x y -> f x = f y). + +(** AC_fun_ext *) + +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 y : A, R x y -> f x = f y). + +(** AC_fun_ext_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 y : A, R x y -> S (f x) (f y)). + +(** AC_fun_ext_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 +306,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 +351,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 @@ -871,3 +971,322 @@ 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 *) + +Theorem gen_setoid_fun_choice_imp_setoid_fun_choice : + GeneralizedSetoidFunctionalChoice -> SetoidFunctionalChoice. +Proof. + intros GenSetoidFunChoice A B 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 : + SetoidFunctionalChoice -> GeneralizedSetoidFunctionalChoice. +Proof. + intros SetoidFunChoice A B 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. + +Theorem setoid_fun_choice_imp_simple_setoid_fun_choice : + SetoidFunctionalChoice -> SimpleSetoidFunctionalChoice. +Proof. + intros SetoidFunChoice A B 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 A B R T' Hequiv Hcompat Hexists) as (f,Hf). + exists f. firstorder. +Qed. + +Theorem simple_setoid_fun_choice_imp_setoid_fun_choice : + SimpleSetoidFunctionalChoice -> SetoidFunctionalChoice. +Proof. + intros SimpleSetoidFunChoice A B R T Hequiv Hcompat Hexists. + destruct (SimpleSetoidFunChoice A B R T Hequiv) as (f,Hf); firstorder. +Qed. + +(**********************************************************************) +(** ** AC_fun_setoid = AC! + AC_fun_repr *) + +Theorem setoid_fun_choice_imp_fun_choice : + SetoidFunctionalChoice -> FunctionalChoice. +Proof. + intros SetoidFunChoice A B 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 : + SetoidFunctionalChoice -> FunctionalRelReification. +Proof. + intro SetoidFunChoice. + intros A B; 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 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 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 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. |