Axiom of choice implies law of excluded middle

Question

Diaconescu's Theorem states that AC implies the Law of Excluded Middle. Essentially the proof goes by defining $A = \{x \in \{0,1\} : x = 0 \lor p\}$, and $B = \{x \in \{0,1\} : x = 1 \lor p\}$, for a given proposition $p$, and defining a choice function $f : \{A,B\} \rightarrow \{0,1\}$. We then show that no matter what values $f$ takes, either $p$ or $\lnot p$ holds. The full proof can be found here.

What confuses me is why the Axiom of Choice is needed, as we are only choosing from two sets, and finite choice is provable in standard ZF. In addition, I've heard that countable choice does not imply excluded middle, but clearly we are not choosing from more than countably many sets in this proof.

Answer 1

Choice from finitely many nonempty sets is indeed provable in standard ZF, but standard ZF is based on classical logic, which includes the law of the excluded middle.

Also, in Diaconescu's proof, the set $\{A,B\}$ cannot be asserted to be a two-element set. It admits a surjective map from, say, $\{0,1\}$, the standard two-element set, but that map might not be bijective since $A$ might equal $B$. If we had classical logic (excluded middle) available, then we could say that $\{A,B\}$ has either two elements or just one element, and it's finite in either case. But without the law of the excluded middle, we can't say that.

In intuitionistic set theory, there are several inequivalent notions of finiteness. The most popular (as far as I can tell) amounts to "surjective image of $\{0,1,\dots,n-1\}$ for some natural number $n$." With this definition, $\{A,B\}$ is finite, but you can't prove choice from finitely many inhabited sets. The second most popular notion of finite amounts to "bijective image of $\{0,1,\dots,n-1\}$ for some natural number $n$." With this definition, you can (unless I'm overlooking something) prove choice from finitely many inhabited sets (just as in classical ZF), but $\{A,B\}$ can't be proved to be finite.

(Side comment: I wrote "inhabited" where you might have expected "nonempty". The reason is that "nonempty" taken literally means that the set is not empty, i.e., that it's not the case that the set has no elements. That's the double-negation of "it has an element". Intuitionistically, the double-negation of a statement is weaker than hte statement itself. In the discussion of choice, I wanted the sets to actually have elements, not merely to not not have elements. "Inhabited" has become standard terminology for "having at least one element" in contexts where "nonempty" doesn't do the job.)

Answer 2

The background theory is an important issue. It is not quite right to say that the law of the excluded middle is provable from the axiom of choice. There are two important details:

1. We are talking about provability in constructive set theories that include separation axioms for undecidable formulas.

2. We are talking about the axiom of choice as expressed in set theory.

There are other constructive systems, such as constructive type theories, where the relevant form of the axiom of choice does not imply the law of the excluded middle. The implication in Diaconescu's theorem is particular to constructive set theory.

Separately, as described in the Stanford Encyclopedia article at http://plato.stanford.edu/entries/set-theory-constructive/index.html#ConChoPri , the axiom of countable choice does not imply the law of excluded middle even in constructive set theory.

If we try to apply the axiom of countable choice to the set in Diaconescu's theorem, nothing odd happens, because it is easy to write a choice function if we view $\{A, B\}$ as a sequence of two sets. The trick in Diaconescu's theorem is that if we apply choice to the family $\{A, B\}$, the choice function has to be extensional, and the theorem leverages the extensionality. Replacing the family with a sequence of two sets $A$ and $B$ makes it easier to write a formula for an extensional choice function.