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