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 theorem, exploiting the form of extensionality provided by proof-irrelevance

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)

Local Notation 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.

Local Notation eps := (epsilon bool true) (only parsing).

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

End ExtensionalEpsilon_imp_EM.