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 http://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).
Lemma lemma1 : induct (fun u => p2b (I u)).
Lemma lemma2 : (forall i:U -> bool, induct i -> b2p (i WF)) -> B.
Theorem paradox : B.
End Paradox.