Each worksheet prints cleanly on A4 or Letter. Answer keys are on a separate page.

The Lumenary · Advanced undergraduate

The axiom of choice and its equivalents

Name: ______________________

Date: ______________________

You will learn to

State the axiom of choice in several forms and prove, over ZF, that it is equivalent to Zorn's lemma and to the well-ordering theorem
Use Zorn's lemma to prove that every vector space has a basis and that every non-zero commutative ring with identity has a maximal ideal
Explain why choosing from countably many two-element sets already needs an axiom, and where countable and dependent choice suffice
Construct a set of reals that is not Lebesgue measurable, and describe what is known when choice is dropped (Gödel, Cohen, Solovay)
Prove Diaconescu's theorem that choice implies the law of excluded middle, and relate it to the foundations of Lean

1.
Which of these choice tasks genuinely needs (some form of) the axiom of choice?
- A.Choose an element from each non-empty subset of $\N$
- B.Choose one element from each of five non-empty sets
- C.Choose one sock from each of countably many pairs of indistinguishable socks
- D.Choose a point from each non-empty closed interval $[a, b]$ with $a \le b$
2.
In the proof that every vector space has a basis, why is the union of a chain $C$ of linearly independent sets again linearly independent?
- A.A dependence involves finitely many vectors, which all lie in a single member of the chain
- B.Because a union of independent sets is always independent
- C.Because the chain is countable
- D.Because the union spans the space
3.
In Krull's theorem, why is the union $U$ of a non-empty chain of proper ideals again proper?
- A.Because $1$ lies in no member of the chain, so $1 \notin U$
- B.Because a union of proper subsets is always proper
- C.Because the chain has a largest element
- D.Because $R$ is commutative
4.
How many (unordered) bases does the vector space $(\Z/2)^3$ have?
5.
How many maximal ideals does the ring $\Z/360$ have?
6.
Which of these are provable in ZF, without any form of choice? Select all.
- A.Every surjection $p : \N \to A$ has a section
- B.If every set can be well-ordered, then AC holds
- C.Every surjection $p : \R \to A$ has a section
- D.A countable union of countable sets is countable
- E.The Schröder–Bernstein theorem
7.
Which Lean proposition expresses the axiom of choice (for families indexed by a type ι)?
- A.∀ (ι : Type) (X : ι → Type), (∀ i, Nonempty (X i)) → Nonempty (∀ i, X i)
- B.∀ (ι : Type) (X : ι → Type), Nonempty (∀ i, X i) → ∀ i, Nonempty (X i)
- C.∀ (ι : Type) (X : ι → Type), (∃ i, Nonempty (X i)) → Nonempty (∀ i, X i)
- D.∀ (ι : Type) (X : ι → Type), Nonempty (Σ i, X i)
8.
In the proof of Diaconescu's theorem, with $U = \{x \in \{0, 1\} \mid x = 0 \lor p\}$ and $V = \{x \in \{0, 1\} \mid x = 1 \lor p\}$ , where exactly is extensionality used?
- A.To conclude $U = V$ (and hence $f(U) = f(V)$ ) from the assumption $p$
- B.To show that $U$ and $V$ are non-empty
- C.To decide whether $f(U) = 0$ or $f(U) = 1$
- D.It is not used; the proof works without it
9.
Vectors in $(\Z/2)^n$ are stored as integers whose binary digits are the coordinates; vector addition is XOR (^). Write span(vectors) returning the set of all sums of subsets of vectors (including 0), and extend_to_basis(start, n) that starts from the linearly independent list start and goes through 1, 2, ..., 2**n - 1, appending every vector not already in the span. It should return the resulting list — a basis containing start.
Computational — Practice

Answer key — The axiom of choice and its equivalents

1.
Only the socks need choice. For subsets of $\N$ and for intervals there is a definable rule (least element, midpoint), and finitely many choices are justified by logic alone. For infinitely many pairs with no distinguishing rule, the existence of a choice function is exactly an instance of (countable) choice, which ZF does not prove.
2.
A linear dependence among vectors of $\bigcup C$ uses finitely many vectors $v_1, \dots, v_n$ , with $v_k \in S_k \in C$ . Since $C$ is a chain, one of $S_1, \dots, S_n$ contains all the others, so all $v_k$ lie in one independent set and the coefficients are all $0$ . The example $\{(1, 0)\} \cup \{(2, 0)\}$ shows why we need a chain.
3.
An ideal $J$ equals $R$ if and only if $1 \in J$ . If $1 \in U = \bigcup C$ , then $1 \in J$ for some $J \in C$ , so $J = R$ , contradicting that $J$ is proper. Hence $1 \notin U$ and $U$ is a proper ideal — an upper bound for the chain, as Zorn's lemma requires.
4.
Ordered bases: $7$ choices for $v_1$ (any non-zero vector), $8 - 2 = 6$ for $v_2$ (outside the $2$ -element span of $v_1$ ), $8 - 4 = 4$ for $v_3$ (outside the $4$ -element span of $v_1, v_2$ ): $7 \cdot 6 \cdot 4 = 168$ . Each unordered basis appears $3! = 6$ times, so there are $168 / 6 = 28$ bases. (The computation section counts the $840$ bases of $(\Z/2)^4$ the same way.)
5.
The ideals of $\Z/360$ are $(d)$ for $d \mid 360$ , with $(d) \subseteq (e)$ exactly when $e \mid d$ . The maximal proper ones are $(p)$ for the primes $p \mid 360 = 2^3 \cdot 3^2 \cdot 5$ : namely $(2), (3), (5)$ . So there are $3$ .
6.
Provable in ZF: sections of surjections from $\N$ (least preimage), the implication WO $\Rightarrow$ AC, and Schröder–Bernstein. Not provable: sections of all surjections from $\R$ (in Solovay's model there is no Vitali set, which such a section would produce from the quotient map $\R \to \R/\Q$ ), and the countable union theorem (Feferman–Lévy model).
7.
AC says: if each X i is non-empty then there is a choice function, an element of ∀ i, X i. In Lean: ∀ (ι : Type) (X : ι → Type), (∀ i, Nonempty (X i)) → Nonempty (∀ i, X i) — this is Lumenary.AxiomOfChoice.ChoiceFunctions (in an arbitrary universe). The converse is trivial and the other two statements are false.
8.
In the case $f(U) = 0$ , $f(V) = 1$ we show $\neg p$ : assuming $p$ , every $x \in \{0, 1\}$ belongs to both $U$ and $V$ , so by extensionality $U = V$ , hence $f(U) = f(V)$ , i.e. $0 = 1$ . In Lean this step is funext together with propext.
9.
```
def span(vectors):
    space = {0}
    for v in vectors:
        space |= {s ^ v for s in space}
    return space


def extend_to_basis(start, n):
    basis = list(start)
    for v in range(1, 2 ** n):
        if v not in span(basis):
            basis.append(v)
    return basis
```
This is the proof of Theorem 6 run on a finite space: keep adding vectors outside the span (each addition keeps the list independent) until nothing can be added — the list is then maximal, hence spanning, hence a basis. In a finite space the climb stops after at most $n$ additions; Zorn's lemma is what guarantees a maximal independent set in infinite dimensions.