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
The axiom of extensionality for predicates
From predicate extensionality we get propositional extensionality
hence proof-irrelevance
From proof-irrelevance and relational choice, we get guarded
relational choice
The form of choice we need: there is a functional relation which chooses
an element in any non empty subset of bool
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
This is an adaptation of Diaconescu's theorem, exploiting the
form of extensionality provided by proof-irrelevance
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
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
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
Proof sketch from Bell
Bell93 (with thanks to P. Castéran)