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.



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.


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 AA is finite or finitely-indexed (respectively) if, for some natural number nn, there is a bijection or surjection (respectively) {0,,n1}A\{0, \ldots, n - 1\} \to A.)


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

On the other hand, if PEM holds, then we can show by induction that if AA and BB are choice, so is ABA\sqcup B (add details). Thus, all finite sets are choice. Now if nAn\to A is a surjection, exhibiting AA as finitely indexed, it has a section AnA\to n. Since a finite set is always projective, and any retract of a projective object is projective, this shows that AA 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.


Review includes

See also