nLab Diaconescu-Goodman-Myhill theorem

Contents

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.


Contents

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

Proof

The proof is as follows. If pp is a truth value, then divide 2={0,1}2 = \{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.

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

Last revised on July 2, 2023 at 04:46:28. See the history of this page for a list of all contributions to it.