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.
The theorem was discovered in 1975 by Radu Diaconescu[1] and later by Goodman and Myhill.
[2] Already in 1967, Errett Bishop posed the theorem as an exercise (Problem 2 on page 58 in Foundations of constructive analysis[3]).
The theorem is a foregone conclusion over classical logic, where law of the excluded middle is assumed.
A crucial role in the set theoretic proof is also played by the axiom of extensionality.
Fixing terminology for the proof: Call a set finite if there exists a bijection with a natural number, i.e. a finite von Neumann ordinal.
The proof below is straight forward in that it does not require pathological distinctions concerning the empty set.
And in the end, only a rather restrained form of full choice must be made use of.
For concreteness and simplicity, the section supposes a constructive set theory with full Separation, i.e. we allow for comprehension involving any proposition
In that context, the following lemma then more sharply isolates the core insight: Once the backward-direction of this equivalence is a given, then the axiom of choice, in particular granting a choice function on all sets of this form, implies excluded middle for all propositions.
To prove the backward-direction one considers two subsets of any doubleton with two distinguishable members.
and fulfill Using the definition of the two subsets and the function's established codomain, this reduces to Using the law of distributivity, this in turn implies
there is only one possible choice function, picking the unique inhabitant of each singleton set.
For bivalent semantics, the above three explicit candidates are all the possible choice assignments.
can be decided true or false, then such a set explicitly simplifies to one of the above three candidates.
Since the former two explicit candidates are each incompatible with the third, it is generally not possible to identify both of the choice function's return values,
So it is not a function in the sense of the word that it could be explicitly evaluated into its codomain of distinguishable values.
or any principle implying it, it cannot even be proven that a disjunction of the set equality statements above must be the case.
(However, any finite ordinal injects into any Dedekind-infinite set and so a subset of a finite ordinal does validate the logically negative notion of Dedekind-finiteness.
Note that such a situation does not arise with the domain of choice functions granted by the weaker principles of countable and dependent choice, since in these cases the domain is always just
Adopting the full axiom of choice or classical logic formally implies that the cardinality of
But a postulate such as this mere function existence axiom still does not resolve the question what exact cardinality this domain has, nor does it determine the cardinality of the set of that functions possible output values.
In summary, functions are related to equality (by the definition of unique existence used in functionality), equality is related to membership (directly through the axiom of extensionality and also through the formalization of choice in sets) and membership is related to predicates (through an axiom of separation).
And the excluded middle statement for it is equivalent to the existence of some choice function on
In theories with only restricted forms of separation, the types of propositions
In particular, in the axiom schema of predicative separation only sentences with set bound quantifiers may be used.
The restricted form of excluded middle provable in that context is however still not acceptable constructively.
For example, when arithmetic has a model (when, relevantly, the infinite collection of natural numbers form a set one may quantify over), then set-bounded but undecidable propositions can be expressed.
There, a form of the axiom of choice is a theorem, yet excluded middle is not.
[citation needed] In Diaconescu's original paper, the theorem is presented in terms of topos models of constructive set theory.