blob: 44d259431246a451b6369fcbcdcff17fa6d743b8 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
|
(****************************************************************************)
(* The Calculus of Inductive Constructions *)
(* *)
(* Projet LogiCal *)
(* *)
(* INRIA LRI-CNRS *)
(* Rocquencourt Orsay *)
(* *)
(* May 29th 2002 *)
(* *)
(****************************************************************************)
(* 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.
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 : (A:Prop)(b2p (p2b A))->A.
Hypothesis p2p2 : (A:Prop)A->(b2p (p2b A)).
Variable B:Prop.
Definition V := (A:Prop)((A->bool)->(A->bool))->(A->bool).
Definition U := V->bool.
Definition sb : V -> V := [z][A;r;a](r (z A r) a).
Definition le : (U->bool)->(U->bool) := [i][x](x [A;r;a](i [v](sb v A r a))).
Definition induct : (U->bool)->Prop := [i](x:U)(b2p (le i x))->(b2p (i x)).
Definition WF : U := [z](p2b (induct (z U le))).
Definition I : U->Prop :=
[x]((i:U->bool)(b2p (le i x))->(b2p (i [v](sb v U le x))))->B.
Lemma Omega : (i:U->bool)(induct i)->(b2p (i WF)).
Proof.
Intros i y.
Apply y.
Unfold le WF induct.
Apply p2p2.
Intros x H0.
Apply y.
Exact H0.
Qed.
Lemma lemma1 : (induct [u](p2b (I u))).
Proof.
Unfold induct.
Intros x p.
Apply (p2p2 (I x)).
Intro q.
Apply (p2p1 (I [v:V](sb v U le x)) (q [u](p2b (I u)) p)).
Intro i.
Apply q with i:=[y:?](i [v:V](sb v U le y)).
Qed.
Lemma lemma2 : ((i:U->bool)(induct i)->(b2p (i WF)))->B.
Proof.
Intro x.
Apply (p2p1 (I WF) (x [u](p2b (I u)) lemma1)).
Intros i H0.
Apply (x [y](i [v](sb v U le y))).
Apply (p2p1 ? H0).
Qed.
Theorem paradox : B.
Proof.
Exact (lemma2 Omega).
Qed.
End Paradox.
|
