选择公理

量词次序揭示了公理的内容。已知

只逐个保证有候选；AC 把它提升为

也就是一个同时完成全部选择的集合对象。有限族可以逐步挑选后拼成函数，无需 AC。无限族若每个成员有统一规则也同样不需要，例如从每个非空自然数子集取最小元。公理处理的是没有这类共同规则的任意集合族，并只断言函数存在，不提供算法或可定义公式。

“每个向量空间都有基公理库向量空间的基Basis of a vector space同时线性无关并张成整个向量空间的向量组。”是标准等价形式。把所有线性无关子集按包含排序；一条链的并仍线性无关，Zorn 引理给出极大线性无关集。若它未张成整个空间，加入一个不在其张成中的向量仍保持线性无关，违背极大性，所以它是基。证明给出存在性，却通常不给出可计算的基。

同一差别可在集合族上直接看见。若 $A_n\subseteq \mathbb{N}$ 非空，$f(n)=min{A}_n$ 是显式选择，不用 AC；若 $(A_i{)}_{i\in I}$ 是没有附加结构的任意非空集合族，断言其积非空正是 AC。知道每次选择都“做得到”，不等于已经拥有所有选择组成的函数。

选择原则还有严格强弱。可数选择只处理可数指标族，依赖选择允许按前一步结果继续选取；两者都弱于完整 AC。紧 Hausdorff 空间的 Tychonoff 定理只需布尔素理想定理（超滤子引理），也弱于完整 AC。另一方面，AC 可推出非 Lebesgue 可测实数集和 Banach–Tarski 分解；这些结论反映其非构造性强度，不是逻辑矛盾。

独立性边界要准确表述：ZF 不能证明每个集合族都有选择函数，也不能证明某个具体熟悉族一定没有。某些选择函数可在 ZF 中显式构造，另一些全称存在命题则确实具有完整 AC 的强度。

良序定理使每个集合由某个初始序数代表，从而让任意两集合的基数公理库基数Cardinality · Size of a set忽略元素性质与排列，只用双射和单射刻画集合的大小及其比较。可比较；它也支撑无限基数加法和乘法的常见坍缩公式。Zorn 引理适合证明极大对象存在，包括向量空间基、非零含幺环中的极大理想以及多种延拓定理。

Tychonoff 定理把选择强度带入拓扑，任意非空集合族的积刻画又把它直接接回集合论。实际证明应记录真正使用的版本：有典范选择时显式构造，只需序列式选择时使用可数选择或依赖选择，只有全称命题确实需要时才调用完整 AC。