nLab Diaconescu-Goodman-Myhill theorem

This entry is about the theorem in logic which is often just called Diaconescu’s theorem, but not to be confused with Diaconescu's theorem in topos theory.

---

Idea

The Diaconescu-Goodman–Myhill theorem (Diaconescu 75, Goodman-Myhill 78) states that the law of excluded middle may be regarded as a very weak form of the axiom of choice.

Statement

The following are equivalent:

1. The principle of excluded middle.
2. Finitely indexed sets are projective (in fact, it suffices 2-indexed sets to be projective).
3. Finite sets are choice (in fact, it suffices for 2 to be choice).

(Here, a set $A$ is finite or finitely-indexed (respectively) if, for some natural number $n$, there is a bijection or surjection (respectively) $\{0, \ldots, n - 1\} \to A$.)

Proof

The proof is as follows. If $p$ is a truth value, then divide $2 = \{0,1\}$ by the equivalence relation where $0 \equiv 1$ iff $p$ holds. Then we have a surjection $2\to A$, whose domain is $2$ (and in particular, finite), and whose codomain $A$ is finitely-indexed. But this surjection splits iff $p$ is true or false, so if either $2$ is choice or $2$-indexed sets are projective, then PEM holds.

On the other hand, if PEM holds, then we can show by induction that if $A$ and $B$ are choice, so is $A\sqcup B$ (add details). Thus, all finite sets are choice. Now if $n\to A$ is a surjection, exhibiting $A$ as finitely indexed, it has a section $A\to n$. Since a finite set is always projective, and any retract of a projective object is projective, this shows that $A$ is projective.

In particular, the axiom of choice implies PEM. This argument, due originally to Diaconescu 75, can be internalized in any topos. However, other weak versions of choice such as countable choice (any surjection to a countable set (which for this purpose is any set isomorphic to the set of natural numbers) has a section), dependent choice, or even COSHEP do not imply PEM. In fact, it is often claimed that axiom of choice is true in constructive mathematics (by the BHK or Brouwer-Heyting-Kolmogorov interpretation of predicate logic), leading to much argument about exactly what that means.

References

• Radu Diaconescu, Axiom of choice and complementation, Proceedings of the American Mathematical Society 51:176-178 (1975) (doi:10.1090/S0002-9939-1975-0373893-X)

• N. D. Goodman J. Myhill, Choice Implies Excluded Middle, Zeitschrift fuer Mathematische Logik und Grundlagen der Mathematik 24:461 (1978)

Review includes

• Colin McLarty, Elementary Categories, Elementary Toposes, Oxford University Press, 1996

See also

• Wikipedia, Diaconescu’ theorem