# Axiom of choice implies law of excluded middle

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.

• I think it's because we want to show $\forall p: p \vee \neg p$, not just $p\vee \neg p$ for some particular $p$. – Gabriel Burns Nov 3 '16 at 18:54
• Classical ZF certainly proves finite choice, but does intuitionistic ZF? – Noah Schweber Nov 3 '16 at 18:57
• Yes, by the same inductive proof. @Noah Schweber – Carl Mummert Nov 4 '16 at 11:29
• According to wikipedia it is spelled "Diaconescu". – DanielV Nov 5 '16 at 6:06

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

• Surely $\{A,B\}$ is at most countable, though? So why is countable choice not sufficient? – Jeffrey Dawson Nov 3 '16 at 19:04
• @JeffreyDawson Countable choice would be sufficient if the notion of "countable" were such that $\{A,B\}$ qualifies. I'm not an expert on the various intuitionistically inequivalent ways of defining "countable", but at least one reasonable-sounding definition, "in bijection with a subset of the natural numbers," doesn't cover $\{A,B\}$. – Andreas Blass Nov 3 '16 at 19:16

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.

• what does it mean for a choice function to be "extensional"? – ziggurism Nov 18 '17 at 23:05
• @ziggurism: In this case, what I mean is that if $U =V$ and $f$ is a choice function then we must have $f(U) = f(V)$. In the proof of Diaconescu's theorem, the trick is to construct $U$ and $V$ in a way that, without knowing the truth value of some statement $P$, we cannot determine whether $U= V$, and moreover so that $U \cap V = \emptyset$ if $P$ is false and $U =V$ if $P$ is true. Then we apply choice to $\{U,V\}$. The choice function has to be extensional, and so by checking whether $f(U) = f(V)$ we are able to tell whether $U = V$ and thus tell whether $P$ is true. – Carl Mummert Nov 19 '17 at 0:42
• More generally, in constructive mathematics, sometimes we work with a set modulo an equivalence relation, for example the set of Cauchy sequences of rationals modulo the relation of "having the same limit". This is called a setoid. An extensional function on the setoid would need to give the same result for any two Cauchy sequences that are equivalent; an intensional function needs to give the same result for identical Cauchy sequences, but possibly not for ones that have the same limit. For example, $f(\alpha) =$ "the first element of $\alpha$" is intensional but not extensional here. – Carl Mummert Nov 19 '17 at 0:44
• In his paper "100 Years of Zermelo's Axiom of Choice: What was the Problem with it?", Martin-Löf argues at length that it is necessary to distinguish between the constructively acceptable, intensional forms of the axiom of choice and the non-constructively-acceptable extensional forms. The paper is at link.springer.com/chapter/10.1007/978-1-4020-8926-8_10 - the book is at doi.org/10.1007/978-1-4020-8926-8 – Carl Mummert Nov 19 '17 at 0:47