Notes to The Axiom of Choice

1. Zermelo does not, however, actually give the principle an explicit name at this point. ( He does so only in 1908, where he uses the term “postulate of choice”. We note that Zermelo here uses the term “product” , which is the reason why a number of mathematicians (in particular Russell and Ramsey) referred to the axiom as the “multiplicative axiom” (see §4 below).

2. A function \(f\): \(A \rightarrow B\) is surjective if for any element \(b \in B\) there is \(a \in A\) such that \(f(a) = b\). A right inverse to \(f\) is a function \(g: B \rightarrow A\) such that, for any \(x\in B\), \(f(g(x) = x\).

3. Zermelo’s formulation reads literally:

A set \(S\) that can be decomposed into a set of disjoint parts \(A\), \(B\), \(C\), … , each containing at least one element, possess at least one subset \(S_{1}\) having exactly one element with each of the parts \(A\), \(B\), \(C\), … , considered.

4. The difficulty here is amusingly illustrated by an anecdote due to Bertrand Russell. A millionaire possesses an infinite number of pairs of shoes, and an infinite number of pairs of socks. One day, in a fit of eccentricity, the millionaire summons his valet and asks him to select one shoe from each pair. When the valet, accustomed to receiving precise instructions, asks for details as to how to perform the selection, the millionaire suggests that the left shoe be chosen from each pair. Next day the millionaire proposes to the valet that he select one sock from each pair. When asked as to how this operation is to be carried out, the millionaire is at a loss for a reply, since, unlike shoes, there is no intrinsic way of distinguishing one sock of a pair from the other. In other words, the selection of the socks must be truly arbitrary.

5. In 1923 Hilbert asserted:

The essential idea on which the axiom of choice is based constitutes a general logical principle which, even for the first elements of mathematical inference, is indispensable.

(Quoted in section 4.8 of Moore 1982.)

6. For a detailed history of the Axiom of Choice, see Moore 1982.

7. Here (\(x)_{x\in X}\) indicates that all the members of \(X\) are taken as designated elements of the structure, i.e. as being named by constant symbols in the associated first-order language.

8. For a detailed account of the proof of the independence of the Axiom of Choice, see Bell 2005 or Jech 1973.

9. For the proof of ZL from AC in ZF, see Mendelson 1987 (Ch. 4, sect. 5). For a proof not using ordinals, and so formulable in Zermelo set theory, see Bourbaki 1950 or Lawvere and Rosebrugh 2003 (Appendix B).

10. Thus a nest in \(S\) is a chain in \(S\) partially ordered by set inclusion.

11. That minimal samplings are transversals requires demonstration. Suppose \(S\) is a minimal sampling; then, given \(X\in \sI\) either (1) \(S\cap X\) is finite nonempty or (2) \(X \subseteq S\). In case (1) \(S\cap X\) cannot contain two distinct elements because the removal of one of them from \(S\) would yield a sampling smaller than \(S\), violating its minimality. So in this case \(S\cap X\) must be a singleton. In case (2) \(S\) cannot contain two distinct elements \(a\), \(b\) since, if it did, \(S' = [(S - X) \cup \{a\}]\) would be a sampling smaller than \(S\) (notice that \(S' \cap X = \{a\}\) and the relations of \(S'\) with the members of \(\sI - \{X\}\) are the same as those of \(S\)), again violating the minimality of \(S\). So in this case \(X\), and a fortiori \(S\cap X\) must be a singleton.

12. Had we elected to follow more closely the intuitive combinatorial derivation of AC as sketched above by using selectors instead of samplings we would have encountered the obstacle that—unlike the set of samplings—the set of selectors is not necessarily reductive.

13. For equivalents of the Axiom of Choice, see Rubin and Rubin 1985; for consequences, see Howard and Rubin 1998.

14. “Weaker” here means that, within the context of the axioms of set theory (minus, of course, AC), the proposition in question is entailed by AC, but not vice-versa.

15. The idea of the proof goes back to Goodman and Myhill 1978, which was itself built on a result of Diaconescu 1975. See below.

16. See Bishop and Bridges 1985.

17. See Supplementary Document. For an analysis of various versions of AC within constructive type theory, see Martin-Löf 2006.

18. Also, of course, use was made of \(0 \ne 1\), but this assumption is so weak that it may be consistently added to virtually any axiomatic system.

19. But in weak set theories lacking the axiom of extensionality the derivation of Excluded Middle from AC does not go through: some form of extensionality, or the existence of quotient sets for equivalence relations, needs to be assumed. See Bell 2008.

20. With Zorn’s Lemma the situation is otherwise. For despite its equivalence to AC in classical set theory, in intuitionistic set theory Zorn’s Lemma does not imply LEM: in fact, it has no “non-constructive” logical consequences whatsoever (Grayson 1975, Bell 1997). Thus Zorn’s Lemma is considerably weaker than AC in intuitionistic set theory. Intuitionistic equivalents of Zorn’s Lemma are scarce; a few have been formulated in Bell 2003.

21. That is, the set of all \(R\)-equivalence classes of members of \(A\).

Notes to Supplementary Document: The Axiom of Choice and Type Theory

1. Dependent types were actually first studied in the late 1960s by de Bruijn and his colleagues at the University of Eindhoven in connection with the AUTOMATH project. CDTT has been employed as a basis for various computational devices employed for the verification of mathematical theories and of software and hardware systems in computer science.

2. Analogous constructive versions of set theory, incorporating choice principles, have been developed by Peter Aczel. See Aczel 1978, 1982, 2005 and Aczel & Rathjen 2001.

3. This idea was advanced by Curry and Feys 1958 and later by Howard 1980. As the Curry-Howard correspondence it has come to play an important role in theoretical computer science.

4. For a complete specification of the operations and rules of DCTT, see Chapter 10 of Jacobs 1999 or Gambino & Aczel 2005.

5. See §4.

6. It is interesting to note that Ramsey 1926 also asserted the tautological character of AC but for quite different reasons. Like Zermelo, Ramsey construed—and accepted the truth of—AC as asserting the objective existence of choice functions, given extensionally and so independently of the manner in which they might be described. But the intensional nature of constructive mathematics, and, in particular, of CDTT, decrees that nothing is given completely independently of its description. This leads to a strong construal of the quantifiers which, as we have observed, essentially trivializes AC by rendering the antecedent of the implication constituting it essentially equivalent to the consequent. It is remarkable that AC can be considered tautological both from an extensional and from an intensional point of view.

7. While in classical set theory each singleton in this sense is either empty or a one-element set, in intuitionistic set theory there are many additional “intermediate” sets qualifying as singletons.