The Axiom of Choice and Excluded Middle (Diaconescu's Theorem)

Classically, the axiom of choice (AC) and the law of excluded middle (LEM) look like two independent optional extras: ZF + LEM is just classical ZF, and AC is a further, separate addition (its independence from ZF is a landmark of set theory). Over intuitionistic logic, this independence breaks down dramatically. Diaconescu's theorem (1975; Goodman–Myhill 1978 for intuitionistic set theory) says:

$$\text{the full set-theoretic axiom of choice implies the law of excluded middle.}$$

So a constructive mathematician cannot adopt full AC without thereby collapsing back into classical logic. AC is not constructively neutral — it secretly is a classical principle.

The result

Working in intuitionistic ZF (IZF) — ZF's axioms over intuitionistic rather than classical logic — with the axiom of extensionality, the full axiom of choice entails $\phi \vee \neg \phi$ for every proposition $\phi$. Since intuitionistic logic is exactly classical logic minus LEM, adding AC on top of it recovers all of classical logic.

The minimal ingredients are modest: extensionality, separation (to form the sets below), pairing, and a two-element set $\{0,1\}$ with decidable equality. The decisive one is extensionality — sets are equal when they have the same members — which is what forces a choice function to respect that equality, and that is where the non-constructive content hides.

The proof (Diaconescu)

Let $\phi$ be an arbitrary proposition. Using separation, form two subsets of $\{0,1\}$:

$$A=\{x\in \{0,1\}:x=0\vee \phi \},B=\{x\in \{0,1\}:x=1\vee \phi \}.$$

Both are inhabited: $0\in A$ and $1\in B$. So $\{A,B\}$ is a set of inhabited sets, and AC supplies a choice function $f$ with $f(A)\in A$ and $f(B)\in B$. Unpacking membership:

$$f(A)=0\vee \phi ,f(B)=1\vee \phi ,\text{with }f(A),f(B)\in \{0,1\}.$$

Equality on $\{0,1\}$ is decidable, so we may case-split on whether $f(A)=f(B)$:

• If $f(A)=f(B)$, then $\phi$. From $f(A)=0\vee \phi$: if $\phi$, done. Otherwise $f(A)=0$, so $f(B)=f(A)=0$; but $f(B)=1\vee \phi$, and $f(B)=1$ would give $0=1$ (absurd, hence $\phi$ by ex falso), so again $\phi$.
• If $f(A)\ne f(B)$, then $\neg \phi$. Suppose $\phi$. Then the defining conditions $x=0\vee \phi$ and $x=1\vee \phi$ both hold for every $x\in \{0,1\}$, so $A=\{0,1\}=B$. By extensionality $A=B$, whence $f(A)=f(B)$ — contradicting $f(A)\ne f(B)$. Hence $\neg \phi$.

Since the case-split is decidable, we have established $\phi \vee \neg \phi$ for arbitrary $\phi$. $■$

The crux is the second case: $\phi$ collapses $A$ and $B$ to the same set, so extensionality forces the choice function to return the same value — and the failure of that collapse is a constructive witness for $\neg \phi$. Choice, forced to respect extensional equality, decides $\phi$.

Doesn't the case-split already use LEM?

A natural worry: the step "decide whether $f(A)=f(B)$" looks like an appeal to $\psi \vee \neg \psi$ — isn't the proof then circular, assuming LEM to derive it? It is not, and seeing why is the whole point.

• Decidable equality is a constructive theorem, not LEM. The set $\{0,1\}$ has decidable equality: it is a finite/discrete subset of $\mathbb{N}$, and $\mathbb{N}$'s equality is decided by the Peano construction (zero vs. successor) and induction. Concretely, $f(A)\in \{0,1\}=\{x:x=0\vee x=1\}$, so membership hands you the genuine disjunction $f(A)=0\vee f(A)=1$ with a determinate, computed disjunct — and likewise for $f(B)$. From two such determinate values, "$f(A)=f(B)$ or not" is settled by a construction. This is decide(f(A), f(B)), not an axiom.
• Excluded middle for decidable propositions is intuitionistically valid. Intuitionistic logic rejects only the blanket schema "$\psi \vee \neg \psi$ for every $\psi$"; individual instances that we can settle are perfectly provable. Using a provably-decidable instance is not "using LEM."
• That is exactly what makes the theorem non-trivial. The case-split is decidable because it ranges over the discrete set $\{0,1\}$ — whereas the target $\phi$ may be wholly undecidable. The argument exports the decidability of $\{0,1\}$-equality to the arbitrary $\phi$, and the bridge that illegitimately ties them together is AC + extensionality, never the case-split. (If the proof had used LEM, the result $\mathrm{AC}+\mathrm{LEM}\Rightarrow \mathrm{LEM}$ would be vacuous.)

So the only excluded-middle used inside the proof is the harmless, decidable kind; the general LEM appears solely in the conclusion, manufactured from choice and extensionality.

Why this does not make all constructive choice illegitimate

The theorem is about the full, extensional, set-theoretic AC. Several nearby principles escape it:

• Type-theoretic "axiom of choice" is a harmless theorem. In Martin-Löf type theory the choice principle $\prod \sum \to \sum \prod$ is actually provable, and it does not imply LEM. The reason is the BHK / Curry–Howard reading: a constructive $\exists$ already carries its witness, so "choosing" is trivial. The set-theoretic AC differs precisely because mere existence (an existence claim with the witness forgotten, i.e. propositionally truncated) must be turned back into an extensional function — the step Diaconescu exploits.
• Weaker choice principles are constructively safe. Constructive set theories (IZF, CZF) reject full AC but consistently retain countable choice (${\mathrm{AC}}_{\omega }$), dependent choice (DC), and the presentation axiom (COSHEP) — enough for constructive analysis (Bishop) without implying LEM.
• No extensionality, no collapse. In settings without a global extensionality axiom (type theory with setoids), choice functions need not respect equality, and the argument does not even start.

Where it sits in the bigger picture

• Over intuitionistic logic, AC is strictly stronger than it looks: $\mathrm{AC}\Rightarrow \mathrm{LEM}$. The converse fails — classical logic does not prove choice (ZF + LEM is just classical ZF, where AC remains independent). So the implication is one-directional.
• This is a different "choice" phenomenon from the one in metatheory of FOL, where the completeness theorem for uncountable languages needs the weak choice principle BPI. There the issue is how much choice a classical metatheorem consumes; here it is that any full choice, added constructively, detonates into classical logic.
• Morally: AC is not a neutral "bookkeeping" axiom. Set-theoretically, the demand that a single function uniformly and extensionally pick witnesses is already a commitment to bivalence.

Take-aways

• Diaconescu's theorem: in IZF with extensionality, full AC implies LEM — constructive mathematics cannot take full choice without becoming classical.
• The proof turns a proposition $\phi$ into two subsets of $\{0,1\}$ that extensionality collapses iff $\phi$; a choice function's output then decides $\phi$.
• The culprit is extensional choice over truncated existence; the type-theoretic choice principle is a provable triviality, and countable/dependent choice are constructively acceptable.
• The implication is one-way: $\mathrm{AC}\Rightarrow \mathrm{LEM}$ constructively, but $\mathrm{LEM}\nRightarrow \mathrm{AC}$.

Related discussions: Intuitionistic Logic (the law of excluded middle and what its absence buys), Axiomatic Set Theory (ZFC) (the classical independence of AC), and What the Metalanguage for First-Order Logic Assumes (the weak choice principle BPI in classical FOL metatheory).