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-MiddleDiaconescu75 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, 1993Carlströ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
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
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
B. Proof-Irrel. + Rel. Axiom of Choice -> Excl.-Middle for Equality
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
We build the subset A' of A made of a1 and a2
Definition A' := sigT (fun x => x=a1 \/ x=a2).
By proof-irrelevance, projection is a retraction
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
An alternative more concise proof can be done by directly using the guarded relational choice
Extensional Hilbert's epsilon description operator -> Excluded-Middle
Local Notation inhabited A := A (only parsing).
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.