diff options
| -rw-r--r-- | theories/Logic/Hurkens.v | 173 | ||||
| -rw-r--r-- | theories/Logic/UniversesFacts.v | 128 |
2 files changed, 167 insertions, 134 deletions
diff --git a/theories/Logic/Hurkens.v b/theories/Logic/Hurkens.v index 1dce51b2b..d7871995c 100644 --- a/theories/Logic/Hurkens.v +++ b/theories/Logic/Hurkens.v @@ -8,22 +8,49 @@ (* Hurkens.v *) (************************************************************************) -(** This is Hurkens paradox [Hurkens] in system U-, adapted by Herman - Geuvers [Geuvers] to show the inconsistency in the pure calculus of - constructions of a retract from Prop into a small type. +(** Exploiting Hurkens' paradox [[Hurkens95]] for system U- so as to + derive contradictions from + - the existence in the pure Calculus of Constructions of a retract + from Prop into a small type of Prop + - the existence in the Calculus of Constructions with universes + of a retract from some Type universe into Prop + + The first proof is a simple and effective formulation by Herman + Geuvers [[Geuvers01]] of a result by Thierry Coquand + [[Coquand90]]. The result implies that Coq with classical logic + stated in impredicative Set is inconsistent and that classical + logic stated in Prop implies proof-irrelevance (see + [ClassicalFacts.v]) + + The second proof is an adaptation of the first proof by Hugo + Herbelin to eventually prove the inconsistency of Prop=Type. References: - - [Hurkens] A. J. Hurkens, "A simplification of Girard's paradox", + - [[Coquand90]] T. Coquand, "Metamathematical Investigations of a + Calculus of Constructions", Proceedings of Logic in Computer + Science (LICS'90), 1990. + + - [[Hurkens95]] A. J. Hurkens, "A simplification of Girard's paradox", Proceedings of the 2nd international conference Typed Lambda-Calculi and Applications (TLCA'95), 1995. - - [Geuvers] "Inconsistency of Classical Logic in Type Theory", 2001 - (see http://www.cs.kun.nl/~herman/note.ps.gz). + - [[Geuvers01]] H. Geuvers, "Inconsistency of Classical Logic in Type + Theory", 2001, revised 2007 + (see http://www.cs.ru.nl/~herman/PUBS/newnote.ps.gz). *) +(* Pleasing coqdoc! *) + +(** * Inconsistency of the existence in the pure Calculus of Constructions of a retract from Prop into a small type of Prop *) + +Module NoRetractFromSmallPropositionToProp. + Section Paradox. +(** Assumption of a retract from Prop to a small type in Prop, using + equivalence as the equality on propositions *) + Variable bool : Prop. Variable p2b : Prop -> bool. Variable b2p : bool -> Prop. @@ -31,6 +58,8 @@ Hypothesis p2p1 : forall A:Prop, b2p (p2b A) -> A. Hypothesis p2p2 : forall A:Prop, A -> b2p (p2b A). Variable B : Prop. +(** Proof *) + Definition V := forall A:Prop, ((A -> bool) -> A -> bool) -> A -> bool. Definition U := V -> bool. Definition sb (z:V) : V := fun A r a => r (z A r) a. @@ -79,3 +108,135 @@ exact (lemma2 Omega). Qed. End Paradox. + +End NoRetractFromSmallPropositionToProp. + +Export NoRetractFromSmallPropositionToProp. + +(** * Inconsistency of the existence in the Calculus of Constructions with universes of a retract from some Type universe into Prop. *) + +(** Note: Assuming the context [down:Type->Prop; up:Prop->Type; forth: + forall (A:Type), A -> up (down A); back: forall (A:Type), up + (down A) -> A; H: forall (A:Type) (P:A->Type) (a:A), + P (back A (forth A a)) -> P a] is probably enough. *) + +Module NoRetractFromTypeToProp. + +Definition Type2 := Type. +Definition Type1 := Type : Type2. + +Section Paradox. + +Notation "'rew1' <- H 'in' H'" := (@eq_rect_r Type1 _ (fun X : Type1 => X) H' _ H) + (at level 10, H' at level 10). +Notation "'rew1' H 'in' H'" := (@eq_rect Type1 _ (fun X : Type1 => X) H' _ H) + (at level 10, H' at level 10). + +(** Assumption of a retract from Type into Prop *) + +Variable down : Type1 -> Prop. +Variable up : Prop -> Type1. +Hypothesis up_down : forall (A:Type1), up (down A) = A :> Type1. + +(** Proof *) + +Definition V : Type1 := forall A:Prop, ((up A -> Prop) -> up A -> Prop) -> up A -> Prop. +Definition U : Type1 := V -> Prop. + +Definition forth (a:U) : up (down U) := rew1 <- (up_down U) in a. +Definition back (x:up (down U)) : U := rew1 (up_down U) in x. + +Definition sb (z:V) : V := fun A r a => r (z A r) a. +Definition le (i:U -> Prop) (x:U) : Prop := x (fun A r a => i (fun v => sb v A r a)). +Definition le' (i:up (down U) -> Prop) (x:up (down U)) : Prop := le (fun a:U => i (forth a)) (back x). +Definition induct (i:U -> Prop) : Type1 := forall x:U, up (le i x) -> up (i x). +Definition WF : U := fun z => down (induct (fun a => z (down U) le' (forth a))). +Definition I (x:U) : Prop := + (forall i:U -> Prop, up (le i x) -> up (i (fun v => sb v (down U) le' (forth x)))) -> False. + +Lemma back_forth (a:U) : back (forth a) = a. +Proof. +apply rew_opp_r with (P:=fun X:Type1 => X). +Defined. + +Lemma Omega : forall i:U -> Prop, induct i -> up (i WF). +Proof. +intros i y. +apply y. +unfold le, WF, induct. +rewrite up_down. +intros x H0. +apply y. +unfold sb, le', le. +rewrite back_forth. +exact H0. +Qed. + +Lemma lemma1 : induct (fun u => down (I u)). +Proof. +unfold induct. +intros x p. +rewrite up_down. +intro q. +generalize (q (fun u => down (I u)) p). +rewrite up_down. +intro r. +apply r. +intros i j. +unfold le, sb, le', le in j |-. +rewrite back_forth in j. +specialize q with (i := fun y => i (fun v:V => sb v (down U) le' (forth y))). +apply q. +exact j. +Qed. + +Lemma lemma2 : (forall i:U -> Prop, induct i -> up (i WF)) -> False. +Proof. +intro x. +generalize (x (fun u => down (I u)) lemma1). +rewrite up_down. +intro r. apply r. +intros i H0. +apply (x (fun y => i (fun v => sb v (down U) le' (forth y)))). +unfold le, WF in H0. +rewrite up_down in H0. +exact H0. +Qed. + +Theorem paradox : False. +Proof. +exact (lemma2 Omega). +Qed. + +End Paradox. + +End NoRetractFromTypeToProp. + +(** Application: Prop<>Type for some given Type *) + +Import NoRetractFromTypeToProp. + +Section Prop_neq_Type. + +Notation "'rew2' <- H 'in' H'" := (@eq_rect_r Type2 _ (fun X : Type2 => X) H' _ H) + (at level 10, H' at level 10). +Notation "'rew2' H 'in' H'" := (@eq_rect Type2 _ (fun X : Type2 => X) H' _ H) + (at level 10, H' at level 10). + +Variable Heq : Prop = Type1 :> Type2. + +Definition down : Type1 -> Prop := fun A => rew2 <- Heq in A. +Definition up : Prop -> Type1 := fun A => rew2 Heq in A. + +Lemma up_down : forall (A:Type1), up (down A) = A :> Type1. +Proof. +unfold up, down. rewrite Heq. reflexivity. +Defined. + +Theorem Prop_neq_Type : False. +Proof. +apply paradox with down up. +apply up_down. +Qed. + +End Prop_neq_Type. diff --git a/theories/Logic/UniversesFacts.v b/theories/Logic/UniversesFacts.v deleted file mode 100644 index 0adb662fc..000000000 --- a/theories/Logic/UniversesFacts.v +++ /dev/null @@ -1,128 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(** A proof of the inconsistency of Prop=Type (for some fixed Type) in - Coq using Hurkens' paradox for system Type:Type [Hurkens]. - - Adapted from an initial formulation by Herman Geuvers [Geuvers] (this - formulation was used to show the inconsistency in the pure - calculus of constructions of a retract from Prop into a small - type, see Hurkens.v). - - - [Hurkens] A. J. Hurkens, "A simplification of Girard's paradox", - Proceedings of the 2nd international conference Typed Lambda-Calculi - and Applications (TLCA'95), 1995. - - - [Geuvers] "Inconsistency of Classical Logic in Type Theory", 2001 - (see http://www.cs.kun.nl/~herman/note.ps.gz). -*) - -Section Paradox. - -Definition Type2 := Type. -Definition Type1 := Type : Type2. - -(** Preliminary *) - -Notation "'rew2' <- H 'in' H'" := (@eq_rect_r Type2 _ (fun X : Type2 => X) H' _ H) - (at level 10, H' at level 10). -Notation "'rew2' H 'in' H'" := (@eq_rect Type2 _ (fun X : Type2 => X) H' _ H) - (at level 10, H' at level 10). -Notation "'rew1' <- H 'in' H'" := (@eq_rect_r Type1 _ (fun X : Type1 => X) H' _ H) - (at level 10, H' at level 10). -Notation "'rew1' H 'in' H'" := (@eq_rect Type1 _ (fun X : Type1 => X) H' _ H) - (at level 10, H' at level 10). - -Lemma rew_rew : forall (A B:Type1) (H:B=A) (x:A), rew1 H in rew1 <- H in x = x. -Proof. -intros. -destruct H. -reflexivity. -Defined. - -(** Main assumption and proof *) - -Variable Heq : Prop = Type1 :> Type2. - -Definition down : Type1 -> Prop := fun A => rew2 <- Heq in A. -Definition up : Prop -> Type1 := fun A => rew2 Heq in A. - -Lemma up_down : forall (A:Type1), up (down A) = A :> Type1. -Proof. -unfold up, down. rewrite Heq. reflexivity. -Defined. - -Definition V : Type1 := forall A:Prop, ((up A -> Prop) -> up A -> Prop) -> up A -> Prop. -Definition U : Type1 := V -> Prop. - -Definition forth (a:U) : up (down U) := rew1 <- (up_down U) in a. -Definition back (x:up (down U)) : U := rew1 (up_down U) in x. - -Definition sb (z:V) : V := fun A r a => r (z A r) a. -Definition le (i:U -> Prop) (x:U) : Prop := x (fun A r a => i (fun v => sb v A r a)). -Definition le' (i:up (down U) -> Prop) (x:up (down U)) : Prop := le (fun a:U => i (forth a)) (back x). -Definition induct (i:U -> Prop) : Type1 := forall x:U, up (le i x) -> up (i x). -Definition WF : U := fun z => down (induct (fun a => z (down U) le' (forth a))). -Definition I (x:U) : Prop := - (forall i:U -> Prop, up (le i x) -> up (i (fun v => sb v (down U) le' (forth x)))) -> False. - -Lemma back_forth (a:U) : back (forth a) = a. -Proof. -apply rew_rew. -Defined. - -Lemma Omega : forall i:U -> Prop, induct i -> up (i WF). -Proof. -intros i y. -apply y. -unfold le, WF, induct. -rewrite up_down. -intros x H0. -apply y. -unfold sb, le', le. -rewrite back_forth. -exact H0. -Qed. - -Lemma lemma1 : induct (fun u => down (I u)). -Proof. -unfold induct. -intros x p. -rewrite up_down. -intro q. -generalize (q (fun u => down (I u)) p). -rewrite up_down. -intro r. -apply r. -intros i j. -unfold le, sb, le', le in j |-. -rewrite back_forth in j. -specialize q with (i := fun y => i (fun v:V => sb v (down U) le' (forth y))). -apply q. -exact j. -Qed. - -Lemma lemma2 : (forall i:U -> Prop, induct i -> up (i WF)) -> False. -Proof. -intro x. -generalize (x (fun u => down (I u)) lemma1). -rewrite up_down. -intro r. apply r. -intros i H0. -apply (x (fun y => i (fun v => sb v (down U) le' (forth y)))). -unfold le, WF in H0. -rewrite up_down in H0. -exact H0. -Qed. - -Theorem paradox : False. -Proof. -exact (lemma2 Omega). -Qed. - -End Paradox. |