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
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
|
(* A variant of Burali-Forti that used to pass in V8.1beta, because of
a bug in the instantiation of sort-polymorphic inductive types *)
(* The following type seems to satisfy the hypothesis of the paradox below *)
(* It should infer constraints forbidding the paradox to go through, but via *)
(* a redefinition that did not propagate constraints correctly in V8.1beta *)
(* it was exploitable to derive an inconsistency *)
(* We keep the file as a non regression test of the bug *)
Record A1 (B:Type) (g:B->Type) : Type := (* Type_i' *)
i1 {X0 : B; R0 : g X0 -> g X0 -> Prop}. (* X0: Type_j' *)
Definition A2 := A1. (* here was the bug *)
Definition A0 := (A2 Type (fun x => x)).
Definition i0 := (i1 Type (fun x => x)).
(* The rest is as in universes-buraliforti.v *)
(* Some properties about relations on objects in Type *)
Inductive ACC (A : Type) (R : A -> A -> Prop) : A -> Prop :=
ACC_intro :
forall x : A, (forall y : A, R y x -> ACC A R y) -> ACC A R x.
Lemma ACC_nonreflexive :
forall (A : Type) (R : A -> A -> Prop) (x : A),
ACC A R x -> R x x -> False.
simple induction 1; intros.
exact (H1 x0 H2 H2).
Qed.
Definition WF (A : Type) (R : A -> A -> Prop) := forall x : A, ACC A R x.
Section Inverse_Image.
Variables (A B : Type) (R : B -> B -> Prop) (f : A -> B).
Definition Rof (x y : A) : Prop := R (f x) (f y).
Remark ACC_lemma :
forall y : B, ACC B R y -> forall x : A, y = f x -> ACC A Rof x.
simple induction 1; intros.
constructor; intros.
apply (H1 (f y0)); trivial.
elim H2 using eq_ind_r; trivial.
Qed.
Lemma ACC_inverse_image : forall x : A, ACC B R (f x) -> ACC A Rof x.
intros; apply (ACC_lemma (f x)); trivial.
Qed.
Lemma WF_inverse_image : WF B R -> WF A Rof.
red in |- *; intros; apply ACC_inverse_image; auto.
Qed.
End Inverse_Image.
(* Remark: the paradox is written in Type, but also works in Prop or Set. *)
Section Burali_Forti_Paradox.
Definition morphism (A : Type) (R : A -> A -> Prop)
(B : Type) (S : B -> B -> Prop) (f : A -> B) :=
forall x y : A, R x y -> S (f x) (f y).
(* The hypothesis of the paradox:
assumes there exists an universal system of notations, i.e:
- A type A0
- An injection i0 from relations on any type into A0
- The proof that i0 is injective modulo morphism
*)
Variable A0 : Type. (* Type_i *)
Variable i0 : forall X : Type, (X -> X -> Prop) -> A0. (* X: Type_j *)
Hypothesis
inj :
forall (X1 : Type) (R1 : X1 -> X1 -> Prop) (X2 : Type)
(R2 : X2 -> X2 -> Prop),
i0 X1 R1 = i0 X2 R2 -> exists f : X1 -> X2, morphism X1 R1 X2 R2 f.
(* Embedding of x in y: x and y are images of 2 well founded relations
R1 and R2, the ordinal of R2 being strictly greater than that of R1.
*)
Record emb (x y : A0) : Prop :=
{X1 : Type;
R1 : X1 -> X1 -> Prop;
eqx : x = i0 X1 R1;
X2 : Type;
R2 : X2 -> X2 -> Prop;
eqy : y = i0 X2 R2;
W2 : WF X2 R2;
f : X1 -> X2;
fmorph : morphism X1 R1 X2 R2 f;
maj : X2;
majf : forall z : X1, R2 (f z) maj}.
Lemma emb_trans : forall x y z : A0, emb x y -> emb y z -> emb x z.
intros.
case H; intros X1 R1 eqx X2 R2 eqy; intros.
case H0; intros X3 R3 eqx0 X4 R4 eqy0; intros.
generalize eqx0; clear eqx0.
elim eqy using eq_ind_r; intro.
case (inj _ _ _ _ eqx0); intros.
exists X1 R1 X4 R4 (fun x : X1 => f0 (x0 (f x))) maj0; trivial.
red in |- *; auto.
Defined.
Lemma ACC_emb :
forall (X : Type) (R : X -> X -> Prop) (x : X),
ACC X R x ->
forall (Y : Type) (S : Y -> Y -> Prop) (f : Y -> X),
morphism Y S X R f -> (forall y : Y, R (f y) x) -> ACC A0 emb (i0 Y S).
simple induction 1; intros.
constructor; intros.
case H4; intros.
elim eqx using eq_ind_r.
case (inj X2 R2 Y S).
apply sym_eq; assumption.
intros.
apply H1 with (y := f (x1 maj)) (f := fun x : X1 => f (x1 (f0 x)));
try red in |- *; auto.
Defined.
(* The embedding relation is well founded *)
Lemma WF_emb : WF A0 emb.
constructor; intros.
case H; intros.
elim eqx using eq_ind_r.
apply ACC_emb with (X := X2) (R := R2) (x := maj) (f := f); trivial.
Defined.
(* The following definition enforces Type_j >= Type_i *)
Definition Omega : A0 := i0 A0 emb.
Section Subsets.
Variable a : A0.
(* We define the type of elements of A0 smaller than a w.r.t embedding.
The Record is in Type, but it is possible to avoid such structure. *)
Record sub : Type := {witness : A0; emb_wit : emb witness a}.
(* F is its image through i0 *)
Definition F : A0 := i0 sub (Rof _ _ emb witness).
(* F is embedded in Omega:
- the witness projection is a morphism
- a is an upper bound because emb_wit proves that witness is
smaller than a.
*)
Lemma F_emb_Omega : emb F Omega.
exists sub (Rof _ _ emb witness) A0 emb witness a; trivial.
exact WF_emb.
red in |- *; trivial.
exact emb_wit.
Defined.
End Subsets.
Definition fsub (a b : A0) (H : emb a b) (x : sub a) :
sub b := Build_sub _ (witness _ x) (emb_trans _ _ _ (emb_wit _ x) H).
(* F is a morphism: a < b => F(a) < F(b)
- the morphism from F(a) to F(b) is fsub above
- the upper bound is a, which is in F(b) since a < b
*)
Lemma F_morphism : morphism A0 emb A0 emb F.
red in |- *; intros.
exists
(sub x)
(Rof _ _ emb (witness x))
(sub y)
(Rof _ _ emb (witness y))
(fsub x y H)
(Build_sub _ x H); trivial.
apply WF_inverse_image.
exact WF_emb.
unfold morphism, Rof, fsub in |- *; simpl in |- *; intros.
trivial.
unfold Rof, fsub in |- *; simpl in |- *; intros.
apply emb_wit.
Defined.
(* Omega is embedded in itself:
- F is a morphism
- Omega is an upper bound of the image of F
*)
Lemma Omega_refl : emb Omega Omega.
exists A0 emb A0 emb F Omega; trivial.
exact WF_emb.
exact F_morphism.
exact F_emb_Omega.
Defined.
(* The paradox is that Omega cannot be embedded in itself, since
the embedding relation is well founded.
*)
Theorem Burali_Forti : False.
apply ACC_nonreflexive with A0 emb Omega.
apply WF_emb.
exact Omega_refl.
Defined.
End Burali_Forti_Paradox.
(* Note: this proof uses a large elimination of A0. *)
Lemma inj :
forall (X1 : Type) (R1 : X1 -> X1 -> Prop) (X2 : Type)
(R2 : X2 -> X2 -> Prop),
i0 X1 R1 = i0 X2 R2 -> exists f : X1 -> X2, morphism X1 R1 X2 R2 f.
intros.
change
match i0 X1 R1, i0 X2 R2 with
| i1 x1 r1, i1 x2 r2 => exists f : _, morphism x1 r1 x2 r2 f
end in |- *.
case H; simpl in |- *.
exists (fun x : X1 => x).
red in |- *; trivial.
Defined.
(* The following command raises 'Error: Universe Inconsistency'.
To allow large elimination of A0, i0 must not be a large constructor.
Hence, the constraint Type_j' < Type_i' is added, which is incompatible
with the constraint j >= i in the paradox.
*)
Definition Paradox : False := Burali_Forti A0 i0 inj.
|
