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
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
(*i $Id: Berardi.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
(** This file formalizes Berardi's paradox which says that in
the calculus of constructions, excluded middle (EM) and axiom of
choice (AC) imply proof irrelevance (PI).
Here, the axiom of choice is not necessary because of the use
of inductive types.
<<
@article{Barbanera-Berardi:JFP96,
author = {F. Barbanera and S. Berardi},
title = {Proof-irrelevance out of Excluded-middle and Choice
in the Calculus of Constructions},
journal = {Journal of Functional Programming},
year = {1996},
volume = {6},
number = {3},
pages = {519-525}
}
>> *)
Set Implicit Arguments.
Section Berardis_paradox.
(** Excluded middle *)
Hypothesis EM : forall P:Prop, P \/ ~ P.
(** Conditional on any proposition. *)
Definition IFProp (P B:Prop) (e1 e2:P) :=
match EM B with
| or_introl _ => e1
| or_intror _ => e2
end.
(** Axiom of choice applied to disjunction.
Provable in Coq because of dependent elimination. *)
Lemma AC_IF :
forall (P B:Prop) (e1 e2:P) (Q:P -> Prop),
(B -> Q e1) -> (~ B -> Q e2) -> Q (IFProp B e1 e2).
Proof.
intros P B e1 e2 Q p1 p2.
unfold IFProp in |- *.
case (EM B); assumption.
Qed.
(** We assume a type with two elements. They play the role of booleans.
The main theorem under the current assumptions is that [T=F] *)
Variable Bool : Prop.
Variable T : Bool.
Variable F : Bool.
(** The powerset operator *)
Definition pow (P:Prop) := P -> Bool.
(** A piece of theory about retracts *)
Section Retracts.
Variables A B : Prop.
Record retract : Prop :=
{i : A -> B; j : B -> A; inv : forall a:A, j (i a) = a}.
Record retract_cond : Prop :=
{i2 : A -> B; j2 : B -> A; inv2 : retract -> forall a:A, j2 (i2 a) = a}.
(** The dependent elimination above implies the axiom of choice: *)
Lemma AC : forall r:retract_cond, retract -> forall a:A, j2 r (i2 r a) = a.
Proof.
intros r.
case r; simpl in |- *.
trivial.
Qed.
End Retracts.
(** This lemma is basically a commutation of implication and existential
quantification: (EX x | A -> P(x)) <=> (A -> EX x | P(x))
which is provable in classical logic ( => is already provable in
intuitionnistic logic). *)
Lemma L1 : forall A B:Prop, retract_cond (pow A) (pow B).
Proof.
intros A B.
destruct (EM (retract (pow A) (pow B))) as [(f0,g0,e) | hf].
exists f0 g0; trivial.
exists (fun (x:pow A) (y:B) => F) (fun (x:pow B) (y:A) => F); intros;
destruct hf; auto.
Qed.
(** The paradoxical set *)
Definition U := forall P:Prop, pow P.
(** Bijection between [U] and [(pow U)] *)
Definition f (u:U) : pow U := u U.
Definition g (h:pow U) : U :=
fun X => let lX := j2 (L1 X U) in let rU := i2 (L1 U U) in lX (rU h).
(** We deduce that the powerset of [U] is a retract of [U].
This lemma is stated in Berardi's article, but is not used
afterwards. *)
Lemma retract_pow_U_U : retract (pow U) U.
Proof.
exists g f.
intro a.
unfold f, g in |- *; simpl in |- *.
apply AC.
exists (fun x:pow U => x) (fun x:pow U => x).
trivial.
Qed.
(** Encoding of Russel's paradox *)
(** The boolean negation. *)
Definition Not_b (b:Bool) := IFProp (b = T) F T.
(** the set of elements not belonging to itself *)
Definition R : U := g (fun u:U => Not_b (u U u)).
Lemma not_has_fixpoint : R R = Not_b (R R).
Proof.
unfold R at 1 in |- *.
unfold g in |- *.
rewrite AC with (r := L1 U U) (a := fun u:U => Not_b (u U u)).
trivial.
exists (fun x:pow U => x) (fun x:pow U => x); trivial.
Qed.
Theorem classical_proof_irrelevence : T = F.
Proof.
generalize not_has_fixpoint.
unfold Not_b in |- *.
apply AC_IF.
intros is_true is_false.
elim is_true; elim is_false; trivial.
intros not_true is_true.
elim not_true; trivial.
Qed.
End Berardis_paradox.
|
