# Library Coq.Logic.Diaconescu

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.
Lemma proof_irrel : forall (A:Prop) (a1 a2:A), a1 = a2.
From proof-irrelevance and relational choice, we get guarded relational choice
Require Import ChoiceFacts.
Variable rel_choice : RelationalChoice.
Lemma guarded_rel_choice : GuardedRelationalChoice.
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' ) ).
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.
first we exhibit the choice functional relation R
the actual "decision": is (R class_of_true) = true or false?
the actual "decision": is (R class_of_false) = true or false?
case where P is false: (R class_of_true)=true /\ (R class_of_false)=false
cases where P is true
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'.
Defined.
Definition a2':A'.
Defined.
By proof-irrelevance, projection is a retraction
Lemma projT1_injective : a1 = a2 -> a1' = a2'.
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 ).
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.
An alternative more concise proof can be done by directly using the guarded relational choice
Lemma proof_irrel_rel_choice_imp_eq_dec' : a1 = a2 \/ ~ a1 = a2.
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.
End ExtensionalEpsilon_imp_EM.