Diaconescu's Theorem

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 ).