(************************************************************) (* *) (* How to derive Proof-Irelevance from *) (* the Excluded Middle in an Impredicative Universe *) (* *) (************************************************************) (* The goal of these exercices is to show a version of * Girard/Hurkens's paradox and use it to show that * Proof Irrelevance follows from Classical Logic in the sort [Prop]: [forall (Bool : Prop) (TT FF : Bool), (forall P : Prop, P \/ ~ P) -> FF = TT] *) (* The method is to use Girard/Hurkens paradox * in order to derive a contradiction from the excluded middle * and a type [Bool : Prop] with at least two distinct inhabitants * (say [TT] and [FF]). *) (* The whole development is adaptable to show * the "inconsistency" (ie: every type is inhabited) * of the sort [Set] with the -impredicative-set option * in presence of the excluded middle in [Set]. * In this case, we could have taken the usual [bool : Set] * for [Bool]. That [true] and [false] are distinct values * is provided by strong eliminations from sort [Set] to sort [Type]. * * We use here [Bool : Prop] rather than [bool : Set] * for reasons related to the existence of paradoxes * like the present one. * It has been chosen to allow Classical Logic in [Prop], * and thus Proof Irrelevance in [Prop]. * Since [Set] and [Type] are proof relevant * (typically [~ false = true], with [false, true : bool : Set]), * it is in general forbided to eliminate a type in [Prop] with at least * two distinct inhabitants to a type in [Set] or [Type]. * We come back on this point in [Section EM_imp_PI] below. *) (* The following development is inspired from Sorensen & Urzyczyn, * where standard references can be found * (Section 14.6 of "Lectures on the Curry Howard Isomorphism", * vol. 149 of "Studies in Logic and the Foundations * of Mathematics", 2006). * * Similar developments are available in Coq's standard library. * See for instance [Coq.Logic.Berardi] and [Coq.Logic.Hurkens] *) (* A first easy exercise: *) (* - Question - *) (* --- Give a proof term of the following: *) Definition FiffT_imp_False : forall P, ~ (~ P <-> P) := ... (**************************) (* *) (* Cantor's paradox *) (* *) (**************************) (* We assume given a universe [U : Prop] * together with a logical retraction * from the powerset [Pow U] of [U] to [U]. * * For the moment, we let [Pow A] = [A -> Prop]. * * The retraction from [Pow U] to [U] is given by * [el : (Pow U) -> U] * and [set : U -> (Pow U)] * such that there is a [set_el_equiv] of type [forall (X : Pow U) (a : U), (X a <-> set (el X) a)] * * The idea of this formalization is that [set : U -> U -> Prop] * is a kind of membership relation, by which the predicate [set b a : Prop] * must be thought of as "[a : U] 'belongs' to [b : U]". * * Hence [set] maps a set [a : U] of the universe [U] to * the set of its elements [set a : Pow U], which is a subset of [U]. * * [el : (Pow U) -> U] is the converse operation: it assigns * an inhabitant [el X : U] of the universe [U] to a familly [X : Pow U] * of elements of [U]. * * The assumption [set_el_equiv] of type [forall (X : Pow U) (a : U), (X a <-> set (el X) a)] * is sufficent to derive Cantor's paradox. *) Section CantorParadox. Notation "'Pow' A" := (A -> Prop) (at level 70, no associativity). Variable U : Prop. Variable el : (Pow U) -> U. Variable set : U -> (Pow U). Hypothesis set_el_equiv : forall (X : Pow U) (a : U), (X a <-> set (el X) a). (* - Question - *) (* --- Define [D : Pow U], * the set of sets that do not belong to themselves *) Let D : Pow U := ... (* Consider now the element of [U] that [el] assigns to * the familly [D : Pow U]: *) Let e : U := el D. Check (set_el_equiv D e : (~(set e e) <-> (set e e))). (* - Question - *) (* --- Show that our assumptions are contradictory *) Lemma cantor : False. Proof. ... Qed. End CantorParadox. Check cantor. (* - Remark - *) (* --- Cantor's paradox can easily be adapted * to a boolean powerset: [Pow A] = [A -> bool] *) (**********************************) (* *) (* Girard/Hurkens's paradox *) (* *) (**********************************) (* The version of Girard/Hurkens paradox that we will present * is based on a Cantor paradox on a boolean powerset [Pow A] = [A -> Bool] * where [Bool : Prop] is a form of retract * (wrt logical equivalence) of [Prop] *) Section BooleanReflection_in_Prop. (* We assume given a type with two distinct inhabitants *) Variable Bool : Prop. Variable TT FF : Bool. Hypothesis NonConf : FF = TT -> False. (* We take these boolean values as our powerset *) Notation "'Pow' A" := (A -> Bool) (at level 70, no associativity). (* We will be able to reflect these booleans into [Prop] * when we will assume the Excluded Middle * (see [Section EM_imp_PI] below) * * For the moment, we only assume one side of the reflection. *) Variable Bool_to_Prop : Bool -> Prop. (* * For the ease of formalization, we use a coercion: *) Local Coercion Bool_to_Prop : Bool >-> Sortclass. (* - Remark - *) (* --- Following ssrbool, [Bool_to_Prop] would typically be [fun (b : Bool) => (b = TT)] * This is always possible, independently from the Excluded Middle. * However, most of the following formalization * does not depend on this choice. *) (* A candidate paradoxal universe *) Variable U : Prop. Variable el : (Pow U) -> U. Variable set : U -> (Pow U). (* Before working on Girard/Hukens paradox, * we will see how to adapt Cantor's paradox * to a universe with * - a retraction from [Prop] to [Bool] * - and a retraction from [Pow U] to [U] * (given by [set_el_equiv], similar to that of * [Section CantorParadox] above). *) Section Cantor_in_Bool. (* We assume given a retraction from [Prop] to [Bool] *) Variable Prop_to_Bool : Prop -> Bool. Hypothesis Bool_complete : forall P:Prop, P -> Prop_to_Bool P. Hypothesis Bool_correct : forall P:Prop, Prop_to_Bool P -> P. (* and a retraction from [Pow U] to [U] *) Hypothesis set_el_equiv : forall (X : Pow U) (a : U), X a <-> set (el X) a. (* - Question - *) (* --- Define [D], the set of sets that do not belong to themselves *) Let D : Pow U := ... (* Consider now the element of [U] that [el] takes from [D]: *) Let e : U := el D. Check (set_el_equiv D e). (* - Question - *) (* --- Show the following: *) Lemma to_ParadoxalCantorSet : forall (b:U), ~ (set b b) -> (set e b). Proof. ... Qed. (* - Question - *) (* --- Show the following: *) Lemma from_ParadoxalCantorSet : forall (b:U), set e b -> ~ (set b b). Proof. ... Qed. (* - Question - *) (* --- Show that our assumptions are contradictory *) Lemma cantor_Bool : False. Proof. ... Qed. End Cantor_in_Bool. (* The idea now would be to use the excluded middle * in order to define some [U : Prop] [el : (Pow U) -> U] [set : U -> (Pow U)] * such that some [set_el_equiv] of type [forall (X : Pow U) (a : U), X a <-> set (el X) a] * is derivable. * * However, this will not be done directly. * * We will be able to define [U], [el] and [set]. * But [set_el_equiv] will not be available as such. * * We can only get a [set_el_raw_equiv] * such that for all [X : Pow U] and [a : U], * [set (el X) a)] is logically equivalent to [exists (c:U), (X c) /\ (a = el (set c))] * * The problem here is that the sets [c:U] and [el (set c) : U] * are different. * It is however possible to quotient our notion of sets * with an equivalence relation [~~] which identifies * [c : U] with [el (set X)]. * * This leads us to also quotient the membership relation. * Given [a : U] and [b : U], the assertion [set b a : Bool] (coerced into a [Prop]) * must now be thought of as kind of "physical membership". * * The quotiented membership relation [a <~ b] is obtained by * quotienting the physical membership with [~~]: [exists c, (a ~~ c) /\ (set b c)] *) (* The variant [el (set a)) : U] of [a : U] is written [a '] *) Notation "a '" := (el (set a)) (at level 30, no associativity). (* Equivalence Relations *) Definition ER (R : U -> U -> Bool) : Prop := forall a b c, (R a a) /\ (R a b -> R b a) /\ (R a b -> R b c -> R a c). (* We will work with the smallest equivalence relation [~~] on [U] * such that [a ~~ a '] for all [a : U]. * * Before working with the actual equivalence relation, * we will show how to derive the paradox * from an axiomatized version of [~~]. *) Section AxiomatizedQuotient. Variable EQ : U -> U -> Prop. Infix "~~" := EQ (at level 70, no associativity). Hypothesis EQ_Refl : forall a, a ~~ a. Hypothesis EQ_Sym : forall a b, a ~~ b -> b ~~ a. Hypothesis EQ_Trans : forall a b c, a ~~ b -> b ~~ c -> a ~~ c. (* Quotiented membership *) Let In a b : Prop := (exists c, (a ~~ c) /\ (set b c)). Infix "<~" := In (at level 60, no associativity). (* We now assume that: *) (* * - [a] and [a '] are equivalent wrt [~~]: *) Hypothesis EQ_Stroke : forall a, a ~~ (a '). (* * - the quotiented membership [a <~ b] is compatible with [~~]: *) Hypothesis EQ_In_Left : forall a b c, a ~~ b -> a <~ c -> b <~ c. Hypothesis EQ_In_Right : forall a b c, a ~~ b -> c <~ a -> c <~ b. (* - Question - *) (* --- Show the following: *) Lemma Stroke_In_Left_Ax : forall a b, a <~ b -> a <~ b '. Proof. ... Qed. (* - Question - *) (* --- Show the following: *) Lemma Stroke_In_Right_Ax : forall a b, a <~ b ' -> a <~ b. Proof. ... Qed. (* We now show that our axioms are sufficient * to derive a contradiction from the following * additional requirements: * - the existence of a retraction from [Prop] to [Bool : Prop] * - and a [set_el_raw_quiv] as described above *) Section AxiomatizedParadox. (* The retraction from [Prop] to [Bool] *) Variable Prop_to_Bool : Prop -> Bool. Hypothesis Bool_complete : forall P:Prop, P -> Prop_to_Bool P. Hypothesis Bool_correct : forall P:Prop, Prop_to_Bool P -> P. Hypothesis set_el_raw_equiv : forall (X : Pow U) (a : U), (set (el X) a <-> exists c, (X c) /\ (a = el (set c))). (* - Question - *) (* --- Define [D], the set of sets that do not belong to themselves *) Let D : Pow U := ... (* Consider now the element of [U] that [el] takes from [D]: *) Let e : U := el D. Check (D : Pow U). Check (e : U). (* - Question - *) (* --- Show the following *) Lemma to_ParadoxalSet : forall b, ~ (b <~ b) -> b <~ e. Proof. ... Qed. (* - Question - *) (* --- Show the following *) Lemma from_ParadoxalSet : forall b, b <~ e -> ~ (b <~ b). Proof. ... Qed. (* - Question - *) (* --- Show that our assumptions are contradictory *) Theorem axiomatized_girard_hurkens : False. Proof. ... Qed. End AxiomatizedParadox. End AxiomatizedQuotient. (* We now define the actual equivalence relation [~~] *) Section Quotient. (* [~~] is the smallest equivalence relation * such that [a ~~ a '] for all [a : U]. *) Let EQ (a b : U) := forall R, ER R -> (forall c, R c (c ')) -> R a b. Infix "~~" := EQ (at level 70, no associativity). (* The quotiented membership is defined from [~~] as above *) Let In (a b : U) := exists c, (a ~~ c) /\ (set b c). Infix "<~" := In (at level 60, no associativity). (* We now show that [EQ] is indeed an equivalence relation. *) (* - Question - *) (* --- Show the following: *) Lemma EQ_Refl : forall a, a ~~ a. Proof. ... Qed. (* - Question - *) (* --- Show the following: *) Lemma EQ_Sym : forall a b, a ~~ b -> b ~~ a. Proof. ... Qed. (* - Question - *) (* --- Show the following: *) Lemma EQ_Trans : forall a b c, a ~~ b -> b ~~ c -> a ~~ c. Proof. ... Qed. (* The properties relating [_ ~~ _], [_ '] and [_ <~ _] * postulated in [Section AxiomatizedQuotient] above * are provable from * - the existence of a retraction from [Prop] to [Bool : Prop] * - and a [set_el_raw_equiv] as described above *) Section Compatibilities. Variable Prop_to_Bool : Prop -> Bool. Hypothesis Bool_complete : forall P:Prop, P -> Prop_to_Bool P. Hypothesis Bool_correct : forall P:Prop, Prop_to_Bool P -> P. Hypothesis set_el_raw_equiv : forall (X : Pow U) (a : U), (set (el X) a <-> exists c, (X c) /\ (a = el (set c))). (* - Question - *) (* --- Show the following: *) Lemma EQ_Stroke : forall a, EQ a (a '). Proof. ... Qed. (* - Question - *) (* --- Show the following: *) Lemma EQ_In_Left : forall a b c, EQ a b -> a <~ c -> b <~ c. Proof. ... Qed. (* - Question - *) (* --- Show the following: *) Lemma Stroke_In_Left : forall a b, a <~ b -> a <~ b '. Proof. ... Qed. (* - Question - *) (* --- Show the following: *) Lemma Stroke_In_Right : forall a b, a <~ b ' -> a <~ b. Proof. ... Qed. (* - Question - *) (* --- Show the following: *) Lemma EQ_In_Right : forall a b c, EQ a b -> c <~ a -> c <~ b. Proof. ... Qed. (* - Question - *) (* --- Derive a contradiction from * [axiomatized_girard_hurkens] and * the properties just shown *) Theorem girard_hurkens : False. Proof. ... Qed. End Compatibilities. End Quotient. End BooleanReflection_in_Prop. Check girard_hurkens. (* We now assume the Excluded Middle and derive * - a retract from [Prop] to [Bool] * - and a universe [U : Prop] * together with [el : (Pow U) -> U] [set : U -> (Pow U)] * such that we get some [set_el_raw_equiv]. *) Section EM_imp_PI. Variable Bool : Prop. Variable TT FF : Bool. Notation "'Pow' A" := (A -> Bool) (at level 70, no associativity). Hypothesis EM : forall P, P \/ ~ P. (* This coercion is * inspired from ssrbool.v (of the ssreflect extension of Coq) *) Definition Bool_to_Prop (b : Bool) := b = TT. Local Coercion Bool_to_Prop : Bool >-> Sortclass. (* The following is the reason for using [Bool : Prop] * rather than the usual [bool : Set] * * Because of paradoxes such as the one we work on, * Classical Logic from an impredicative sort (such as [Prop]) * implies Proof Irrelevance from the same sort. * * It has been chosen to allow Clasical Logic in [Prop], * and thus the system must be compatible with Proof Irrelevance * from [Prop]. * * Non Confusion from a given sort * (for instance [~ true = false] from [bool : Set]) * contradicts Proof Irrelevance from the same sort. * Since Non Confusion holds from [Set] and [Type], * we have to forbid Proof Irrelevance from [Set] and [Type]. * * However, strong eliminations from [Prop] to [Set] would in general * allow to derive Proof Irrelevance from [Set] from Proof Irrelevance * from [Prop], hence to derive a contradiction * from Classical Logic in [Prop]. * * Hence, we can not in general eliminate from an inductive of * sort [Prop] to sort [Set] or [Type]. * * Typically, the following is rejected: [[ Definition Prop_to_Bool (S : Prop) : bool := match (EM S) with | or_introl _ => true | or_intror _ => false end. ]] * * A notable exception to this rule are the one-constructor * inductive types in Prop, typically such as [eq], * whose only constructor is [refl_equal]. *) (* - Question - *) (* --- Uncomment and try to typecheck the following *) (* Definition Prop_to_Bool (S : Prop) : bool := match (EM S) with | or_introl _ => true | or_intror _ => false end. *) Definition Prop_to_Bool (S : Prop) : Bool := match (EM S) with | or_introl _ => TT | or_intror _ => FF end. Section EM_imp_NonConf_imp_False. Hypothesis NonConf : FF = TT -> False. (* - Question - *) (* --- Show the following: *) Lemma Bool_complete : forall P:Prop, P -> Prop_to_Bool P. Proof. ... Qed. (* - Question - *) (* --- Show the following: *) Lemma Bool_correct : forall P:Prop, Prop_to_Bool P -> P. Proof. ... Qed. (* The paradoxal universe is defined using a Mendler's style * coding of inductive types. This (key) definition is directly * taken from (Sorensen & Urzyczyn 2006). *) Definition U : Prop := forall (X:Prop), (forall (Y:Prop), (Y -> X) -> (Pow Y) -> X) -> X. Definition el : (Pow U) -> U := fun X P k => k U (fun x => x P k) X. Definition set : U -> (Pow U) := fun a => a (Pow U) (fun P (f : P -> Pow U) (S : Pow P) (b : U) => Prop_to_Bool (exists c:P, (S c) /\ (b = el (f c)))). Lemma rewrite_setel: forall (X : Pow U) (a : U), (set (el X) a) = Prop_to_Bool (exists c, (X c) /\ (a = el (set c))). Proof. intros X a. reflexivity. Qed. (* - Question - *) (* --- Show the following: *) Lemma set_el_raw_equiv : forall (X : Pow U) (a : U), (set (el X) a <-> exists c, (X c) /\ (a = el (set c))). Proof. ... Qed. (* - Question - *) (* --- Show the following: *) Theorem EM_imp_NonConf_imp_False : False. Proof. ... Qed. End EM_imp_NonConf_imp_False. (* - Question - *) (* --- Show the following: *) Theorem EM_imp_PI : FF = TT. Proof. ... Qed. End EM_imp_PI. Check EM_imp_PI.