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
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
|
(* -*- coding: utf-8 -*- *)
(************************************************************************)
(* 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: Diaconescu.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
(** Diaconescu showed that the Axiom of Choice entails Excluded-Middle
in topoi [Diaconescu75]. Lacas and Werner adapted the proof to show
that the axiom of choice in equivalence classes entails
Excluded-Middle in Type Theory [LacasWerner99].
Three variants of Diaconescu's result in type theory are shown below.
A. A proof that the relational form of the Axiom of Choice +
Extensionality for Predicates entails Excluded-Middle (by Hugo
Herbelin)
B. A proof that the relational form of the Axiom of Choice + Proof
Irrelevance entails Excluded-Middle for Equality Statements (by
Benjamin Werner)
C. A proof that extensional Hilbert epsilon's description operator
entails excluded-middle (taken from Bell [Bell93])
See also [Carlström] for a discussion of the connection between the
Extensional Axiom of Choice and Excluded-Middle
[Diaconescu75] Radu Diaconescu, Axiom of Choice and Complementation,
in Proceedings of AMS, vol 51, pp 176-178, 1975.
[LacasWerner99] Samuel Lacas, Benjamin Werner, Which Choices imply
the excluded middle?, preprint, 1999.
[Bell93] John L. Bell, Hilbert's epsilon operator and classical
logic, Journal of Philosophical Logic, 22: 1-18, 1993
[Carlström04] Jesper Carlström, EM + Ext_ + AC_int <-> AC_ext,
Mathematical Logic Quaterly, vol 50(3), pp 236-240, 2004.
*)
(**********************************************************************)
(** * Pred. Ext. + Rel. Axiom of Choice -> Excluded-Middle *)
Section PredExt_RelChoice_imp_EM.
(** The axiom of extensionality for predicates *)
Definition PredicateExtensionality :=
forall P Q:bool -> Prop, (forall b:bool, P b <-> Q b) -> P = Q.
(** From predicate extensionality we get propositional extensionality
hence proof-irrelevance *)
Require Import ClassicalFacts.
Variable pred_extensionality : PredicateExtensionality.
Lemma prop_ext : forall A B:Prop, (A <-> B) -> A = B.
Proof.
intros A B H.
change ((fun _ => A) true = (fun _ => B) true) in |- *.
rewrite
pred_extensionality with (P := fun _:bool => A) (Q := fun _:bool => B).
reflexivity.
intros _; exact H.
Qed.
Lemma proof_irrel : forall (A:Prop) (a1 a2:A), a1 = a2.
Proof.
apply (ext_prop_dep_proof_irrel_cic prop_ext).
Qed.
(** From proof-irrelevance and relational choice, we get guarded
relational choice *)
Require Import ChoiceFacts.
Variable rel_choice : RelationalChoice.
Lemma guarded_rel_choice : GuardedRelationalChoice.
Proof.
apply
(rel_choice_and_proof_irrel_imp_guarded_rel_choice rel_choice proof_irrel).
Qed.
(** The form of choice we need: there is a functional relation which chooses
an element in any non empty subset of bool *)
Require Import Bool.
Lemma AC_bool_subset_to_bool :
exists R : (bool -> Prop) -> bool -> Prop,
(forall P:bool -> Prop,
(exists b : bool, P b) ->
exists b : bool, P b /\ R P b /\ (forall b':bool, R P b' -> b = b')).
Proof.
destruct (guarded_rel_choice _ _
(fun Q:bool -> Prop => exists y : _, Q y)
(fun (Q:bool -> Prop) (y:bool) => Q y)) as (R,(HRsub,HR)).
exact (fun _ H => H).
exists R; intros P HP.
destruct (HR P HP) as (y,(Hy,Huni)).
exists y; firstorder.
Qed.
(** The proof of the excluded middle *)
(** Remark: P could have been in Set or Type *)
Theorem pred_ext_and_rel_choice_imp_EM : forall P:Prop, P \/ ~ P.
Proof.
intro P.
(** first we exhibit the choice functional relation R *)
destruct AC_bool_subset_to_bool as [R H].
set (class_of_true := fun b => b = true \/ P).
set (class_of_false := fun b => b = false \/ P).
(** the actual "decision": is (R class_of_true) = true or false? *)
destruct (H class_of_true) as [b0 [H0 [H0' H0'']]].
exists true; left; reflexivity.
destruct H0.
(** the actual "decision": is (R class_of_false) = true or false? *)
destruct (H class_of_false) as [b1 [H1 [H1' H1'']]].
exists false; left; reflexivity.
destruct H1.
(** case where P is false: (R class_of_true)=true /\ (R class_of_false)=false *)
right.
intro HP.
assert (Hequiv : forall b:bool, class_of_true b <-> class_of_false b).
intro b; split.
unfold class_of_false in |- *; right; assumption.
unfold class_of_true in |- *; right; assumption.
assert (Heq : class_of_true = class_of_false).
apply pred_extensionality with (1 := Hequiv).
apply diff_true_false.
rewrite <- H0.
rewrite <- H1.
rewrite <- H0''. reflexivity.
rewrite Heq.
assumption.
(** cases where P is true *)
left; assumption.
left; assumption.
Qed.
End PredExt_RelChoice_imp_EM.
(**********************************************************************)
(** * B. Proof-Irrel. + Rel. Axiom of Choice -> Excl.-Middle for Equality *)
(** This is an adaptation of Diaconescu's paradox exploiting that
proof-irrelevance is some form of extensionality *)
Section ProofIrrel_RelChoice_imp_EqEM.
Variable rel_choice : RelationalChoice.
Variable proof_irrelevance : forall P:Prop , forall x y:P, x=y.
(** Let [a1] and [a2] be two elements in some type [A] *)
Variable A :Type.
Variables a1 a2 : A.
(** We build the subset [A'] of [A] made of [a1] and [a2] *)
Definition A' := sigT (fun x => x=a1 \/ x=a2).
Definition a1':A'.
exists a1 ; auto.
Defined.
Definition a2':A'.
exists a2 ; auto.
Defined.
(** By proof-irrelevance, projection is a retraction *)
Lemma projT1_injective : a1=a2 -> a1'=a2'.
Proof.
intro Heq ; unfold a1', a2', A'.
rewrite Heq.
replace (or_introl (a2=a2) (refl_equal a2))
with (or_intror (a2=a2) (refl_equal a2)).
reflexivity.
apply proof_irrelevance.
Qed.
(** But from the actual proofs of being in [A'], we can assert in the
proof-irrelevant world the existence of relevant boolean witnesses *)
Lemma decide : forall x:A', exists y:bool ,
(projT1 x = a1 /\ y = true ) \/ (projT1 x = a2 /\ y = false).
Proof.
intros [a [Ha1|Ha2]]; [exists true | exists false]; auto.
Qed.
(** Thanks to the axiom of choice, the boolean witnesses move from the
propositional world to the relevant world *)
Theorem proof_irrel_rel_choice_imp_eq_dec : a1=a2 \/ ~a1=a2.
Proof.
destruct
(rel_choice A' bool
(fun x y => projT1 x = a1 /\ y = true \/ projT1 x = a2 /\ y = false))
as (R,(HRsub,HR)).
apply decide.
destruct (HR a1') as (b1,(Ha1'b1,_Huni1)).
destruct (HRsub a1' b1 Ha1'b1) as [(_, Hb1true)|(Ha1a2, _Hb1false)].
destruct (HR a2') as (b2,(Ha2'b2,Huni2)).
destruct (HRsub a2' b2 Ha2'b2) as [(Ha2a1, _Hb2true)|(_, Hb2false)].
left; symmetry; assumption.
right; intro H.
subst b1; subst b2.
rewrite (projT1_injective H) in Ha1'b1.
assert (false = true) by auto using Huni2.
discriminate.
left; assumption.
Qed.
(** An alternative more concise proof can be done by directly using
the guarded relational choice *)
Declare Implicit Tactic auto.
Lemma proof_irrel_rel_choice_imp_eq_dec' : a1=a2 \/ ~a1=a2.
Proof.
assert (decide: forall x:A, x=a1 \/ x=a2 ->
exists y:bool, x=a1 /\ y=true \/ x=a2 /\ y=false).
intros a [Ha1|Ha2]; [exists true | exists false]; auto.
assert (guarded_rel_choice :=
rel_choice_and_proof_irrel_imp_guarded_rel_choice
rel_choice
proof_irrelevance).
destruct
(guarded_rel_choice A bool
(fun x => x=a1 \/ x=a2)
(fun x y => x=a1 /\ y=true \/ x=a2 /\ y=false))
as (R,(HRsub,HR)).
apply decide.
destruct (HR a1) as (b1,(Ha1b1,_Huni1)). left; reflexivity.
destruct (HRsub a1 b1 Ha1b1) as [(_, Hb1true)|(Ha1a2, _Hb1false)].
destruct (HR a2) as (b2,(Ha2b2,Huni2)). right; reflexivity.
destruct (HRsub a2 b2 Ha2b2) as [(Ha2a1, _Hb2true)|(_, Hb2false)].
left; symmetry; assumption.
right; intro H.
subst b1; subst b2; subst a1.
assert (false = true) by auto using Huni2, Ha1b1.
discriminate.
left; assumption.
Qed.
End ProofIrrel_RelChoice_imp_EqEM.
(**********************************************************************)
(** * Extensional Hilbert's epsilon description operator -> Excluded-Middle *)
(** Proof sketch from Bell [Bell93] (with thanks to P. Castéran) *)
Notation Local inhabited A := A (only parsing).
Section ExtensionalEpsilon_imp_EM.
Variable epsilon : forall A : Type, inhabited A -> (A -> Prop) -> A.
Hypothesis epsilon_spec :
forall (A:Type) (i:inhabited A) (P:A->Prop),
(exists x, P x) -> P (epsilon A i P).
Hypothesis epsilon_extensionality :
forall (A:Type) (i:inhabited A) (P Q:A->Prop),
(forall a, P a <-> Q a) -> epsilon A i P = epsilon A i Q.
Notation Local eps := (epsilon bool true) (only parsing).
Theorem extensional_epsilon_imp_EM : forall P:Prop, P \/ ~ P.
Proof.
intro P.
pose (B := fun y => y=false \/ P).
pose (C := fun y => y=true \/ P).
assert (B (eps B)) as [Hfalse|HP]
by (apply epsilon_spec; exists false; left; reflexivity).
assert (C (eps C)) as [Htrue|HP]
by (apply epsilon_spec; exists true; left; reflexivity).
right; intro HP.
assert (forall y, B y <-> C y) by (intro y; split; intro; right; assumption).
rewrite epsilon_extensionality with (1:=H) in Hfalse.
rewrite Htrue in Hfalse.
discriminate.
auto.
auto.
Qed.
End ExtensionalEpsilon_imp_EM.
|
