In mathematical logic, Diaconescu's theorem, or the Goodman–Myhill theorem, states that the full axiom of choice is sufficient to derive the law of the excluded middle, or restricted forms of it, in constructive set theory. It was discovered in 1975 by Diaconescu and later by Goodman and Myhill. Already in 1967, Errett Bishop posed the Theorem as an exercise (Problem 2 on page 58 in Foundations of constructive analysis).
Proof
For any proposition
and
These are sets, using the axiom of specification. In classical set theory this would be equivalent to
and similarly for
Assuming the axiom of choice, there exists a choice function for the set
By the definition of the two sets, this means that
which implies
But since
Thus
The proof relies on the use of the full separation axiom. In constructive set theories with only the predicative separation, the form of P will be restricted to sentences with bound quantifiers only, giving only a restricted form of the law of the excluded middle. This restricted form is still not acceptable constructively.
In constructive type theory, or in Heyting arithmetic extended with finite types, there is typically no separation at all - subsets of a type are given different treatments. A form of the axiom of choice is a theorem, yet excluded middle is not.