Diaconescu's theorem

Remarks

The same argument works in constructive set theory, where it is often given in the form of Goodman and Myhill. Let $P$ be a proposition, and let $U = \set{x \in \set{0,1} : x = 0 \lor P}$ and $V = \set{x \in \set{0,1} : x = 1 \lor P}$. Both sets are inhabited, so a choice function on $\set{U, V}$ gives $u \in U$ and $v \in V$. Equality on $\set{0,1}$ is decidable, so either $u \ne v$ or $u = v$. If $u \ne v$, then $P$ is false, because $P$ would give $U = V$ and hence $u = v$; if $u = v$, then either $u = 1 \in U$ or $v = 0 \in V$, and in both cases $P$ holds. So $P \lor \lnot P$ holds.

The converse fails. For a nontrivial group $G$, the topos of $G$-sets is Boolean. But the epimorphism from $G$, acting on itself, to the one-point $G$-set has no section, since $G$ has no fixed point. In the topos $\mathbf{Set}$, both choice and excluded middle hold, in line with the theorem.

Going deeper

For a student

In a topos the logic is intuitionistic in general: the subobject classifier is an internal Heyting algebra, not a Boolean algebra. Diaconescu's theorem shows that choice forces this algebra to be Boolean. This is why constructive set theories and type theories use weaker forms such as countable choice or dependent choice.