Axiom of Choice

The Axiom of Choice is a controversial axiom of set theory. In addition to those of $Z F$ it forms the final axiom of $Z F C$ . Some equivalent formulations are #m/def/set/zfc

For any set $𝑋$ of inhabited sets, there exists a choice function $𝑓 : 𝑋 ↣ ⋃ 𝑋$ .

(\forall 𝔐 𝑋) [(\forall 𝑥 \in 𝑋) (\exists 𝑦 \in 𝑥) ⟹ (\exists 𝑓 : 𝑋 \to ⋃ 𝑋) (\forall 𝐴 \in 𝑋) [𝑓 (𝐴) \in 𝐴]]

Let $𝐴, 𝐵$ be functions and $𝑃 \subseteq 𝐴 \times 𝐵$ be a Relation. If $𝑃$ is left-total, i.e. relates every $𝑥 \in 𝐴$ with at least one $𝑦 \in 𝐵$ , then there exists a choice function that selects such a $𝑦$ for each $𝑥$ , i.e.

(\forall 𝑥 \in 𝐴) (\exists 𝑦 \in 𝐵) 𝑃 (𝑥, 𝑦) ⟹ (\exists 𝑓 : 𝐴 \to 𝐵) (\forall 𝑥 \in 𝐴) 𝑃 (𝑥, 𝑓 (𝑥))

The cartesian product of an arbitrary collection of inhabited sets is itself inhabited.

(\forall 𝛼 \in 𝐴) [𝑋 𝛼 \neq \emptyset] ⟹ \prod 𝛼 \in 𝐴 𝑋 𝛼 \neq \emptyset

Every surjection in $𝖲 𝖾 𝗍$ is split epic. This structuralist formulation is an example of the External Axiom of Choice.

Proof of equivalence over

Z F

#missing/proof

In other theories

In type theory we have the Propositional Axiom of Choice, requiring propositional truncation.

Other equivalences

Set-theoretic
Topological
- Tikhonov's theorem

Relationship to other axioms

Weakenings

Over $Z F$

#state/tidy | #lang/en | #SemBr