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

Proof

The theorem is a forgone conclusion over classical logic, where law of the excluded middle is assumed, so the proof here is instead in the context of a constructive set theory. A core ingredient is the axiom of extensionality as well as an axiom of comprehension that allows for comprehension involving some proposition ${\displaystyle P}$.

Using comprehension, one considers two subsets of a set with two distinguishable members, such as ${\displaystyle \{0,1\}}$ with ${\displaystyle 0\neq 1}$:

${\displaystyle U=\{x\in \{0,1\}\mid (x=0)\vee P\}}$

and

${\displaystyle V=\{x\in \{0,1\}\mid (x=1)\lor P\}.}$

If ${\displaystyle P}$ can be proven, then both of these sets equal ${\displaystyle \{0,1\}}$. In particular, ${\displaystyle P\,\to \,U=V}$ by extensionality. In turn, for any mathematical function ${\displaystyle g}$ that can take both of these sets as an argument, one finds ${\displaystyle P\,\to \,g(U)=g(V)}$, the contrapositive of which is ${\displaystyle g(U)\neq g(V)\,\to \,\neg P}$.

A choice function ${\displaystyle f}$ for the set ${\displaystyle \{U,V\}}$ into their union ${\displaystyle \{0,1\}}$ by definition fulfills

${\displaystyle f(U)\in U\,\land \,f(V)\in V.}$

Using the definition of the two subsets and the function's established codomain, this reduces to

${\displaystyle {\big (}f(U)=0\lor P{\big )}\land {\big (}f(V)=1\lor P{\big )}.}$

Using the law of distributivity, this in turn implies ${\displaystyle P\lor {\big (}f(U)\neq f(V){\big )}}$. By the previous comment on functions, the existence of a choice function on this set thus implies (indeed is equivalent to) the disjunction ${\displaystyle P\lor \neg P}$.

Both ${\displaystyle U}$ and ${\displaystyle V}$ are inhabited, as witnessed by ${\displaystyle 0\in U}$ and ${\displaystyle 1\in V}$. So the axiom of choice, in particular granting a choice function on all sets of this form, implies excluded middle for all propositions.

Discussion

As noted, ${\displaystyle P}$ implies that both defined sets equal ${\displaystyle \{0,1\}}$. In that case, the pair ${\displaystyle \{U,V\}}$ equals the singleton set ${\displaystyle \{\{0,1\}\}}$ and there are two possible choice functions on that domain, picking either ${\displaystyle 0}$ or ${\displaystyle 1}$. If, instead, ${\displaystyle P}$ can be rejected, i.e. if ${\displaystyle \neg P}$ holds, then ${\displaystyle U=\{0\}}$ and ${\displaystyle V=\{1\}}$. So in that case ${\displaystyle U\neq V}$, and on the proper pair ${\displaystyle \{\{0\},\{1\}\}}$ there is only one possible choice function, picking the unique inhabitant of each singleton set. This last assignment "${\displaystyle U\mapsto 0}$ and ${\displaystyle V\mapsto 1}$" is not viable if ${\displaystyle P}$ holds, as then the two inputs are actually the same. Similarly, the former two assignments are not viable if ${\displaystyle \neg P}$ holds, as then the two inputs share no common member. What can be said is that if a choice function exists at all, then there exists a choice function choosing ${\displaystyle 0}$ from ${\displaystyle U}$, and one (possibly the same function) choosing ${\displaystyle 1}$ from ${\displaystyle V}$.

For bivalent semantics, the above three explicit candidates are all the possible choice assignments.

One may define certain sets in terms of the proposition ${\displaystyle P}$ and, using excluded middle, in classical set theory prove that these sets constitute choice functions ${\displaystyle f\colon \{U,V\}\to \{0,1\}}$. Such a set represents an assignment conditioned on whether or not ${\displaystyle P}$ holds. If ${\displaystyle P}$ can be decided true or false, then such a set explicitly simplifies to one of the above three candidates.

But, in any case, neither ${\displaystyle P}$ nor ${\displaystyle \neg P}$ can necessarily be established. Indeed, they may even be independent of the theory at hand. 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, ${\displaystyle f(U)}$ and ${\displaystyle f(V)}$, among the terms ${\displaystyle 0}$ and ${\displaystyle 1}$. So it is not a function in the sense of the word that it could be explicitly evaluated into its codomain of distinguishable values.

Notes