选择公理（AC）是集合论中的一条公理，断言对于任意以集合为指标集的非空集合族，都存在一个从每个集合中选取一个元素的函数。即使没有明确指定选择规则，它也保证这种同时选择的存在性。在策梅洛—弗兰克尔集合论（ZF）中加入 AC，便得到称为 ZFC 的公理系统。选择公理将有关无限集合的基础问题与数学各领域中的存在性定理联系起来。(math.vanderbilt.edu)
形式表述与解释
设 (I) 是一个集合，((A_i){i\in I}) 是一个非空集合族。AC 断言，存在一个函数 [ f:I\longrightarrow\bigcup{i\in I}A_i ] 使得 [ f(i)\in A_i\qquad\text{对每个 }i\in I. ] 这样的 (f) 称为选择函数。这些集合不必互不相交，不同的指标也可以对应同一个集合。等价地，任意非空集合族的笛卡尔积都是非空的：积中的一个元素，恰好就是为每个因子同时指定一个成员。(math.vanderbilt.edu)
这里的“选择”并不是指一个随时间进行的过程、随机抽取或计算程序。这条公理断言的是存在性，而非唯一性，也不提供寻找所选元素的算法。不过，在某个具体情形中，仍可能存在明确的选择函数；此时就无须援引 AC。(math.vanderbilt.edu)
对于有限集合族，选择函数的存在性可以在 ZF 中证明。如果有统一的选择规则，无限多次选择也可能不依赖 AC。例如，可以从自然数的每个非空子集中选取其最小元素。因此，问题并不只在于无限性，而在于如何从没有给定选择规则的任意集合族中进行选择。(sites.lsa.umich.edu)
等价原理
在 ZF 的基础上，若干表述不同的命题与 AC 等价：它们都可以由 AC 推出，而将其中任何一个加入 ZF，也都能推出 AC。以下三种表述尤为重要：(people.math.ethz.ch)
- **良序定理：**每个集合都可以赋予一个全序，使其每个非空子集都有最小元素。这个序不必与该集合原有的序相似。
- **佐恩引理：**如果一个非空的偏序集中的每条链都在该集合中有上界，那么这个偏序集就有极大元素。链是指元素两两可比较的子集；极大元素不一定大于所有其他元素。
- **满射的分裂：**每个满射函数 (p:X\to Y) 都有一个右逆 (s:Y\to X)，满足 (p(s(y))=y)。这样的右逆从每个纤维 (p^{-1}({y})) 中选取一个元素。(people.math.ethz.ch)
这些表述提供了不同的证明方法。良序使得沿有序集合逐步进行构造成为可能，而佐恩引理则用于证明某个对象的存在性：在保持指定性质的前提下，该对象无法再扩大。(people.math.ethz.ch)
数学应用
在线性代数中，AC 蕴含每个域上的向量空间都有一组基。一种标准证明是对由线性无关子集组成的偏序集应用佐恩引理。极大的线性无关子集必定张成整个空间，否则就还能加入另一个向量。“每个向量空间都有一组基”这一全称命题本身，在 ZF 的基础上也与 AC 等价。(people.math.ethz.ch)
在拓扑学中，吉洪诺夫定理断言：任意一族紧空间的积，在积拓扑下仍是紧的。在这种不加限制的形式下，它与 AC 等价。选择公理也为泛函分析中的延拓论证提供支持，尤其是哈恩—巴拿赫定理的证明。不过，一个定理是 AC 的推论，并不意味着它就与 AC 等价。(people.math.ethz.ch)
选择公理在测度论和几何学中还有一些不那么直观的推论。它能推出实数轴上存在相对于勒贝格测度不可测的子集。它也使巴拿赫—塔斯基悖论的构造成为可能：三维欧几里得空间中的一个实心球，可以被分割为有限多个集合，再通过刚体运动重新拼成两个与原球全等的球。这些部分并不是普通的物理碎片；由于它们不可测，通常的体积可加性论证不再适用。(publish.uwo.ca)
历史与独立性
1904 年，恩斯特·策梅洛在证明每个集合都可以良序化时，明确提出了 AC。由此引发的争论集中在一个问题上：存在性证明是否可以合理地依赖于未给出具体规则的同时选择。(publish.uwo.ca)
1938 年，库尔特·哥德尔宣布了一项相对一致性结果：如果 ZF 是一致的，那么加入 AC 不会引入矛盾。他的方法利用了可构造宇宙，这是一个满足选择公理的集合内宇宙。1963 年，保罗·科恩利用与力迫法有关的方法，以及选择公理不成立的模型，证明了与之互补的独立性结果。(pmc.ncbi.nlm.nih.gov)
综合这两项结果可知，在假定 ZF 一致的前提下，无论 AC 还是它的否定，都无法从 ZF 中证明。这些结果并没有证明 ZF 本身的绝对一致性。不采用 AC 也不同于断言 AC 的否定：仅凭 ZF，无法判定这一问题。(pmc.ncbi.nlm.nih.gov)
受限的选择原理
较弱的选择原理对所考虑的集合族或选择方式作出限制。可数选择公理断言：对于每个以可数集为指标集的非空集合族，都存在一个选择函数。完整的 AC 蕴含这一原理，但在 ZF 的基础上，反向蕴含不成立。这些区分使数学基础研究能够明确某个论证究竟需要多强的选择原理，而不必把每一次无限选择都视为完整 AC 的应用。(plato.stanford.edu)