---
tag: 6155D300EB
kind: statement
role: theorem
name: Diaconescu's theorem
msc: [03G30, 18B25, "03E25"]
uses: [6837RS7N82, RVXDSY04KG, NKP5TPQ79X, FS1FKAE89H, 0HTGB13FE2, 0RYYK8PG4S, NG943XNQWH]
about: [6837RS7N82, 0HTGB13FE2, 0RYYK8PG4S]
sources:
  - url: https://en.wikipedia.org/wiki/Diaconescu%27s_theorem
same_as:
  wikidata: Q3527059
  wikipedia: Diaconescu's theorem
---

## Statement

Let $\mathcal{E}$ be an elementary [[topos|6837RS7N82]].
Suppose that every [[epimorphism|RVXDSY04KG]] in $\mathcal{E}$ has a section, that is, $\mathcal{E}$ satisfies the [[axiom of choice|0HTGB13FE2]].
Then $\mathcal{E}$ is Boolean: every [[subobject|FS1FKAE89H]] of every object of $\mathcal{E}$ has a complement.
Equivalently, the internal logic of $\mathcal{E}$ satisfies the [[law of excluded middle|0RYYK8PG4S]].

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

## Explanations

### L1 human

The theorem says that the axiom of choice is not a neutral addition to constructive mathematics.
Once one can always choose an element from each nonempty set in a family, every statement becomes either true or false.
So a constructive setting that wants to avoid excluded middle must also avoid full choice.

### L2 human

In a [[topos|6837RS7N82]] the logic is intuitionistic in general: the [[subobject classifier|NKP5TPQ79X]] is an internal [[Heyting algebra|NG943XNQWH]], 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.