# 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öm04] 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 is equivalent
to AC_ext, Mathematical Logic Quaterly, vol 50(3), pp 236-240, 2004.

Require ClassicalFacts ChoiceFacts.

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

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

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

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.

End PredExt_RelChoice_imp_EM.

# Proof-Irrel. + Rel. Axiom of Choice -> Excl.-Middle for Equality

Section ProofIrrel_RelChoice_imp_EqEM.

Import ChoiceFacts.

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 A (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

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.

Theorem extensional_epsilon_imp_EM : forall P:Prop, P \/ ~ P.

End ExtensionalEpsilon_imp_EM.