# Library Coq.Logic.Hurkens

``` ```
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.

References:

• `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 www.cs.kun.nl/~herman/note.ps.gz).
``` Section Paradox. Variable bool : Prop. Variable p2b : Prop -> bool. Variable b2p : bool -> Prop. Hypothesis p2p1 : forall A:Prop, b2p (p2b A) -> A. Hypothesis p2p2 : forall A:Prop, A -> b2p (p2b A). Variable B : Prop. 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. Definition le (i:U -> bool) (x:U) : bool :=   x (fun A r a => i (fun v => sb v A r a)). Definition induct (i:U -> bool) : Prop :=   forall x:U, b2p (le i x) -> b2p (i x). Definition WF : U := fun z => p2b (induct (z U le)). Definition I (x:U) : Prop :=   (forall i:U -> bool, b2p (le i x) -> b2p (i (fun v => sb v U le x))) -> B. Lemma Omega : forall i:U -> bool, induct i -> b2p (i WF). Proof. intros i y. apply y. unfold le, WF, induct in |- *. apply p2p2. intros x H0. apply y. exact H0. Qed. Lemma lemma1 : induct (fun u => p2b (I u)). Proof. unfold induct in |- *. intros x p. apply (p2p2 (I x)). intro q. apply (p2p1 (I (fun v:V => sb v U le x)) (q (fun u => p2b (I u)) p)). intro i. apply q with (i := fun y => i (fun v:V => sb v U le y)). Qed. Lemma lemma2 : (forall i:U -> bool, induct i -> b2p (i WF)) -> B. Proof. intro x. apply (p2p1 (I WF) (x (fun u => p2b (I u)) lemma1)). intros i H0. apply (x (fun y => i (fun v => sb v U le y))). apply (p2p1 _ H0). Qed. Theorem paradox : B. Proof. exact (lemma2 Omega). Qed. End Paradox. ```