Library Stdlib.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.

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

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

This is an adaptation of Diaconescu's theorem, exploiting the form of extensionality provided by proof-irrelevance

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

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.